Editing Kolmogorov complexity (section)

==Chaitin's incompleteness theorem==
[[File:Kolmogorov complexity and computable lower bounds svg.svg|thumb|right|600px|Kolmogorov complexity {{color|#ff0000|''K''(''s'')}}, and two computable lower bound functions <code>{{color|#00e000|prog1(s)}}</code>, <code>{{color|#0000ff|prog2(s)}}</code>. The horizontal axis ([[logarithmic scale]]) enumerates all [[string (computer science)|strings]] ''s'', ordered by length; the vertical axis ([[linear scale]]) measures Kolmogorov complexity in [[bit]]s. Most strings are incompressible, i.e. their Kolmogorov complexity exceeds their length by a constant amount. 9 compressible strings are shown in the picture, appearing as almost vertical slopes. Due to Chaitin's incompleteness theorem (1974), the output of any program computing a lower bound of the Kolmogorov complexity cannot exceed some fixed limit, which is independent of the input string ''s''.]]
By the above theorem ({{slink||Compression}}), 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 proven, 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 number]]s. The axiomatic system has to be powerful enough so that, to certain assertions  '''A''' about complexity of strings, one can associate a formula '''F'''<sub>'''A'''</sub> in '''S'''. This association must have the following property:

If '''F'''<sub>'''A'''</sub> is provable from the axioms of '''S''', then the corresponding assertion '''A''' must be true. This "formalization" can be achieved based on a [[Gödel numbering]].

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

:''K''(''s'') ≥  ''L'' &nbsp;  &nbsp;  &nbsp; (as formalized in '''S''')

can be proven within '''S'''.<ref>{{cite journal | url=http://www.cas.mcmaster.ca/~sancheg/EE_UCU2006_thesis/biblio/Information-theoretic%20limitations%20of%20Formal%20Systems%20(acm74).pdf | author=Gregory J. Chaitin | title=Information-theoretic limitations of formal systems | journal=Journal of the ACM | volume=21 | number=3 | pages=403&ndash;434 | date=Jul 1974 | doi=10.1145/321832.321839 | s2cid=2142553 }} Here: Thm.4.1b</ref><ref>{{Cite book|last=Calude |first=Cristian S. |title=Information and Randomness: an algorithmic perspective |date=12 September 2002 |publisher=Springer |url=https://www.springer.com/br/book/9783540434665 |language=en |isbn=9783540434665 }}</ref>

'''Proof Idea''': The proof of this result is modeled on a self-referential construction used in [[Berry's paradox]]. We firstly obtain a program which enumerates the proofs within '''S''' and we specify a procedure ''P'' which takes as an input an integer ''L'' and prints the strings ''x'' which are within proofs within '''S''' of the statement ''K''(''x'') ≥ ''L''. By then setting ''L'' to greater than the length of this procedure ''P'', we have that the required length of a program to print ''x'' as stated in ''K''(''x'') ≥ ''L'' as being at least ''L'' is then less than the amount ''L'' since the string ''x'' was printed by the procedure ''P''. This is a contradiction. So it is not possible for the proof system '''S''' to prove ''K''(''x'') ≥ ''L'' for ''L'' arbitrarily large, in particular, for ''L'' larger than the length of the procedure ''P'', (which is finite).

'''Proof''':

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'')&nbsp;≥&nbsp;''n'' where ''s'' and ''n'' are constants in the language of '''S'''. There is a procedure

 '''function''' NthProofProvesComplexityFormula('''int''' ''n'')

which determines whether the ''n''th proof actually proves a complexity formula ''K''(''s'')&nbsp;≥&nbsp;''L''. The strings ''s'', and the integer ''L'' in turn, are computable by procedure:

 '''function''' StringNthProof('''int''' ''n'')

 '''function''' ComplexityLowerBoundNthProof('''int''' ''n'')

Consider the following procedure:

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

Given an ''n'', this procedure tries every proof until it finds a string and a proof in the formal system '''S''' of the formula ''K''(''s'')&nbsp;≥&nbsp;''L'' for some ''L''&nbsp;≥&nbsp;''n''; if no such proof exists, it loops forever.

Finally, consider the program consisting of all these procedure definitions, and a main call:

 GenerateProvablyComplexString(''n''<sub>0</sub>)

where the constant ''n''<sub>0</sub> will be determined later on. The overall program length can be expressed as ''U''+log<sub>2</sub>(''n''<sub>0</sub>), where ''U'' is some constant and log<sub>2</sub>(''n''<sub>0</sub>) represents the length of the integer value ''n''<sub>0</sub>, under the reasonable assumption that it is encoded in binary digits. We will choose ''n''<sub>0</sub> to be greater than the program length, that is, such that ''n''<sub>0</sub> > ''U''+log<sub>2</sub>(''n''<sub>0</sub>).  This is clearly true for ''n''<sub>0</sub> sufficiently large, because the left hand side grows linearly in ''n''<sub>0</sub> whilst the right hand side grows logarithmically in ''n''<sub>0</sub> up to the fixed constant ''U''.

Then no proof of the form "''K''(''s'')≥''L''" with ''L''≥''n''<sub>0</sub> can be obtained in '''S''', as can be seen by an [[indirect argument]]:
If <code>ComplexityLowerBoundNthProof(i)</code> could return a value ≥''n''<sub>0</sub>, then the loop inside <code>GenerateProvablyComplexString</code> would eventually terminate, and that procedure would return a string ''s'' such that
{| style="border: 1px solid darkgray;"
|-
| || ''K''(''s'')
|-
| ≥ || ''n''<sub>0</sub> || &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; || by construction of <code>GenerateProvablyComplexString</code>
|-
| > || ''U''+log<sub>2</sub>(''n''<sub>0</sub>) || || by the choice of ''n''<sub>0</sub> 
|-
| ≥ || ''K''(''s'') || || since ''s'' was described by the program with that length
|}
This is a contradiction, [[Q.E.D.]]

As a consequence, the above program, with the chosen value of ''n''<sub>0</sub>, must loop forever.

Similar ideas are used to prove the properties of [[Chaitin's constant]].