cousin_it comments on A model of UDT with a halting oracle

cousin_it 29 Jan 2012 11:18 UTC
0 points
Thanks! I think you found a real hole and the conclusion is also wrong. Or at least I don’t see how

(S⊢¬P)⇒¬Con(S+Con(S))

implies the conclusion.
- Nisan 29 Jan 2012 19:18 UTC
  1 point
  Parent
  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)