The consistency of PA is falsifiable. Can the same be said of its soundness?

Suppose I say: "Here's my attempt to axiomatize the truths of arithmetic of successor, addition and multiplication over the natural numbers", and I start writing down some axioms. And for the sixth axiom I write down

(A6)$\quad\forall x\forall y(x \times Sy = x \times y + y)$

Then you could say "Hold on! That implies $2 \times 2 = 2 \times S1 = 2 \times 1 + 1 = 3$ so something has gone horribly wrong, for it's plain false that $2 \times 2 = 3$! Surely what you meant to write was $\forall x\forall y(x \times Sy = x \times y + x)$."

Now note, would you in this little exchange, be deploying a fancy metatheory? Well, you would just be using some plain old arithmetic (hey, $2 \times 2 \neq 3$) in criticizing my attempt to axiomatize plain old arithmetic! (I suppose, if you really it is must, you can call at least some plain old arithmetic part of our metatheory, i.e. part of the background we have in play as we are trying to build a formalized arithmetic: but then don't build too much into the idea of "metatheory". Nothing fancy is going on.)

Well back to the drawing board. This time, I come up with a better axiomatization, our old friend PA.

Now suppose, just suppose, you could again deduce a sentence $\varphi$ in this new theory which is clearly false as a sentence of plain old arithmetic. Then you would have shown that PA is as bad as my first failed attempt (it isn't a sound axiomatization of arithmetic). And again, you wouldn't be appealing to a fancy metatheory in saying this -- just to arithmetic again. Sure in criticising PA you are appealing to something -- but to nothing other than what PA is trying to axiomatize in the first place.

Of course, few of us think that the supposition is going to get realized, and you get to find a falsehood in PA -- but that's another story!


There is indeed a significant difference between proving a theory is consistent, and proving that all of its theorems are true, which is what the question calls "soundness".

The consistency of a theory is a universal statement that can be concretely disproved by giving a counterexample. Soundness cannot be disproved in that way. The argument that it cannot is necessarily heuristic.

The first key point is that any consistent theory of arithmetic which is sufficiently strong will be sound for atomic sentences - so it will not prove anything like "$2 + 2 = 5$" that could be used to concretely see the theory is unsound. This is because any is strong theory already proves every true atomic sentence, so it can only prove a false one if it is inconsistent.

So if PA is consistent and unsound, the false sentence $\phi$ that it proves would have to involve at least one quantifier. But then, to show PA is unsound, we would have to show that $\phi$ is true. In general, $\phi$ might have a very large number of nested quantifiers; it is known that for each $n$ there is a theory that is unsound but is sound for all formulas that have no more than $n$ quantifiers. So there is no reason to think that the falsity of $\phi$ would be intuitively clear or obvious. In general we would need to give an argument in some (meta)theory that $\phi$ is false.

Wrapping up point 1: if $\phi$ is provable in PA, that can be demonstrated concretely by giving a proof of it in PA. But, to argue PA is unsound, we also need to argue that $\phi$ is false. That additional step is what distinguishes proving unsoundness from merely proving inconsistency.

As a second point: for any sound, effective theory $T$ of arithmetic, the theory $S = T + \lnot \text{Con}(T)$ is also consistent, and is "sound relative to $T$" in the sense that whenever $S$ proves a sentence, $T$ cannot disprove that sentence. So, if we had some effective way of listing all the "obvious" facts about the natural numbers, would could call that $T$, and there would be some other theory $S$ that is unsound although our "obvious" facts cannot verify the unsoundness.

As I said, these two points provide only a heuristic argument, but together they give a lot of evidence that there is no reason to expect that a concrete (finitistic) demonstration of the unsoundness of an unsound theory of arithmetic can always be provided. As usual, we cannot make that statement precise without formalizing the metatheory.


Here are two definitions, as mentioned in the comments.

A first-order theory $T$ is called sound if all the theorems of $T$ are true. Here "true" means "true in the intended interpretation of $T$", which is usually determined from context. For a theory in first-order logic, because the inference rules all preserve truth, soundness of a theory is equivalent to all the axioms of the theory being true in the intended interpretation. This sense of soundness is closely related to the traditional notion of a sound argument: an argument is sound if its form is valid and all of its premises are true. On the other hand one can present valid arguments that use false hypotheses; the difference is that sound arguments establish the truth of their conclusions, while valid arguments may not. Similarly, sound theories establish the truth of their theorems, while unsound theories do not.

Soundness of a logic is a more delicate matter. A general (two-valued) logic has a collection $\mathcal{L}$ of sentences, a collection $\mathcal{D}$ of inference rules, and a collection $\mathcal{I}$ of interpretations, where each interpretation includes a function from $\mathcal{L}$ to $\{T,F\}$ which tells whether each sentence is true or false in that interpretation. The logic $(\mathcal{L}, \mathcal{D}, \mathcal{I})$ is sound if, whenever a sentence $\phi \in \mathcal{L}$ is provable from some set $H$ of hypotheses, then every interpretation in $\mathcal{I}$ that makes every sentence in $H$ true also makes $\phi$ true.

The difference is that a general logic may have no sense of an "intended interpretation", so soundness of a logic merely states that the inference rules preserve truth in all the interpretations in $\mathcal{I}$. But in the case of foundational theories, such as Peano arithmetic, we already have an intended interpretation in mind, and so for soundness of a theory we focus on truth in the intended interpretation rather than truth in all interpretations.