In particular I wish to extract from that paper the following very simple (albeit non-constructive) proof of Chaitin’s Incompleteness:
Given a (reasonable, sound) formal theory F, we know that F cannot prove all true sentences of the form “Program P never halts” (the reason is that if it could, we could solve the halting problem by searching over all possible proofs in F for the proof of P either halting with a particular run, or never halting, being sure our search will finish in finite time). Consider the shortest program P such that P never halts but F cannot prove that fact. Let L(P) be its length. Claim: F can never prove that Kolmogorov complexity of anything can be greater than L(P). Proof: given any output X, F can never refute the possibility that P might yet halt at some future time and output exactly X. Therefore L(P) must remain a candidate for the Kolmogorov complexity of X as far as F is concerned.
Edit: nevermind this. I’ve realized the proof is wrong. It’s only true that “F can never refute the possibility that P might yet halt at some time and output some Y”, but it is not true that “F can never refute the possibility that P might yet halt and output this specific X”. It’s conceivable (albeit unusual) that P doesn’t halt, F is unable to prove that, but is able to prove that should P halt, its output will not be X. For example, think of P as a Turing machine with one halt state, which is easily “backwards-traceable” to a sequence of actions that erases the entire tape so far and writes out “123″. Then F can easily be strong enough to be able to prove that if P halts at all, it outputs “123” and not anything else.
I emailed the article’s author and he replied acknowledging the problem, which has been raised by a bunch of people before, and giving me links to a few paywalled articles with the correct exposition. However, this correct exposition is nowhere as succint and attractive as the short and faulty proof above.
In particular I wish to extract from that paper the following very simple (albeit non-constructive) proof of Chaitin’s Incompleteness:
Given a (reasonable, sound) formal theory F, we know that F cannot prove all true sentences of the form “Program P never halts” (the reason is that if it could, we could solve the halting problem by searching over all possible proofs in F for the proof of P either halting with a particular run, or never halting, being sure our search will finish in finite time). Consider the shortest program P such that P never halts but F cannot prove that fact. Let L(P) be its length. Claim: F can never prove that Kolmogorov complexity of anything can be greater than L(P). Proof: given any output X, F can never refute the possibility that P might yet halt at some future time and output exactly X. Therefore L(P) must remain a candidate for the Kolmogorov complexity of X as far as F is concerned.
Edit: nevermind this. I’ve realized the proof is wrong. It’s only true that “F can never refute the possibility that P might yet halt at some time and output some Y”, but it is not true that “F can never refute the possibility that P might yet halt and output this specific X”. It’s conceivable (albeit unusual) that P doesn’t halt, F is unable to prove that, but is able to prove that should P halt, its output will not be X. For example, think of P as a Turing machine with one halt state, which is easily “backwards-traceable” to a sequence of actions that erases the entire tape so far and writes out “123″. Then F can easily be strong enough to be able to prove that if P halts at all, it outputs “123” and not anything else.
I emailed the article’s author and he replied acknowledging the problem, which has been raised by a bunch of people before, and giving me links to a few paywalled articles with the correct exposition. However, this correct exposition is nowhere as succint and attractive as the short and faulty proof above.
LOL