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^*$.