Kindly comments on Bounded versions of Gödel's and Löb's theorems - Less Wrong

32 Post author: cousin_it 27 June 2012 06:28PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (21)

You are viewing a single comment's thread.

Comment author: Kindly 28 June 2012 12:00:32AM 2 points [-]

Since f(n)>>exp(g(n)), and the theory T proves in n symbols that "T can't prove a falsehood in f(n) symbols", we see that T proves in slightly more than n symbols that the program R won't find any proofs.

Could you elaborate on this? What is the slightly-more-than-n-symbols-long proof?

Comment author: Zetetic 28 June 2012 01:01:44AM *  2 points [-]

As I understand it, because T proves in n symbols that "T can't prove a falsehood in f(n) symbols", taking the specification of R (program length) we could do a formal verification proof that R will not find any proofs, as R only finds a proof if T can prove a falsehood within g(n)<exp(g(n)<<f(n) symbols. So I'm guessing that the slightly-more-than-n-symbols-long is on the order of:

n + Length(proof in T that R won't print with the starting true statement that "T can't prove a falsehood in f(n) symbols")

This would vary some with the length of R and with the choice of T.

Comment author: cousin_it 28 June 2012 12:27:12AM *  2 points [-]

"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?

Comment author: Kindly 28 June 2012 12:49:47AM 1 point [-]

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?

Comment author: cousin_it 28 June 2012 01:16:51AM *  1 point [-]

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.