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$ Commented Feb 7, 2015 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
    Commented Feb 7, 2015 at 23:24
  • 2
    $\begingroup$ @ThomasAndrews That's not true. $\mathsf{PA}$ can talk about arithmetic sets. $\endgroup$ Commented Feb 7, 2015 at 23:43
  • $\begingroup$ Whoops, yep, brain slip on my part. @AndresCaicedo $\endgroup$ Commented Feb 8, 2015 at 0:06
  • 1
    $\begingroup$ All work and no play make Cai a dull boy. $\endgroup$
    – Asaf Karagila
    Commented Feb 9, 2015 at 20:22

1 Answer 1


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.

  • $\begingroup$ Could you put some brackets in your def'n of T' ? I'm having difficulty parsing it. $\endgroup$ Commented Nov 18, 2015 at 5:08
  • $\begingroup$ I don't get why you claim that $T' ≡ T$. $\endgroup$
    – user21820
    Commented Jan 25, 2019 at 12:36
  • $\begingroup$ @user21820 There's an implicit assumption that $T$ is consistent (so the "$T'=PA$"-case doesn't hold). $\endgroup$ Commented Apr 27, 2020 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
    Commented Apr 27, 2020 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$ Commented Apr 27, 2020 at 18:25

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .