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.

Article Navigation

Comments (100)

Comments (100)

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

Comment author: cousin_it 19 December 2011 08:36:01PM *  5 points [-]

I can't solve your problem yet, but I found a cute lemma. Let P be the proposition "A()=a" where a is the first action inspected in step 1 of A's algorithm.

  1. (S⊢¬P)⇒P (by inspection of A)

  2. S⊢((S⊢¬P)⇒P) (S can prove 1)

  3. (S⊢(S⊢¬P))⇒(S⊢P) (unwrap 2)

  4. (S⊢¬P)⇒(S⊢(S⊢¬P)) (property of any nice S)

  5. (S⊢¬P)⇒(S⊢P) (combine 3 and 4)

  6. (S⊢¬P)⇒(S⊢(P∧¬P)) (rephrasing of 5)

  7. (S⊢¬P)⇒¬Con(S)

All the above steps can also be formalized within S, so each player knows that if any player plays chicken with the first inspected action, then S is inconsistent. The proof generalizes to the second inspected action, etc., by looking at the first one that yields a contradiction. But if S is inconsistent, then it will make all players play chicken. So if one player plays chicken, then all of them do, and that fact is provable within S.

Did you manage to make any progress?

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 [-]

  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)

Powered by Reddit Powered by Reddit