<p>(Note: This answer works for most any consistient theory, not just $ZFC$.)</p>

<p>We will define a machine $p$ based on <a href="http://jdh.hamkins.org/the-universal-algorithm-a-new-simple-proof-of-woodins-theorem/" rel="nofollow noreferrer">the universal algorithm</a>. $p$ does a search, looking for a string that represents a proof of a statement of the form "not ($p$ halts and outputs $n$)" (note that this requires <a href="https://en.wikipedia.org/wiki/Quine_(computing)" rel="nofollow noreferrer">quining</a>, since it is self-referential), for some numeral $n$, such that the proof is valid in ZFC. When it finds such a proof, it outputs $n$.</p>

<p>Lemma: For any numeral $n$, if ZFC is consistient, ZFC does not prove the statement "not ($p$ halts and outputs $n$)".</p>

<p>Assume to the contrary that for some $n$, ZFC proves "not ($p$ halts and outputs $n$)". Then $p$ will find this proof, output $n$, and halt. Moreover, since $p$ must halt in a finite amount of time, we can construct a step by step proof of this in ZFC. That is, we can prove "$p$ halts and outputs $n$" in ZFC. This is a contradiction in ZFC, but ZFC is consistient by assumption. Therefore ZFC does not prove the statement "not ($p$ halts and outputs $n$)" for any numeral $n$.</p>

<p>Now, formalize $p$ into a program $\rho$. Let $$L_\text{ZFC} = |\rho|+1$$ Suppose that $ZFC$ proves for some $s$ that $K(s) \ge L_\text{ZFC} \gt |\rho|$. This implies that the machine that $\rho$ encodes, $p$, does not output $s$. But by the lemma, ZFC can not prove this! Therefore, there is no $s$ such that ZFC proves $$K(s) \ge L_\text{ZFC}$$</p>

<p>Now all that needs to be done is to actually create $\rho$ in some programming language, but we will leave that as an exercise to the programmer.</p>

CC BY-SA 3.0
2017-10-21T12:52:37.330Z
+1: Thanks for the link to the universal algorithm articles!
Stella Biderman
CC BY-SA 3.0
2017-10-20T22:27:09.723Z
2017-10-27T00:52:30.623Z
2017-10-27T00:52:30.623Z
Christopher King
<p><a href="https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin.27s_incompleteness_theorem" rel="noreferrer">Chaitin's incompleteness theorem</a> states for any formal system $F$ (which satisfies various criteria), there is a $L$ such that for any $s$ the statement $$K(s) \ge L_F$$ is unprovable in that formal system. My question is, do we know what that constant is for ZFC. (Note that, like all questions involving Kolmogorov complexity, the specific value depends on the description language, but only up to an additive constant. If you want a specific language, you can use <a href="https://en.wikipedia.org/wiki/Binary_combinatory_logic" rel="noreferrer">Binary combinatory logic</a>, but once you find a $L_{ZFC}$ in one language, its trivial to find it in another.)</p>

<p>Note: I am not asking for the minimum $L_{ZFC}$, just any $L_{ZFC}$. In other words, I'm looking for an upper bound on the minimum $L_{ZFC}$.</p>

<kolmogorov-complexity><upper-bounds><set-theory>
Do we know a specific $L_{ZFC}$ such that $K(s) \ge L_{ZFC}$ is unprovable in ZFC for all strings $s$?
Christopher King
# Do we know a specific $L_{ZFC}$ such that $K(s) \ge L_{ZFC}$ is unprovable in ZFC for all strings $s$?

(Asked by: username_0 on 2017-10-14)

[Chaitin's incompleteness theorem](https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin.27s_incompleteness_theorem) states for any formal system $F$ (which satisfies various criteria), there is a $L$ such that for any $s$ the statement $$K(s) \ge L\_F$$ is unprovable in that formal system. My question is, do we know what that constant is for ZFC. (Note that, like all questions involving Kolmogorov complexity, the specific value depends on the description language, but only up to an additive constant. If you want a specific language, you can use [Binary combinatory logic](https://en.wikipedia.org/wiki/Binary_combinatory_logic), but once you find a $L\_{ZFC}$ in one language, its trivial to find it in another.)

Note: I am not asking for the minimum $L\_{ZFC}$, just any $L\_{ZFC}$. In other words, I'm looking for an upper bound on the minimum $L\_{ZFC}$.

**Tags:** kolmogorov-complexity, upper-bounds, set-theory


---

## 1 answers

### Answer by username_0 on 2017-10-20. Score: 5 | Accepted answer

(Note: This answer works for most any consistient theory, not just $ZFC$.)

We will define a machine $p$ based on [the universal algorithm](http://jdh.hamkins.org/the-universal-algorithm-a-new-simple-proof-of-woodins-theorem/). $p$ does a search, looking for a string that represents a proof of a statement of the form "not ($p$ halts and outputs $n$)" (note that this requires [quining](https://en.wikipedia.org/wiki/Quine_(computing)), since it is self-referential), for some numeral $n$, such that the proof is valid in ZFC. When it finds such a proof, it outputs $n$.

Lemma: For any numeral $n$, if ZFC is consistient, ZFC does not prove the statement "not ($p$ halts and outputs $n$)".

Assume to the contrary that for some $n$, ZFC proves "not ($p$ halts and outputs $n$)". Then $p$ will find this proof, output $n$, and halt. Moreover, since $p$ must halt in a finite amount of time, we can construct a step by step proof of this in ZFC. That is, we can prove "$p$ halts and outputs $n$" in ZFC. This is a contradiction in ZFC, but ZFC is consistient by assumption. Therefore ZFC does not prove the statement "not ($p$ halts and outputs $n$)" for any numeral $n$.

Now, formalize $p$ into a program $\rho$. Let $$L\_\text{ZFC} = |\rho|+1$$ Suppose that $ZFC$ proves for some $s$ that $K(s) \ge L\_\text{ZFC} \gt |\rho|$. This implies that the machine that $\rho$ encodes, $p$, does not output $s$. But by the lemma, ZFC can not prove this! Therefore, there is no $s$ such that ZFC proves $$K(s) \ge L\_\text{ZFC}$$

Now all that needs to be done is to actually create $\rho$ in some programming language, but we will leave that as an exercise to the programmer.

> **Comments:**
> **username_1**: +1: Thanks for the link to the universal algorithm articles!  

---

