Gödel's Second Incompleteness Theorem and Arithmetically Non-Definable Theories

Question

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.

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.