Nisan comments on A model of UDT with a halting oracle

[Nisan]

The proof generalizes to the second inspected action, etc., by looking at the first one that yields a contradiction.

I tried this in the case that the output of A provably lies in the set {a,b}. I only managed to prove

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

where P is the proposition “A()=b” where b is the second inspected action. But this still implies

if one player plays chicken, then all of them do, and that fact is provable within S.

[cousin_it]

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]

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]

I’m still not getting it. Can you explain the proof of the following:

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

[Nisan]

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)