= 27d567bc2d48d9f40e9ccc20ea370b15)
Douglas_Knight comments on A model of UDT with a halting oracle - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (100)
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.
(S⊢¬P)⇒P (by inspection of A)
S⊢((S⊢¬P)⇒P) (S can prove 1)
(S⊢(S⊢¬P))⇒(S⊢P) (unwrap 2)
(S⊢¬P)⇒(S⊢(S⊢¬P)) (property of any nice S)
(S⊢¬P)⇒(S⊢P) (combine 3 and 4)
(S⊢¬P)⇒(S⊢(P∧¬P)) (rephrasing of 5)
(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?
Cool.
I had a lot of trouble reading this because in my mind ⇒ binds tighter than ⊢. When I figured it out, I was going to suggest that you use spaces to hint at parsing, but you already did. I don't know what would have helped.