(Very) Large numbers, Chaitin's incompletness theorem and a specific upper bound

Question

Chaitin's incompleteness theorem roughly saying states that for any theory $S$ there exists universal constant $L$ that for any string $\sigma$ one cannot prove (within this theory) that $K(\sigma)>L$ where $K$ is the Kolmogorov complexity. Since this constant is universal I'm very curious

How one can estimate thisconstant for some well known theories (Peano arithmetic is the first one which comes to my mind but the answer would be even more interesting for ZFC)-for example could it be compared with Busy Beaver numbers?

I suspect that in order to say anything about such a constant one has to use some richer theory so for ZFC I would be also interested what axioms do we have to add to $ZFC$?

EDIT: adressing a comment below: I'm not sure whether it is enough but I would like to stick to Turing model of computation: namely fix some universal Turning machine and then ask my questions: please, correct me if it is still not enough information for my question to be well posed

Answer 1

One way to provide an explict bound on $L$ is as follows, using the idea of the universal algorithm.

Namely, for any computably axiomatizable theory $T$ in question, consider the algorithm $p$ that searches for a proof of a statement of the form "sequence $s$ is not the output of program $p$ on empty input," where the sequence is mentioned explicitly in the statement. For the first such sequence found, halt immediately and give that sequence as output.

(One might notice that the program $p$ is defined in a self-referential manner, since $p$ is looking for proofs about itself; but this is no problem at all, and the existence of a program fulfilling this recursive definition follows directly from the Kleene recursion theorem — it's just like creating a Quine program. We can in principle write down $p$ explicitly.)

The crucial feature of this program is the following universality property. Namely, if $T$ is consistent (and let us suppose it includes some very minimal arithmetic theory), then you will not be able to prove of any specific $s$ that it is not the output of this program, for if you could, then the program would indeed find such an $s$ and give it as output. But in this case, the theory would also be able to prove that this $s$ was the output of $p$, since we can easily prove that the output of a halting computation is what it actually happens to be. This would be proving a contradiction.

So you cannot prove of any particular $s$ that it is not the output of $p$. And so it is consistent with the theory for any $s$ that it IS the output of $p$. In other words, for every finite sequence $s$ it is consistent with the theory $T$ that the Kolmogorov complexity of $s$ does not exceed the number of states in $p$.

So the number of states in $p$, which is a program that we can in principle write down explicitly, is an upper bound for the universal constant $L$. Because of this, the number $L$ is not as large as one might have supposed. It is not crazy large like the busy beaver numbers, but rather something approachable.

The bound I provide, estimating very roughly, is probably something less than ten thousand or so, since I would think that we can write the program within that many states. Certainly less than one hundred thousand. (But actually I believe that apart from the universal algorithm, the optimal value of $L$ will be considerably less than this, probably less than one hundred.)

I note also that the bound provided by this argument does not vary much with the strength of the theory, whether PA or ZFC or ZFC + large cardinals, or what have you. Each theory will have a somewhat different program, but the sizes of these programs will be in roughly the same ballpark.