Requirements for claiming Con(PA) is true

Question

It is well known that the consistency of PA (Peano arithmetic) is not provable in PA, if PA is consistent. More precisely, an arithmetic encoding Con(PA) of the statement "PA is consistent" is not provable in PA, if PA is consistent.

It is often claimed that this is an unprovable but true arithmetic statement.

I'm wondering about what assumptions are needed to make this assertion. Of course, we must assume PA is consistent to begin with. That will be an implicit assumption throughout the rest of this question.

But it also seems possible, at least a priori, that if one's metamathematical assumptions are too weak, then we might not have the ability to even speak (metamathematically) about truth of statements in the base theory. So, my question is simply:

Question: Besides assuming PA+Con(PA), how much more does our metamathematics need in order for us to have the ability to state that Con(PA) is true?

In the book "Inexhaustibility: A non-exhaustive treatment", to prove soundness they needed a system the author called ACA. On pages 148-149, it is asserted that the first order arithmetical consequences of this theory are precisely the same as those we get when adding to PA a (standard) truth predicate, so it seems quite minimal (in some sense) in getting us what we want.

Answer 1

Working in first-order arithmetic, the equivalence between $True_k(\ulcorner\varphi\urcorner)$ and $\varphi$ (for a specific $\varphi\in\Sigma_k$) is fairly uninteresting: it's provable in I$\Sigma_1$ alone. There might be something interesting to be said about the situation below I$\Sigma_1$, but I suspect not - at a glance I think I$\Delta_0$ + Exp is already enough, and we might be able to push it even lower.

The interesting truth notion, as you point out, crops up when we shift to the language of second-order arithmetic, where we can explicitly talk about structures and express "$\mathcal{A}\models\varphi$" (where $\mathcal{A}$ is a structure coded by a real and $\varphi$ is a sentence coded by a number) as a $\Sigma^1_1$ formula in a natural way - more or less, asserting the existence of an appropriate family of Skolem functions (or a realizing tree, or similar).

This brings us to something more relevant to your question. I'll restrict attention to $\mathbb{N}$ for simplicity, although this does generalize to arbitrary structures; I'll also focus on "boldface" rather than "lightface" theories, since the former are more natural, e.g. ACA$_0$ rather than "$0'$ exists" or the scheme "$0^{(n)}$ exists" for each specific $n$:

How do $\varphi$ and $\mathbb{N}\models\varphi$ compare in general?

Well, the latter asserts the existence of Skolem functions witnessing the truth of $\varphi$. Thinking in terms of computability theory, we need $k$-many jumps to build these; this means that for each specific $k$, the theory ACA$_0$ is enough to prove "For each $\varphi\in\Sigma^0_k$, we have $\varphi \iff \mathbb{N}\models\varphi$."

As a first step, along the lines of this complexity analysis ACA$_0$ is enough to show locally that "$\mathbb{N}$ is bivalent" - that is, that for each arithmetic $\varphi$, ACA$_0$ proves that either $\mathbb{N}\models\varphi$ or $\mathbb{N}\models\neg\varphi$. Basically, we turn the intuition that Skolem functions for $\Sigma^0_k$ sentences are uniformly computable from $0^{(k)}$ into an ACA$_0$-argument, for each specific $k$.

The second step global bivalence: the statement "For all arithmetic $\varphi$, either $\mathbb{N}\models\varphi$ or $\mathbb{N}\models\neg\varphi$." Here we need a mild strengthening of ACA$_0$, namely the principle "For each $X$, the $n$th jump of $X$ exists for all finite $n$;" if memory serves, this is called "ACA$_*$."

• Incidentally, ACA$_*$ also proves (for the same reason, and again if memory serves) that PA is arithmetically sound, in the sense that it proves "For all $\varphi\in$ PA, we have $\mathbb{N}\models \varphi$."

The final step is theories: bivalence + "The set of all arithmetic formulas true (in the $\Sigma^1_1$ sense) in $\mathbb{N}$ exists." For this, we want the theory ACA$_0$ + "For each $X$, the $\omega$th jump of $X$ exists," which I believe is called "ACA$_0^+$."

• The $\omega$th jump of a set $X$ is just the set $$\{\langle a,b\rangle\in\mathbb{N}^2: a\in X^{(b)}$\}.$$ More generally, we can iterate the jump along an arbitrary well-ordering of $\mathbb{N}$. Looking at ordinal notations, we can in a precise sense "iterate the jump through the computable ordinals," and this gives rise to the notion of hyperarithmeticity.

  • Incidentally, there's a rare clash here between reverse mathematics and computability theory: Kleene showed that "hyperarithmetic = $\Delta^1_1$," so one might expect that the theory corresponding to a natural principle with "hyperarithmetic solutions" is $\Delta^1_1$-CA$_0$, but in general that's too weak and we need ATR$_0$ instead - the issue being that in order to apply Kleene's theorem we need to know that the set we want already exists!

    • A double aside, but hopefully still interesting: another such clash around the same level concerns determinacy principles: computable clopen games always have hyperarithmetic winning strategies while open games don't, but clopen and open determinacy are equivalent (and are each equivalent to ATR$_0$), the culprit being the complexity of clopenness. Things get better when we look higher up the descriptive set theoretic hierarchy; this has been looked at by myself, Sherwood Hachtman, and I believe (although the paper isn't out yet) Kentaro Sato.

---

That said, ACA$_*$ is massive overkill for your specific question: consistency is $\Sigma^0_1$, and RCA$_0$ alone proves the equivalence between $\varphi$ and $\mathbb{N}\models\varphi$ for $\varphi\in\Sigma^0_3$.

• This is easiest to see if we think in terms of computability theory: to give ourselves "full information" about the truth of $\exists x\forall y\exists z(\theta(x,y,z)))$ with $\theta\in\Sigma^0_0$, we just need to know an appropriate value for $x$ (which is finitely much data); from such an $x$, for each $y$ we can find the appropriate $z$ by brute-force search. Conversely, it's not hard to show that this equivalence breaks down for $\Pi^0_3$ sentences in general - consider for instance the statement "For every Turing machine $\Phi$, there is some $n$ such that if $\Phi$ halts, it halts by stage $n$."

So in your specific case, ACA$_0$ + Con(PA) is sufficient. And this is conservative over PA + Con(PA), so - modulo the language issue - I claim that PA + Con(PA) is already sufficient.

---

There's another aspect of arithmetic truth (in an informal sense) here, however, which - while not relevant to your question - I think you'll find interesting. Namely, in ACA$_0$ we have a distinguished model of PA (namely, the first-order part of our universe); in what sense does this deserve the term "the standard model?" This question has a couple different answers, depending on how we interpret it:

• RCA$_0$ is already enough to show that $\mathbb{N}$ is a minimal model of $P^-$ - that is, that $\mathbb{N}$ has a unique initial segment embedding into every discrete ordered semiring. The first step is local: we prove existence via I$\Sigma^0_1$, and uniqueness via I$\Pi_1^0$, of - for each $n$ - an initial segment embedding of $[0,n]$ into an arbitrary model of $P^-$. Since I$\Pi^0_1$ is provable in I$\Sigma^0_1$ (this isn't trivial), the above goes through in RCA$_0$, and "patching the local embeddings" requires only $\Sigma^0_0$-comprehension.

• But is $\mathbb{N}$ the only (up to isomorphism) minimal model of $P^-$? Well, ACA$_0$ does the job very nicely. Suppose $M$ is another minimal model of $P^-$, and let $f:\mathbb{N}\rightarrow M$ and $g: M\rightarrow\mathbb{N}$ be the corresponding unique initial segment embeddings. If $f$ is surjective then $\mathbb{N}\cong M$; otherwise, let $N=im(f)$. By assumption, there is an initial segment embedding $h$ of $M$ into $N$. But then there are at least two initial segment embeddings of $M$ into itself, namely $h$ and the identity. All I seem to be able to get from RCA$_0$, on the other hand, is that any other minimal model of $P^-$ has an externally (that is, in our model of RCA$_0$, not in $M$ itself) $\Sigma^0_1$-definable descending sequence. But I don't see how to get a contradiction from this. In fact, since this descending sequence isn't a priori definable in $M$, I don't even see how to conclude that this $M$ doesn't satisfy each individual axiom of PA. So perhaps ACA$_0$ is the "right" theory here.

• And Simpson and Yokoyama took yet a third perspective: they focused on "Peano systems," that is, sets equipped with a zero element and a successor operation satisfying the obvious axioms such that every inductive set is the whole thing, and the principle that every Peano system is isomorphic to the naturals. This principle is equivalent, over RCA$_0$ (and indeed the weaker theory RCA$_0^*$, whose first-order part is I$\Delta_0$ + Exp if memory serves), to WKL$_0$.

---

Based on this, I think the conclusion at this point is:

The theory ACA$_0^+$ suffices to develop the "right" basic theory of satisfaction; moreover, even less is required to show that $\mathbb{N}$ deserves the term "the standard model of $P^-$" in various senses (and in ACA$_0$ we can replace $P^-$ with PA, of course). So in general, ACA$_0^+$ is the right theory to develop arithmetic truth. In the specific case of Con(PA), however, RCA$_0$ is already enough.