<p>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 <span class="math-container">$s$</span> and proof <span class="math-container">$p$</span>, the value CORR<span class="math-container">$(s,p)$</span> equals True if and only if <span class="math-container">$p$</span> is a correct proof of <span class="math-container">$s$</span> in F. For convenience and rigor, let us assume that statements and proofs are encoded using some finite alphabet <span class="math-container">$\Sigma$</span>.</p>
<p>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 <span class="math-container">$s$</span> 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 <span class="math-container">$(s,p)$</span> of strings in <span class="math-container">$\Sigma^*$</span>, and each time <span class="math-container">$p$</span> is a valid proof of <span class="math-container">$s$</span>, it writes <span class="math-container">$s$</span> on the output tape. By construction, a statement appears on the output tape if and only if it is provable in F.</p>
<p>Finally, the algorithm <span class="math-container">$P$</span> of your question has a value <span class="math-container">$n$</span> hardcoded and runs the above program until there appears a statement of the form &quot;<span class="math-container">$x$</span> is random&quot; with <span class="math-container">$x$</span> of length at least <span class="math-container">$n$</span>. When found, it prints <span class="math-container">$x$</span>.</p>
<p>Let us finish the proof assuming that F is sound. If for some <span class="math-container">$n$</span>, the program <span class="math-container">$P$</span> outputs a string <span class="math-container">$x$</span>, then we found a program of length <span class="math-container">$O(\log n) + c + O(1)$</span>, where <span class="math-container">$c$</span> is the bitsize of the program for CORR. On the other hand, if F is sound, then <span class="math-container">$x$</span> must be random. In other words, no program shorter than <span class="math-container">$n$</span> prints <span class="math-container">$x$</span>. Combined this implies that <span class="math-container">$O(\log n) + c + O(1) \ge n$</span> and this implies that <span class="math-container">$n$</span> is bounded by a constant. In conclusion, if the statement &quot;<span class="math-container">$x$</span> is random&quot; is provable, then the length of <span class="math-container">$x$</span> must be bounded by a constant.</p>
<p>Although it is not important for the above argument, let us anyway talk about the function CORR, which checks whether a statement <span class="math-container">$s$</span> and a proof <span class="math-container">$p$</span> in <span class="math-container">$F$</span> 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 <span class="math-container">$f$</span> in the above argument.</p>
<p>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 &quot;<span class="math-container">$x$</span> is random&quot; are not provable whenever <span class="math-container">$x$</span> is large. Now we explain that F can not declare all statements &quot;x is random&quot; to be false for large x, because this would violate the pigeon whole principle (there are <span class="math-container">$2^n$</span> strings of length <span class="math-container">$n$</span>, but the number of strings of length less than <span class="math-container">$n$</span> equals <span class="math-container">$1 + 2^1 + ... + 2^{n-1} &lt; 2^n$</span>). Thus if F is sufficiently powerful, it can prove that not all strings of a given length <span class="math-container">$n$</span> are random. On the other hand, if it declares all these strings to be nonrandom, F would be inconsistent, and this contradicts the assumption.</p>

CC BY-SA 4.0
2022-10-22T13:38:04.120Z
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.
Julian Moore
CC BY-SA 4.0
2022-10-22T10:36:30.557Z
2022-10-22T10:36:30.557Z
Bruno Bauwens
<p>(Cross-posted from <a href="https://cs.stackexchange.com/questions/154105/clarification-sought-re-li-vitanyis-proof-of-godel-incompleteness-in-formal-s">Computer Science</a> due to lack of response after 1 week)</p>
<p>From <em>An Introduction to Kolmogorov Complexity and Its Applications</em>, Li &amp; Vitany, 4th Ed. Example 1.1.1.</p>
<p>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.</p>
<p>This example concerns &quot;Godel’s incompleteness result&quot;; 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.</p>
<p>We need first their definition of random, i.e. uncompressible (maximal Kolmogorov complexity)</p>
<blockquote>
<p>We write “x is random” if the shortest binary description of x with
respect to the optimal specification method <span class="math-container">$D_0$</span> has length at least
that of the literal description of x</p>
</blockquote>
<p>The part of the argument I don't follow and would like help understanding occurs in this section:</p>
<blockquote>
<p>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 <span class="math-container">$n \gg f$</span> 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.</p>
</blockquote>
<p><strong>Problem</strong> Given a string of length <em>n</em>, the argument relies on the length of a procedure P with respect to <span class="math-container">$D_0$</span> being given by both</p>
<ul>
<li><span class="math-container">$|P| = log_2(n) + f$</span> (Eq I)</li>
<li><span class="math-container">$|P| &gt; n$</span>, (Eq II) because &quot;x is random&quot; (and strictly &gt; because there must be <em>some</em> instruction to output the &quot;literal  description of x&quot; having length n)</li>
</ul>
<p>We were told that <span class="math-container">$n \gg f$</span>, i.e. <span class="math-container">$f \ll n$</span> and hence necessarily in Eq I that <span class="math-container">$log_2(n) + f &lt; n$</span> (for sufficiently large n), contradicting Eq II.</p>
<p>Which implies that F is not consistent, but ex hypothesis F is sound (i.e. consistent) therefore the assumption that '&quot;x is random&quot; is provable in F' (for arbitrary x) must be false.</p>
<p>However, whilst I have no problem with the statement that formal system F &quot;can be described in f bits&quot;, 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.</p>
<p><strong>Question(s)</strong> 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.</p>

CC BY-SA 4.0
2022-09-20T09:46:06.260Z
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.
Emil Jeřábek
CC BY-SA 4.0
2022-09-20T10:21:09.797Z
@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.
Julian Moore
<turing-machines><kolmogorov-complexity>
Clarification sought re Li & Vitanyi's Proof of Godel Incompleteness in Formal System F
Julian Moore
# Clarification sought re Li & Vitanyi's Proof of Godel Incompleteness in Formal System F

(Asked by: username_0 on 2022-09-19)

(Cross-posted from [Computer Science](https://cs.stackexchange.com/questions/154105/clarification-sought-re-li-vitanyis-proof-of-godel-incompleteness-in-formal-s) 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.

**Tags:** turing-machines, kolmogorov-complexity

> **Comments:**
> **username_1**: 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.  
> **username_0**: @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.  

---

## 1 answers

### Answer by username_2 on 2022-10-22. Score: 1 | Accepted answer

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.

> **Comments:**
> **username_0**: 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.  

---

