= 27d567bc2d48d9f40e9ccc20ea370b15)
cousin_it comments on Bounded versions of Gödel's and Löb's theorems - 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 (21)
"If R found a proof, then two proofs would exist: a proof of length g(n) found by R, and a proof by simulation of length exp(g(n)) that R does the opposite thing. Together they would yield a proof of falsehood in less than f(n) symbols. But I know that T can't prove a falsehood in less than f(n) symbols. That's a contradiction, so R won't find a proof."
That reasoning is quite short. The description of R is bounded by the description of T, which is not longer than n symbols. The proof that "T can't prove a falsehood in f(n) symbols" has n symbols by assumption. So overall it should be no more than linear in n. Does that make sense, or have I missed something?
How do we know what the proof by simulation does in exp(g(n)) symbols, if the length of our argument is linear in n?
Exhibiting the complete proof by simulation is not necessary, I think. It's enough to prove that it exists, that its length is bounded, and that it must contradict the proof found by R. All these statements have simple proofs by inspection of R.