Nisan comments on A model of UDT with a halting oracle

Nisan 29 Jan 2012 19:18 UTC
1 point
The conclusions that I think I can draw are

¬(S⊢A()=a)∧(S⊢A()=b) ⇒ Con(S)∧¬Con(S+Con(S)) ⇒ A()=b

So if one player plays chicken on the second inspected action, then all of them do.
- cousin_it 29 Jan 2012 21:15 UTC
  0 points
  Parent
  I’m still not getting it. Can you explain the proof of the following:
  
  Con(S)∧¬Con(S+Con(S)) ⇒ A()=b
  - Nisan 30 Jan 2012 0:59 UTC
    2 points
    Parent
    ¬Con(S+Con(S)) ⇒ S⊢¬Con(S)
    
    ⇒ S⊢Prv(A()≠a) (if S is inconsistent, then it proves anything)
    
    ⇒ S⊢A()=a (because A plays chicken)
    
    ⇒ S⊢A()≠b
    
    Con(S)∧¬Con(S+Con(S)) ⇒ Con(S)∧(S⊢A()≠b) (follows directly from 4)
    
    ⇒ (S⊬A()=b)∧(S⊢A()≠b) (a consistent theory can’t prove a proposition and its negation)
    
    ⇒ (S⊬A()≠a)∧(S⊢A()≠b) (here I’m assuming that S⊢(A()=a∨A()=b). I don’t know what to do if A can choose between more than two alternatives.)
    
    ⇒ A()=b (A plays chicken on the second inspected action)