My recursion theory knowledge has become a bit rusty, so I will appreciate any corrections for misstatements.

Gödel's incompleteness theorem is often exploited by philosophical discussions which overlook the fact that in order to apply Gödel's theorem, one should have recursive (or recursively enumerable) set of axioms.

Indeed, here is how I think of Gödel's theorems: $Th(\mathbb{N},+,*,0,1)$ has Turing degree $0^{(\omega)}$. Therefore, unless our axiom system is sufficiently complicated, we cannot hope to prove every true statement about the natural numbers since the set of theorems of an axiom set of Turing degree $A$ is recursively enumerable in $A$.

Today, I was having a discussion with a friend about the second incompleteness theorem and I happened to say that it can be violated as long as we keep our axiom set computationally complicated enough. Then, it struck me that I may not be making any sense.

Assume that we pick a complete consistent theory $T$ extending PA in the language of PA, such as $Th(\mathbb{N},+,*,0,1)$. For $T=Th(\mathbb{N},+,*,0,1)$, how can we state that $T$ is consistent?

By Post's theorem, any formula defining a subset of natural numbers in the arithmetical hierarchy will define a subset of Turing degree $\leq 0^{(k)}$ for some $k \in \omega$. But then, this set cannot possibly define $T$ since $0^{(\omega)}$ is not recursively enumerable in $0^{(k)}$. Hence, $T$ cannot be arithmetically definable.

If there is any justice in the world, there should be some way of seeing that true arithmetic "believes" that it is consistent. What is the right way of thinking about this? What is the right interpretation? In particular, is there a way to interpret within $T$ (in the language of PA) the fact that $T$ is consistent .

Basically, my purpose is to come up with a sufficiently strong and computationally complicated theory that can "violate" the second incompleteness theorem. We do not have to work in the language of PA. Jumping to set theories like ZFC is fine as long as it achieves the purpose.

I thought true arithmetic was the most obvious choice but it is not, since it requires $T$ to be arithmetically definable to even write down the statement $Con(T)$. On the other hand, we do not have to stick to $Con()$ to state that a theory is consistent. I am open to any suggestions (like formula schemes etc.) as long as you come up with a reasonable way of saying that $T$ is consistent.

  • $\begingroup$ Well, you can theoretically simply take as your axioms all the true statements in the theory. $\endgroup$ – Thomas Andrews Feb 7 '15 at 23:22
  • $\begingroup$ That is exactly what I am doing. My theory $T$ is the complete theory of natural numbers. How does it believe that it is consistent? It can't seem to state this. $\endgroup$ – Burak Feb 7 '15 at 23:24
  • 2
    $\begingroup$ @ThomasAndrews That's not true. $\mathsf{PA}$ can talk about arithmetic sets. $\endgroup$ – Andrés E. Caicedo Feb 7 '15 at 23:43
  • $\begingroup$ Whoops, yep, brain slip on my part. @AndresCaicedo $\endgroup$ – Thomas Andrews Feb 8 '15 at 0:06
  • 1
    $\begingroup$ All work and no play make Cai a dull boy. $\endgroup$ – Asaf Karagila Feb 9 '15 at 20:22

OK, here is Mingzhong's answer.

$\mathbf{Theorem }$: Let $T$ be a first order definable theory stronger than $PA+Con(PA)$, then there is a theory $T'\equiv T$ so that $T'\vdash Con(T')$.

$\mathbf{Proof}$: Let $T$ be such a theory. Define $T'$ so that $T'=PA$ if $\neg Con(T)$, or $T'=T$ if $Con(T)$.

We prove that $T'\vdash (Con(T)\vee \neg Con(T))\rightarrow Con(T')$ and so $T'\vdash Con(T')$. Note that $T'\equiv T\vdash Con(PA)$.

$T'\vdash Con(T)\rightarrow T=T'$ and so $T'\vdash Con(T)\rightarrow Con(T')$.

$T'\vdash\neg Con(T)\rightarrow T'=PA$. But $T'\vdash Con(PA)$, so $T'\vdash \neg Con(T)\rightarrow Con(T')$. QED

Note that $T'$ cannot "recognize" this proof. In other words, usually $T'\not\vdash Prb_{T'}(Con(T'))$. Some additional effort are needed to prove this, but not quite difficult.

| cite | improve this answer | |
  • $\begingroup$ Could you put some brackets in your def'n of T' ? I'm having difficulty parsing it. $\endgroup$ – DanielWainfleet Nov 18 '15 at 5:08
  • $\begingroup$ I don't get why you claim that $T' ≡ T$. $\endgroup$ – user21820 Jan 25 '19 at 12:36
  • $\begingroup$ @user21820 There's an implicit assumption that $T$ is consistent (so the "$T'=PA$"-case doesn't hold). $\endgroup$ – Noah Schweber Apr 27 at 17:59
  • $\begingroup$ @NoahSchweber: I still don't get it; what's the point of mentioning a case that is assumed never to hold? Can you write an answer? $\endgroup$ – user21820 Apr 27 at 18:23
  • $\begingroup$ @user21820 I'm not sure I understand your question. $T'$ doesn't know that $T$ is consistent, so within $T'$ we're not assuming that the case $\neg Con(T)$ holds. Basically, the point is: "Suppose $T$ is as required and consistent. Then the corresponding arithmetically-defined $T'$ proves $Con(T')$ and is equivalent to $T$." $\endgroup$ – Noah Schweber Apr 27 at 18:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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