Kolmogorov Complexity - Chaitin's Incompleteness Theorem | Chaitin Incompleteness Theorem

Chaitin's Incompleteness Theorem

We know that, in the set of all possible strings, most strings are complex in the sense that they cannot be described in any significantly "compressed" way. However, it turns out that the fact that a specific string is complex cannot be formally proved, if the complexity of the string is above a certain threshold. The precise formalization is as follows. First, fix a particular axiomatic system S for the natural numbers. The axiomatic system has to be powerful enough so that, to certain assertions A about complexity of strings, one can associate a formula F_A in S. This association must have the following property:

if F_A is provable from the axioms of S, then the corresponding assertion A must be true. This "formalization" can be achieved, either by an artificial encoding such as a Gödel numbering, or by a formalization which more clearly respects the intended interpretation of S.

Theorem: There exists a constant L (which only depends on the particular axiomatic system and the choice of description language) such that there does not exist a string s for which the statement

(as formalized in S) can be proven within the axiomatic system S.

Note that, by the abundance of nearly incompressible strings, the vast majority of those statements must be true.

The proof of this result is modeled on a self-referential construction used in Berry's paradox. The proof is by contradiction. If the theorem were false, then

Assumption (X): For any integer n there exists a string s for which there is a proof in S of the formula "K(s) ≥ n" (which we assume can be formalized in S).

We can find an effective enumeration of all the formal proofs in S by some procedure

function NthProof(int n)

which takes as input n and outputs some proof. This function enumerates all proofs. Some of these are proofs for formulas we do not care about here, since every possible proof in the language of S is produced for some n. Some of these are complexity formulas of the form K(s) ≥ n where s and n are constants in the language of S. There is a program

function NthProofProvesComplexityFormula(int n)

which determines whether the nth proof actually proves a complexity formula K(s) ≥ L. The strings s, and the integer L in turn, are computable by programs:

function StringNthProof(int n) function ComplexityLowerBoundNthProof(int n)

Consider the following program

function GenerateProvablyComplexString(int n) for i = 1 to infinity: if NthProofProvesComplexityFormula(i) and ComplexityLowerBoundNthProof(i) ≥ n return StringNthProof(i)

Given an n, this program tries every proof until it finds a string and a proof in the formal system S of the formula K(s) ≥ L for some L ≥ n. The program terminates by our Assumption (X). Now, this program has a length U. There is an integer n₀ such that U + log₂(n₀) + C < n₀, where C is the overhead cost of

function GenerateProvablyParadoxicalString return GenerateProvablyComplexString(n₀)

The program GenerateProvablyParadoxicalString outputs a string s for which there exists an L such that K(s) ≥ L can be formally proved in S with L ≥ n₀. In particular, K(s) ≥ n₀ is true. However, s is also described by a program of length U + log₂(n₀) + C, so its complexity is less than n₀. This contradiction proves Assumption (X) cannot hold.