Do we know a specific $L_{ZFC}$ such that $K(s) \ge L_{ZFC}$ is unprovable in ZFC for all strings $s$?

Question

Chaitin's 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, 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}$.

Answer 1

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

We will define a machine $p$ based on the universal algorithm. $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, 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.