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.
 A: 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. 
A: 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:


*

*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.

*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.
