Comparing the Kolmogorov complexity of theories

Question

Chaitin's incompleteness theorem says no sufficiently strong theory of arithmetic can prove $K(s) > L$ where $K(s)$ is the Kolmogorov complexity of string $s$ and $L$ is a sufficiently large constant. $L$ is sufficiently large if it is larger than the size in bits of a proof checking machine (PCM). A PCM for theory $T$ takes a string encoded as an integer as input and outputs a 1 if the string is a valid proof in the language of $T$.

Assume that $L(T) > |PCM_T|$ for theory $T$ is an upper bound for the complexity of $T$. Consider the following hierarchy of theories: Let the base theory be Robinson arithmetic ($Q$). Augment $Q$ with increasingly stronger axioms of polynomial bounded induction. Let $Q^*$ be the theory of theorems provable with $Q$ and any of these bounded induction axioms. Assume we can define $L(Q)$ and $L({Q^*})$ by defining PCM's for each theory.

I want to consider an enhanced proof checking machine (EPCM) for $Q^*$. This EPCM takes a string as input just like an ECM and has a second input which defines the rank and level of a sub-theory of $Q^*$. If the input string is a valid proof in $Q^*$ the EPCM then goes through the steps of the proof to determine the highest rank and level of induction used. This EPCM then writes a 1 if the input sentence is a valid proof in the specified sub-theory of $Q^*$.

Is the enhanced proof checker I describe feasible? If so, would the size of this EPCM be an upper bound not just for the complexity of $Q^*$, but also an upper bound on the complexity of any sub-theory of $Q^*$?

Is it reasonable to say there is a constant upper bound on the complexity of $Q^*$ and all of its sub-theories?

---

This question was inpired by Nelson's failed proof of the inconsistency of arithmetic. I didn't point this out earlier because some people find that proof disturbing. My motivation is to ask an interesting question. CSTheory seems to be the right forum for this question. The complexity of $Q^*$ and all of its sub-theories is either bounded by a constant or unbounded. Either answer leads to more questions.

If the complexity of the sub-theories is unbounded we can ask questions like what is the weakest sub-theory of $Q^*$ more complex than $Q^*$? Or more complex than PA and ZFC? Thinking about this question has already shown me there is a severe limit on how much a theory can prove about the Kolmogorov complexity of strings. If $Q^*$ is consistent then none of its sub-theories can prove $K(s) > L(Q^*)$ for any string. This means even really strong sub-theories can't prove there are more complex strings than some much weaker sub-theory where the weaker theory is more complex than $Q^*$.

Answer 1

I'll try and give an answer to this question, and try to clear up some confusion as to the exact form of the question.

The first point I want to make: the $L$ in the statement of Chaitin's constant is indeed a function of $T$. In the absolute sense, it is monotonic in the expressiveness of $T$: if $L(T)$ is the smallest natural number for which $$T\not\vdash K(s)\geq L(T)$$ for any string $s$, then if $T'$ is a consistent theory stronger than $T$ ($T\vdash\varphi$ implies $T'\vdash\varphi$ for any arithmetic sentence $\varphi$) then $L(T')\geq L(T)$. The argument is very simple: if there exists $s$ such that $T\vdash K(s)\geq L$ then $T'\vdash K(s)\geq L$ by hypothesis.

However, this is only true if $L(T)$ is the absolute Chaitin constant. In particular, if $T'$ proves $\mathrm{Con}(T)$, then $$ T'\vdash \exists L\forall s\ \lceil T\not\vdash K(\overline{s})\geq \overline{L}\rceil $$

by internalizing Chaitin's argument. However, a concrete $l$ for which

$$ T'\vdash\forall s\ \lceil T\not\vdash K(\overline{s})\geq\overline{l}\rceil$$

will in general not be equal to $L(T)$. In particular it may be much larger, generally proportional to the size of the proof of $\mathrm{Con}(T)$ in $T'$. This can easily be seen in the proof of the theorem itself, which crucially relies on the consistency of $T$.

So while $Q^*$ can prove consistency of the system with bounded induction, the length of these proofs gets longer the closer you get to $Q^*$ in expressiveness (one way to understand the incompleteness theorems is that the length becomes infinite when you reach $Q^*$, thus it has no finite proof of consistency in $Q^*$ itself). Thus the same applies to the various upper bounds on the internal $L(T)$s $Q^*$ can describe for each sub-theory.

So here is the short answer to your question: $L(T)$ is bounded uniformly for all subtheories of $Q^*$, but $Q^*$ itself cannot show that this bound holds for all such sub-theories. This was the crucial mistake Nelson made (buried under several layers of formalism) and that Tao pointed out here.