1
$\begingroup$

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

$\endgroup$
2
  • 1
    $\begingroup$ The procedure is uniform, it uses the description of $F$ as a black box. Thus, it can be described by an algorithm of constant size + a description of a subroutine defining $F$ + a description of $n$. This gives an $O(f+\log n)$ upper bound. Whether it can be described in an even shorter way (it likely can, in some cases) is irrelevant for the argument. $\endgroup$ Sep 20, 2022 at 9:46
  • $\begingroup$ @EmilJeřábek Many thanks for the comment. Just to be sure, you are saying: that there is a universal Turing machine whose description contains a) description of $F$ b) the number $n$, and c) the common overhead for iteration etc., which we run to iterate over strings of length n and enumerate all proofs for such strings. Possibly also: we cannot omit the description of F because we need to know that $P$ is valid within F, i.e. in hindsight, my problem was thinking of F as being outside the TM. $\endgroup$ Sep 20, 2022 at 10:21

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thank you for the detailed answer. I will digest it carefully. As an aside though, I shall have to carefully consider the idea that a system can be without inconsistencies and yet proves false theorems (to be correct)! ( I can't help thinking that false proofs should "pollute" the system, but maybe the system just gets partitioned into consistently True and consistently False sub-systems?) Anyway, lot to learn from, thank you. $\endgroup$ Oct 22, 2022 at 13:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.