cousin_it comments on A model of UDT with a halting oracle

cousin_it 29 Jan 2012 21:15 UTC
0 points
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
  1. ¬Con(S+Con(S)) ⇒ S⊢¬Con(S)
  2. ⇒ S⊢Prv(A()≠a) (if S is inconsistent, then it proves anything)
  3. ⇒ S⊢A()=a (because A plays chicken)
  4. ⇒ S⊢A()≠b
  5. Con(S)∧¬Con(S+Con(S)) ⇒ Con(S)∧(S⊢A()≠b) (follows directly from 4)
  6. ⇒ (S⊬A()=b)∧(S⊢A()≠b) (a consistent theory can’t prove a proposition and its negation)
  7. ⇒ (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.)
  8. ⇒ A()=b (A plays chicken on the second inspected action)