**The PA sentence “$\newcommand{\Con}{\text{Con}}\Con(\newcommand{\PA}{\text{PA}}\PA)$” says that PA is consistent in exactly the same ways that the PA sentences representing, say, the fundamental theorem of arithmetic, or Goldbach’s conjecture, express the ordinary versions of those statements.**

There are a couple of main senses in which these formal sentences sentences represent their ordinary versions. The first is that if you believe the set of natural numbers exists (which I think most of us do, outside extremely skeptical or contrarian moods), then you can interpret PA in the set of natural numbers — this is the “standard model” — and then you can show (fairly straightforwardly) that the standard interpretation of each of these PA-sentences is equivalent to the statement it was meant to represent — that, say, the PA version of FLT holds under the standard interpretation if and only if FLT actually holds. This is a precise mathematical claim, and if you want you can make it fully formal in ZFC, Martin-Löf Type Theory, or your other favourite foundation: ZFC/MLTT/etc proves “FLT is equivalent to the standard interpretation of the PA-encoding of FLT”. The standard model is just that — giving the symbols of PA their standard reading, and so interpreting its sentences as statements about actual natural numbers and finite objects.

The second sense is less mathematical, but perhaps more fundamental. If you believe that formalised logic reflects everyday mathematical reasoning at all, then you must start at some point by simply *recognising* that when concepts/terms/statements in a formal language represent statements of your everyday mathematical language — just like how if you think that the natural numbers represent anything about finite collections in the real world, you must be willing to recognise that e.g. the number 3 counts this row of dots: [•••]. This inherently isn’t a mathematical claim — it’s the step of connecting your mathematics to something outside it. It may well be supported in part by mathematical reasoning, e.g. to count 5 crates of 24 egg-boxes, and conclude after a few moments’ thought that you have 720 eggs — but at base, it’s a non-mathematical act, recognising that some natural number counts some real-world collection. In the same way, you can look at the PA-sentence “$\forall x y,\ x\cdot y = y \cdot x$” and immediately recognise that it expresses the commutativity of addition; and with a bit more thought (a mixture of mathematical reasoning and non-mathematical “recognition”), you can do the same for the PA-sentences expressing Goldbach’s conjecture, FLT, or the consistency of PA.

(This has significant overlap with my older answer to a similar question; Timothy Chow’s answer there is also very relevant.)

Finally, the existence of non-standard models of PA doesn’t affect any of this. If you replace PA with a smaller theory — say, just the semiring axioms — then this is clear and familiar: the statement “$\exists x, (x \neq 0 \land x\cdot x = 0)$” holds in some rings, so we could say “nilpotent numbers exist in some non-standard models of the semiring axioms”, but that doesn’t make us worry that an actual nilpotent natural number exists, it just shows nilpotents are compatible with a certain few properties of $\mathbb{N}$. Similarly, a non-standard model of PA is just a structure sharing rather more properties with $\mathbb{N}$; its elements can be viewed as “nonstandard numbers” and (via coding) represent things we might call “nonstandard lists”, “nonstandard syntax-/proof-trees”, and so on. If $\Con(\PA)$ fails in such a structure, that means there’s some “nonstandard proof of a contradiction from PA” inside it — but that has no bearing on the existence of an actual such proof.

(With a little more inspection of a nonstandard model, you can see that its “nonstandard numbers” can always be externalised to certain total orders, in general infinite and ill-founded; its “nonstandard sequences” will yield sequences of nonstandard numbers of nonstandard length; its “nonstandard formulas”, similarly, externalise to certain potentially-ill-founded syntax trees, where each node is marked with a logical symbol in the normal way. Finally, a “non-standard proof” will externalise to a tree of such non-standard formulas, in which each node is a legitimate deduction step between such formulas; but both the tree as a whole and the formulas it contains may be ill-founded, and hence need it not represent any actual proof.)

15more comments