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?
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.
“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?
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.
Could you elaborate on this? What is the slightly-more-than-n-symbols-long proof?
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.
“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.