<p>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.</p>

<p>The first point I want to make: the $L$ in the statement of Chaitin's constant is indeed a function of $T$. In the <strong>absolute</strong> sense, it is monotonic in the expressiveness of $T$: if $L(T)$ is the <strong>smallest</strong> 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.</p>

<p>However, this is only true if $L(T)$ is the <strong>absolute</strong> 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 $$</p>

<p>by internalizing Chaitin's argument. <strong>However</strong>, a <em>concrete</em> $l$ for which</p>

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

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

<p>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 <strong>internal</strong> $L(T)$s $Q^*$ can describe for each sub-theory.</p>

<p>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 <a href="https://golem.ph.utexas.edu/category/2011/09/the_inconsistency_of_arithmeti.html#c039547">here</a>.</p>

CC BY-SA 3.0
2015-02-12T03:35:30.813Z
[PRA](http://en.wikipedia.org/wiki/Primitive_recursive_arithmetic) can prove $Con(Q^*)$. Is the size of this proof an upper bound on the complexity of $Q^*$ and all of it sub-theories (assuming a compatible encoding of axioms, sentences, etc)?
Russell Easterly
CC BY-SA 3.0
2015-02-12T20:19:47.717Z
PRA can give a uniform bound for $L$ for each of the sub-theories. since $\mathrm{PRA}\vdash \mathrm{Con}(Q^*)$ and for any sub-theory $T$ of $Q^*$, $\mathrm{PRA}\vdash\mathrm{Con}(Q^*)\rightarrow\mathrm{Con}(T)$, and so it is not hard to show that the bound for $Q^*$ also works for $T$ (within PRA).
cody
CC BY-SA 3.0
2015-02-12T20:21:25.120Z
By *any* sub-theory of $Q^*$ I of course meant any sub-theory which can be proven to be so in PRA.
cody
CC BY-SA 3.0
2015-02-13T16:58:03.320Z
Hey Cody, thanks for the answer.  Hope all is well.  :)
Michael Wehar
CC BY-SA 3.0
2015-02-13T19:02:40.990Z
Thanks Mike! This was a fun question. The fact Nelson himself got confused in the details suggests that there are some subtle pitfalls along the way...
cody
CC BY-SA 3.0
2015-02-10T22:50:52.077Z
2015-02-10T22:50:52.077Z
cody
<p><a href="http://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin.27s_incompleteness_theorem">Chaitin's incompleteness theorem</a> says no sufficiently strong theory of arithmetic can prove $K(s) &gt; L$ where $K(s)$ is the Kolmogorov complexity of string $s$ and $L$ is a sufficiently large constant. $L$ is <a href="https://golem.ph.utexas.edu/category/2011/09/the_inconsistency_of_arithmeti.html#c039547">sufficiently large</a> 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$.</p>

<p>Assume that $L(T) &gt; |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 <a href="http://en.wikipedia.org/wiki/Robinson_arithmetic">Robinson arithmetic</a> ($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. </p>

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

<p>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^*$? </p>

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

<hr>

<p>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.</p>

<p>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) &gt; 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^*$.</p>

CC BY-SA 3.0
2015-02-04T02:39:43.730Z
The additional complexity would be $log(n)$. If I require $n \le L$ then I would only have to show $L > c+log(L)$.
Russell Easterly
CC BY-SA 3.0
2015-02-04T23:41:56.917Z
Your notation somewhat disturbingly reminds me of [this](https://golem.ph.utexas.edu/category/2011/09/the_inconsistency_of_arithmeti.html) incorrect attempt to prove inconsistency of arithmetic. Can you clarify your motivations?
cody
CC BY-SA 3.0
2015-02-07T07:56:23.413Z
Hi Russell.  This sounds pretty interesting to me.  If you ever would like to chat, please let me know.  Have a nice day!  :)
Michael Wehar
CC BY-SA 3.0
2015-02-07T20:14:29.850Z
Yes, such a TM can be used to define the complexity of a theory. I am asking if there is a bound on the size of this TM when we have multiple theories.
Russell Easterly
<lo.logic><kolmogorov-complexity>
Comparing the Kolmogorov complexity of theories
Russell Easterly
# Comparing the Kolmogorov complexity of theories

(Asked by: username_0 on 2015-02-03)

[Chaitin's incompleteness theorem](http://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin.27s_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](https://golem.ph.utexas.edu/category/2011/09/the_inconsistency_of_arithmeti.html#c039547) 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](http://en.wikipedia.org/wiki/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^\*$.

**Tags:** lo.logic, kolmogorov-complexity
> **Comments:**
> **username_0**: The additional complexity would be $log(n)$. If I require $n \le L$ then I would only have to show $L > c+log(L)$.  
> **username_1**: Your notation somewhat disturbingly reminds me of [this](https://golem.ph.utexas.edu/category/2011/09/the_inconsistency_of_arithmeti.html) incorrect attempt to prove inconsistency of arithmetic. Can you clarify your motivations?  
> **username_2**: Hi Russell.  This sounds pretty interesting to me.  If you ever would like to chat, please let me know.  Have a nice day!  :)  
> **username_0**: Yes, such a TM can be used to define the complexity of a theory. I am asking if there is a bound on the size of this TM when we have multiple theories.  

---

## 1 answers

### Answer by username_1 on 2015-02-10. Score: 5 | Accepted answer

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](https://golem.ph.utexas.edu/category/2011/09/the_inconsistency_of_arithmeti.html#c039547).

> **Comments:**
> **username_0**: [PRA](http://en.wikipedia.org/wiki/Primitive_recursive_arithmetic) can prove $Con(Q^*)$. Is the size of this proof an upper bound on the complexity of $Q^*$ and all of it sub-theories (assuming a compatible encoding of axioms, sentences, etc)?  
> **username_1**: PRA can give a uniform bound for $L$ for each of the sub-theories. since $\mathrm{PRA}\vdash \mathrm{Con}(Q^*)$ and for any sub-theory $T$ of $Q^*$, $\mathrm{PRA}\vdash\mathrm{Con}(Q^*)\rightarrow\mathrm{Con}(T)$, and so it is not hard to show that the bound for $Q^*$ also works for $T$ (within PRA).  
> **username_1**: By *any* sub-theory of $Q^*$ I of course meant any sub-theory which can be proven to be so in PRA.  
> **username_2**: Hey Cody, thanks for the answer.  Hope all is well.  :)  
> **username_1**: Thanks Mike! This was a fun question. The fact Nelson himself got confused in the details suggests that there are some subtle pitfalls along the way...  

---

