Nisan comments on A model of UDT with a halting oracle - Less Wrong

41 Post author: cousin_it 18 December 2011 02:18PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Sort By: Best

You are viewing a single comment's thread. Show more comments above.

Comment author: Nisan 29 January 2012 07:36:23AM 3 points [-]

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.

Comment author: cousin_it 29 January 2012 11:18:43AM 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.

Comment author: Nisan 29 January 2012 07:18:00PM 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.

Comment author: cousin_it 29 January 2012 09:15:08PM 0 points [-]

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

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

Comment author: Nisan 30 January 2012 12:59:37AM 2 points [-]

¬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)

Comments (100)