= 27d567bc2d48d9f40e9ccc20ea370b15)
dankane comments on Robust Cooperation in the Prisoner's Dilemma - 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 (145)
Ah, never mind I see it. You just need to modify the proof of Lob's Theorem. Instead of using L = (there exists a proof of L) -> S you instead use L = (there exists a proof of L of length at most Ackermann(10)) -> S and the rest of the proof of Lob's Theorem still works.
Yeah, that's the main idea. Note that to state the bounded version of Lob's theorem, you actually have to use two separate limits: "if having a bounded-size proof of statement S would imply the truth of S, and that fact itself has a short enough proof, then S is provable". The proof is similar to the regular Lob's theorem, but each step has to keep track of length limits, and these bookkeeping details eventually determine how high the limits have to be in the first place for the theorem to be true.