You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

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

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.

Comments (100)

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

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)