13
$\begingroup$

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

$\endgroup$
5
  • 1
    $\begingroup$ This is correct as far as it goes, but of course the additional input ($n$, say) required to check the restriction on the induction schema is of unbounded complexity itself, so it is somewhat misleading to suggest that you've bounded these complexities uniformly. $\endgroup$
    – user30585
    Feb 3, 2015 at 21:36
  • $\begingroup$ The additional complexity would be $log(n)$. If I require $n \le L$ then I would only have to show $L > c+log(L)$. $\endgroup$ Feb 4, 2015 at 2:39
  • $\begingroup$ Your notation somewhat disturbingly reminds me of this incorrect attempt to prove inconsistency of arithmetic. Can you clarify your motivations? $\endgroup$
    – cody
    Feb 4, 2015 at 23:41
  • $\begingroup$ Hi Russell. This sounds pretty interesting to me. If you ever would like to chat, please let me know. Have a nice day! :) $\endgroup$ Feb 7, 2015 at 7:56
  • $\begingroup$ 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. $\endgroup$ Feb 7, 2015 at 20:14

1 Answer 1

5
+50
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ PRA 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)? $\endgroup$ Feb 12, 2015 at 3:35
  • $\begingroup$ 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). $\endgroup$
    – cody
    Feb 12, 2015 at 20:19
  • $\begingroup$ By any sub-theory of $Q^*$ I of course meant any sub-theory which can be proven to be so in PRA. $\endgroup$
    – cody
    Feb 12, 2015 at 20:21
  • $\begingroup$ Hey Cody, thanks for the answer. Hope all is well. :) $\endgroup$ Feb 13, 2015 at 16:58
  • 1
    $\begingroup$ 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... $\endgroup$
    – cody
    Feb 13, 2015 at 19:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.