# Is there a sentence in the language of $\mathrm{PA}$ asserting that $\mathrm{PA}$ is sound?

We often write $\mathrm{Con}(\mathrm{PA})$ for the sentence (in the language of $\mathrm{PA}$) asserting that $\mathrm{PA}$ is consistent. Is there a sentence $\mathrm{Sou}(\mathrm{PA})$ (in the language of $\mathrm{PA}$) asserting that $\mathrm{PA}$ is sound? I'm thinking that the existence of such a sentence might run afoul of Tarski's undefinability theorem.

• If $\sf PA$ is sound, how come we can't hear it? :-) – Asaf Karagila Apr 29 '13 at 9:29
• Doesn't soundness imply consistency? If PA proves only true sentences (i.e. is sound), then in particular it doesn't prove $\bot$ and is thus consistent, no? – fgp Apr 29 '13 at 9:33
• @fgp, yes; and thus we'd expect that PA cannot prove Sou(PA), if such a sentence even exists. – goblin Apr 29 '13 at 10:51
• Can you tell us what is the sentence "Sou(PA)"? I can see how to write down a sentence which expresses "there is no (finite) proof ...", i.e., expresses "PA is consistent". On the other hand I do not see how to write down a sentence (in the Peano language) that expresses "there is a (infinite) first-order structure ...". This trouble would not appear if one wants to write a sentence in the ZFC language saying that "PA is sound", this can be clearly done. – boumol Apr 29 '13 at 11:04
• @fgp I don't see it. Soundness says that if a sentence is provable then it is true in every model. If a theory has no models, anything can be proved, including $\bot$, and the theory is still being sound. – Anguepa Feb 8 '15 at 11:44

The closest thing that is well-studied is the reflection scheme, which in the case of Peano Arithmetic includes each formula of the form $$\text{Pvbl}_{\text{PA}}(\phi) \to \phi.$$ This scheme says that each provable sentence is true, and thus could be viewed as a soundness scheme.

The reflection scheme is not provable, in general, in Peano arithmetic. Löb's theorem can be phrased as: if the instance of the reflection scheme for a sentence $\phi$ is provable in PA, then $\phi$ is already provable in PA. Thus there are many instances of the reflection scheme that are not provable in PA. The reflection scheme is consistent with PA, however, because it is satisfied by the standard model.

One place to start looking at information on this scheme is Smorynski's article in the Handbook of Mathmatical Logic.

• Good answer! I'm going to check out that reference. A couple of quick questions. 1) is this schema stronger than the corresponding consistency statement? And 2) is the schema $\mathrm{Pvbl}_{\mathrm{PA}+\neg \mathrm{Con(PA)}}(\phi)\rightarrow\phi$ consistent with $\mathrm{PA}+\neg \mathrm{Con(PA)}$? Anyway, thank you for the reference. – goblin Apr 29 '13 at 12:00
• The reflection scheme is not consistent with $T = PA + \lnot \text{Con}(\text{PA})$. $T$ proves $\text{Pvbl}_\text{PA}(\ulcorner 0=1 \urcorner)$, but $T$ also includes an axiom to the effect of $0 \not = 1$. – Carl Mummert Apr 29 '13 at 12:46
• PA + reflection for $\Pi_1$ sentences is equivalent to PA + Con. – Peter Smith Apr 29 '13 at 13:18
• This deserved acceptance a long time ago. Sorry about that. – goblin Feb 8 '15 at 12:22

I think the main issue with this question is that it's not clear what it means to assert the soundness of $\mathrm{PA}$. For instance, $\mathrm{Sou(PA)}$ is true, so it is equivalent to, say $0 = 0$. To some extent the same issue comes up with $\mathrm{Con(PA)}$, but in the case we have the following two points:

1. We can write down explicitly what $\mathrm{Con(PA)}$ should be, so even if we don't know what it means in general to assert the consistency of $\mathrm{PA}$ we at least have an example of one sentence that does so.

2. We can write down a formula with one free variable $\mathrm{Con}(x)$ such that for any recursively axiomatizable theory $T$, if $\ulcorner T \urcorner$ is a Gödelnumber for $T$, then $\mathbb{N} \models \mathrm{Con}(\ulcorner T \urcorner)$ if and only if $T$ is consistent.

Clearly 1 is no good in the case of soundness. However, if something like 2 should hold for soundness, then we could use $\mathrm{Sou}(x)$ to define a truth predicate, and yes, this would contradict Tarski's undefinability theorem.

Edit: The reason that this defines a truth predicate is that for any sentence $\phi$, the "singleton" theory $\{\phi\}$ consisting of a single axiom $\phi$ is recursively axiomatizable and $\phi$ is true if and only if $\{\phi\}$ is sound.

• Why? ISTM that Sou(PA) is equivalent to $\textrm{Provable}(x) \implies \textrm{True}(x)$. It might very well be that this is definable, yet plain $\textrm{True}(x)$ is not, no? – fgp Apr 29 '13 at 11:12
• I think the bit just added in the edit should answer your question. – aws Apr 29 '13 at 11:26