(Cross-posted from Computer Science due to lack of response after 1 week)
From An Introduction to Kolmogorov Complexity and Its Applications, Li & Vitany, 4th Ed. Example 1.1.1.
As you might guess, given that I have been tripped up by the very first example, I am just getting to grips with incompleteness, Kolmogorov complexity etc. so mea culpa if this is just a dumb noob question.
This example concerns "Godel’s incompleteness result"; the authors aim to use the incompressibility argument (i.e. that there are random strings of every length) to prove by contradiction that there are infinitely many undecidable statements in some sound formal system F.
We need first their definition of random, i.e. uncompressible (maximal Kolmogorov complexity)
We write “x is random” if the shortest binary description of x with respect to the optimal specification method $D_0$ has length at least that of the literal description of x
The part of the argument I don't follow and would like help understanding occurs in this section:
Fix any sound formal system F in which we can express statements like “x is random.” Suppose F can be described in f bits — assume, for example, that this is the number of bits used in the exhaustive description of F in the first chapter of the textbook Foundations of F. We claim that for all but finitely many random strings x, the sentence “x is random” is not provable in F. Assume the contrary. Then given F, we can start to search exhaustively for a proof that some string of length $n \gg f$ is random, and print it when we find such a string. This is an x satisfying the “x is random” sentence. This procedure to print x of length n uses only log n + f bits of data, where log denotes the binary logarithm, which is much less than n. But x is random by the proof, which is a true fact since F is sound, and thus its shortest effective description has binary length at least n. Hence, F is not consistent, which is a contradiction.
Problem Given a string of length n, the argument relies on the length of a procedure P with respect to $D_0$ being given by both
- $|P| = log_2(n) + f$ (Eq I)
- $|P| > n$, (Eq II) because "x is random" (and strictly > because there must be some instruction to output the "literal description of x" having length n)
We were told that $n \gg f$, i.e. $f \ll n$ and hence necessarily in Eq I that $log_2(n) + f < n$ (for sufficiently large n), contradicting Eq II.
Which implies that F is not consistent, but ex hypothesis F is sound (i.e. consistent) therefore the assumption that '"x is random" is provable in F' (for arbitrary x) must be false.
However, whilst I have no problem with the statement that formal system F "can be described in f bits", it is not obvious to me that the f bits required to describe F are (all) necessarily part of P per Eq I. It is conceivable to me that P could be vastly longer than f bits, or considerably shorter.
Question(s) How does the argument work given that the length of a proof is (surely?) not directly related to the length of the procedure/statement to be proved? Why is the length of the description of F relevant at all? etc. etc. etc.