Is there a consistent arithmetically definable extension of PA that proves its own consistency?

The negation would be the obvious generalization of Gödel's second incompleteness from r.e. extensions of PA to any arithmetically definable extension of PA.

I see that there is a complete consistent $\Sigma^0_2$ extension of PA. Said theory therefore contains either the sentence "I am consistent" or "I am inconsistent". However, just because it's consistent and complete doesn't mean it contains the sentence "I am consistent" — it could contain the sentence "I am inconsistent", and remain consistent by being such that any model is a nonstandard model in which there exists a strictly nonstandard proof of its inconsistency

• You might want to check out this post. – Burak Feb 13 '16 at 3:13

Surprisingly, the answer is yes! Well, let me say that the answer is yes for what I find to be a reasonable way to understand what you've asked.

Specifically, what I claim is that if PA is consistent, then there is a consistent theory $T$ in the language of arithmetic with the following properties:

1. The axioms of $T$ are definable in the language of arithmetic.
2. PA proves, of every particular axiom of PA, that it satisfies the defining property of $T$, and so $T$ extends PA.
3. $T$ proves that the set of axioms satisfying that definition forms a consistent theory. In other words, $T$ proves that $T$ is consistent.

In this sense, the theory $T$ is a positive instance of what you request.

But actually, a bit more is true about the theory $T$ I have in mind, and it may lead you to think a little about what exactly you want.

• Actually, PA proves that $T$ is consistent.
• Furthermore, the theory $T$ has exactly the same axioms as PA.

I believe that this was observed first by Feferman: S. Feferman, Arithmetization of metamathematics in a general setting, Fund. Math. 49 (1960-1961), 35--92. (Thanks to Andreas Blass for pointing out the precise reference.)

The idea of the proof is simple. We shall simply describe the axioms of PA in a different way, rather than enumerating them in the usual way. Specifically, let $T$ consist of the usual axioms of PA, added one at a time, except that we add the next axiom only so long as the resulting theory remains consistent.

Since we assumed that PA is consistent, it follows that actually all the axioms of PA will actually satisfy the defining property of $T$, and so PA will be contained in $T$. Furthermore, since PA proves of any particular finite number of axioms of PA that they are consistent, it follows that PA proves that any particular axiom of PA will be in $T$.

Because of how we defined it, however, it is clear that PA and hence also $T$ proves that $T$ is consistent, since if it weren't, there would be a first stage where the inconsistency arises, and then we wouldn't have added the axiom making it inconsistent. Almost by definition, $T$ is consistent, and PA can prove that. So $T$ proves that $T$, as defined by the definition we gave for it, is consistent. So this theory $T$ actually proves its own consistency!

Meanwhile, let me point out that if one makes slightly stronger requirements on what is wanted, then the question has a negative answer, essentially by the usual proof of the second incompleteness theorem:

Theorem. Suppose that $T$ is a arithmetically definable theory extending PA, such that if $\sigma$ is an axiom of $T$, then $T$ proves that $\sigma$ is an axiom of $T$ and furthermore PA proves these things about $T$. If $T$ is consistent, then it does not prove its own consistency.

Proof. By the Gödel fixed-point lemma, let $\psi$ be a sentence for which PA proves $\psi\leftrightarrow\ \not\vdash_T\psi$. Thus, PA proves that $\psi$ asserts its own non-provability in $T$.

I claim, first, that $T$ does not prove $\psi$, since if it did, then since $T$ proves that its actual axioms are indeed axioms, it follows that $T$ would prove that that proof is indeed a proof, and so $T$ would prove that $\psi$ is provable in $T$, a statement which PA and hence $T$ proves is equivalent to $\neg\psi$, and so $T$ would also prove $\neg\psi$, contrary to consistency. So $T$ does not prove $\psi$. And this is precisely what $\psi$ asserts, so $\psi$ is true.

In the previous paragraph, we argued that if $T$ is consistent, then $\psi$ is true. By formalizing that argument in arithmetic, then since we assumed that PA proved our hypotheses on $T$, we see that PA proves that $\text{Con}(T)\to\psi$. So if $T$ were to prove $\text{Con}(T)$, then it would prove $\psi$, contradicting our earlier observation. So $T$ does not prove $\text{Con}(T)$. QED

• What about your first three conditions but we demand that PA prove that PA is contained in T? – Will Sawin Feb 12 '16 at 23:34
• Well, PA does prove that any particular axiom of PA is in T, since PA proves that any particular finite subset of PA is consistent. (But that proof is not uniform, so PA does not prove the universal assertion "PA is contained in T".) – Joel David Hamkins Feb 12 '16 at 23:53
• @JoelDavidHamkins: I guess the whole point of this re-enumeration trick is to make ${Prov}_{T}(\cdot)$ not satisfy the Hilbert-Bernays provability conditions, which is necessary for the second incompleteness theorem as you have shown in the last paragraph. (In particular, $T$ cannot recognize that its axioms are actually axioms.) – Burak Feb 13 '16 at 3:45
• @JoelDavidHamkins Dear Prof. Hamkins, i have proved similar, and a little generalized results at this paper :arxiv.org/abs/1602.02416 – Payam Seraji Feb 15 '16 at 18:03
• I believe the relevant paper by Feferman is "Arithmetization of metamathematics in a general setting" (Fundamenta Mathematicae 49 (35-92). – Andreas Blass Feb 15 '16 at 18:56

I add some history to the Joel's answer and also some generalizations.

A similar example can be found in this article by R. Jeroslow. It is also possible to construct a complete and $\Sigma_2$(in fact $\Delta_2$) definable theory which proves its own consistency, see this aricle of M. Kasa. I have presented another method for constructing such a theory in this paper which also proves this generalization :

For every $n>1$ there is a complete $\Delta_n$-definable theory $T$ which contains PA, "T contains PA" is PA-provable and $T$ proves its own $\Sigma_{n-2}$-soundness.

(note that for $\Sigma_1$-complete theories, $\Sigma_0$-soundness is equivalent to simple consistency).

It is also proved that if the theory $T$ is $\Sigma_n$-definable, $\Sigma_{n-1}$-sound and "T contains PA" is PA-provable, then $T$ can not prove its own $\Sigma_{n-1}$-soundness and it can be seen as a generalization of the second incompleteness theorem.