Clarification sought re Li & Vitanyi's Proof of Godel Incompleteness in Formal System F

Question

(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.

Answer 1

In this argument, we assume that the formal system F provides us with a way to check whether a proof of a mathematical statement is correct. Thus formally, we assume that there is a computable function CORR such that for mathematical statement $s$ and proof $p$, the value CORR$(s,p)$ equals True if and only if $p$ is a correct proof of $s$ in F. For convenience and rigor, let us assume that statements and proofs are encoded using some finite alphabet $\Sigma$.

For now, let us assume that such a computable function exists. Let us observe that all F-provable statements can be enumerated. This means that there exists a Turing machine with a separate output tape. The machine works infinitely long and each statement $s$ that has a proof should at some point appear on this output tape. Such a machine can be constructed as follows. It enumerates all pairs $(s,p)$ of strings in $\Sigma^*$, and each time $p$ is a valid proof of $s$, it writes $s$ on the output tape. By construction, a statement appears on the output tape if and only if it is provable in F.

Finally, the algorithm $P$ of your question has a value $n$ hardcoded and runs the above program until there appears a statement of the form "$x$ is random" with $x$ of length at least $n$. When found, it prints $x$.

Let us finish the proof assuming that F is sound. If for some $n$, the program $P$ outputs a string $x$, then we found a program of length $O(\log n) + c + O(1)$, where $c$ is the bitsize of the program for CORR. On the other hand, if F is sound, then $x$ must be random. In other words, no program shorter than $n$ prints $x$. Combined this implies that $O(\log n) + c + O(1) \ge n$ and this implies that $n$ is bounded by a constant. In conclusion, if the statement "$x$ is random" is provable, then the length of $x$ must be bounded by a constant.

Although it is not important for the above argument, let us anyway talk about the function CORR, which checks whether a statement $s$ and a proof $p$ in $F$ are correct. Often, a formal system consists out of a finite set of axioms and a list of deduction rules. A deduction rule transforms a few statements into another statement. A proof encodes which statements should be used, which deduction rule should be applied, and perhaps some auxiliary information (e.g. what variables are substituted). It is easy to believe that such procedures can be checked by an algorithm. In fact, there exist theorem provers like COQ and isabelle/HOL that do such things. To write such a procedure, one just needs to know the axioms and deduction rules, and the size of their description is denoted $f$ in the above argument.

Remark. In the above argument we used that F is sound. This is in some sense unsatisfying, we might be ready to accept formal system that proves false theorems, as long as it is sufficiently powerful and has no inconsistencies. This is Rosser's variant of Godel's incompleteness theorem: if F is consistent and sufficiently powerful, then F can neither prove or disprove some statement. In the above argument, we already said that statements "$x$ is random" are not provable whenever $x$ is large. Now we explain that F can not declare all statements "x is random" to be false for large x, because this would violate the pigeon whole principle (there are $2^n$ strings of length $n$, but the number of strings of length less than $n$ equals $1 + 2^1 + ... + 2^{n-1} < 2^n$). Thus if F is sufficiently powerful, it can prove that not all strings of a given length $n$ are random. On the other hand, if it declares all these strings to be nonrandom, F would be inconsistent, and this contradicts the assumption.