In what sense does the sentence $\operatorname{con}(\mathsf{PA})$ "say" that $\mathsf{PA}$ is consistent?

Question

It seems common amongst logicians to think of "truth" as being relative to a particular structure. Consider, for instance, the first-order theory of groups. The sentence $\forall x\forall y(x\cdot y=y\cdot x)$ is neither provable nor disprovable from the group axioms. However, rather than saying this sentence is neither true nor false, we would simply say that it is true for some groups (namely, the abelian ones), and false for others. The situation seems similar for most set-theoretical issues – for instance, while saying the continuum hypothesis is true without any qualification is clearly controversial, all set theorists can agree that the continuum hypothesis is true in some models of set theory, and not in others.

However, the situation feels a little different when it comes to the question of whether an axiom system is consistent. Here, it seems like there is an "objective" answer to whether a certain axiom system will lead to a contradiction (provided we agree upon the logical axioms, inference rules, and proof procedure) – there either is a finite derivation that leads to a contradiction, or there is not. What I find puzzling, however, is that from a purely formal viewpoint, the arithmetic statement $\operatorname{con}(\mathsf{PA})$ seems no different to other arithmetic statements that are independent of $\mathsf{PA}$. So, following the line of reasoning expressed in the first paragraph, it seems that I should believe that $\mathsf{con}(\mathsf{PA})$ is true in some models of arithmetic, and not in others. This makes me cast doubt about whether $\mathsf{con}(\mathsf{PA})$ "really" says that $\mathsf{PA}$ is consistent – if the latter has an "objective" truth value that doesn't require qualification, then the idea of $\mathsf{con}(\mathsf{PA})$ being true in some models and not in others appears very strange.

So, in light of these objections, what viewpoints do logicians have about the relationship between the assertion that $\mathsf{PA}$ is consistent, and the arithmetic sentence $\mathsf{con}(\mathsf{PA})$?

Answer 1

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

Answer 2

There is really nothing peculiar about Con(PA) in this regard. Let's take a simpler statement, such as $$(\exists x \exists y \exists z : xxx + yyy - zzz = 114) \vee (\exists x \exists y \exists z : xxx - yyy - zzz = 114)$$ Nobody doubts that "114 is the sum of three cubes" has a clear meaning. But does the above formal string—call it $S$—"say" that 114 is the sum of three cubes? For all we know, $S$ could be independent of PA, which would mean that there are some models of PA in which it is true and others in which it is false. But the possibility that $S$ is independent of PA is irrelevant to the question of whether $S$ "correctly expresses" the statement that 114 is the sum of three cubes. For that, what we need is that if someone were to exhibit a PA-proof of $S$, then we would recognize it as yielding a correct mathematical proof that 114 is the sum of three cubes. There is indeed something to be checked here, but it has nothing to do with whether $S$ turns out to be PA-provable or not.

Answer 3

• "So, in light of these objections, what viewpoints do logicians have about the relationship between the assertion that $PA$ is consistent, and the arithmetic sentence $con(PA) $?"

Logicians consider, among other things, notions of representability as possible precisifications of the expressibility relation between metatheory and object theory.

For instance, assuming some (recursive) Gödel numbering, we say that a formula $\varphi(x)$ in the object theory $PA$ weakly represents a metatheoretical property $B$ iff

$B(n)\leftrightarrow PA\vdash \varphi(\bar n)$,

where $\bar n$ is the numeral corresponding to the metatheoretical $n$.

Now, the metatheoretical sentence that $PA$ is consistent is not a metatheoretical property, so we cannot directly apply the above notion to it. However, indirectly, we can formulate some arguments using weak representability:

First argument:

1. The metatheoretical consistency sentence is of the form $B(\bot)$, where $B$ is the metatheoretical property of not being a theorem.
2. The property of not being a theorem is not weakly representable in $PA$, unconditionally with respect to the consistency of $PA$. (Just diagonalize the weakly representable properties).
3. Therefore, the $PA$ sentence $\neg Thm(\ulcorner 0=1\urcorner)$ does not express $B(\bot)$ because $\neg Thm(x)$ does not represent property $B$.

Second argument:

1. The metatheoretical sentence that $PA$ is consistent is a $0$-ary metatheoretical property.
2. Pushing the weak representability notion to the limit, we could say that a $PA$ sentence $\varphi$ weakly represents a $0$-ary property $B$ iff $B\leftrightarrow PA\vdash \varphi$.
3. Therefore, there is no $PA$ sentence weakly representing the $0$-ary property of consistency, for the negation of $B$ implies $PA\vdash\varphi$, for any $\varphi$.

Third argument:

1. Gödel's (meta)theorem implies that $PA\vdash con(PA)$ iff $PA$ is inconsistent.
2. The above equivalence is the exact negation of the limit case of weak representability.
3. Therefore, $con(PA)$ turns weak representability upside down.

With respect to the determinacy of the metatheoretical consistency of $PA$: The usual metatheory cannot define its own truth (Tarski), so doubts about the determinacy of truth value of the metatheoretical statement naturally live in a metametatheory where one can speak about the notion of truth in the metatheory. This means that if one is not willing to move to a metametatheory, then one is adopting the metatheoretical excluded middle as the last word on the topic.

Answer 4

Let's go back to the continuum hypothesis. Some, probably most, people think that it really is objectively true or false, despite having different truth values in different models, because they believe that there is one canonical correct model. While others might say that no model of ZFC has ontological priority, and so the truth value of CH simply depends on the choice of model and there is nothing more to be said.

The situation with Con(PA) is rather similar. Here too most of us think there is one preferred model of PA, and that Con(PA) is objectively true in it. But others (not as many as in the case of set theory, I think, but they do exist) believe there is no canonical model of PA and therefore no objective truth value for Con(PA).

One reason I find the latter view a little weird is that Con(PA) being false in some model of PA means that there does exist a model of PA, which would seem to imply that Con(PA) is objectively true. Part of the problem here is that if all models of PA are equally valid versions of $\mathbb{N}$, then there as far as I can see there is no canonical formal system PA. Because according to nonstandard models of PA there are formulas of nonstandard length and therefore the induction scheme can vary. So I'm personally not sure there is a coherent rendering of the "all models of PA are equally valid" idea.

Answer 5

I am going to answer the question in the title - In what sense does the sentence con(PA) "say" that PA is consistent? - rather than the question in the body. This is not what the OP wants, but I think it's fair.

And the short answer is: con(PA) does not say that PA is consistent. It says less than that and is a weaker statement. This is because the assertion of consistency is the denial that a contradiction is provable, and the provability formula used to define con(PA) makes a stronger assertion than the intuitive notion of provability. That is, the provability formula Prf$(n,m)$ (as say defined in a proof of the Incompleteness Theorem for PA) asserts that there exists some very big numbers $n$ and $m$ where, basically, $n$ has the structure of a formula $\phi$ and $m$ has the structure of a proof of $\phi$. So Prf$(n,m)$ not only makes an assertion about a proof proving a formula, it makes in addition the assertion that some big numbers representing the formula and the proof exist.

You can best see this in a weak arithmetic, which does not assume the Successor Axiom, that every natural number has a successor, which you can call FPA. (See here: Can FPA really prove its consistency?)

In FPA you have the downward property: basically, once you assume or have proven a number exists, every number less than that number exists; but you can't assume or prove that bigger numbers exist. con(FPA) denies there exists a really big number which has the structure of the proof of a contradiction. FPA is able to prove this. But it's unknown whether FPA can prove the consistency of FPA, when stated in a more reasonable way. That is, con(FPA) is weaker than the assertion of the consistency of FPA.

Similarly con(PA) is weaker than the assertion of the consistency of PA. Since PA proves that the big numbers do exist, con(PA) is logically equivalent to the consistency of PA, in the framework of PA. But "logically equivalent" is not the same thing as "says the same thing as."