How does one prove the consistency of $\mathrm{PA}$ in $\mathrm{Z_2}$?

Question

It is "well-known" (e.g. stated here without proof and sketched here) that $\mathrm{Z_2}$ proves $\mathrm{Con(PA)}$ using the "usual" model-theoretic proof, that is one can build a notion of model $\mathbb{N}$ and satisfaction $\models$ such that $\mathrm{Z_2}$ proves $\mathbb{N}\models\mathrm{PA}$.

I'm struggling to reproduce the proof, with the main difficulty being defining the satisfaction relation $\models$; the issue being how to define it so that for any (code) of a predicate $\phi\rightarrow\psi$, one has $$\mathbb{N}\models \phi\rightarrow\psi\quad \mbox{iff}\quad \mathbb{N}\models\phi\ \mbox{implies}\ \mathbb{N}\models\psi $$ which must use the fact that $\phi$ and $\psi$ are structurally smaller than $\phi\rightarrow\psi$.

Does anyone know a detailed reference for this folklore result?

Answer 1

I don't know a detailed reference, but here's a more detailed proof sketch.

The key point is that the "naive" understanding of $\models$ admits a $\Sigma^1_1$ definition, which $\mathsf{Z_2}$ can unproblematically implement. (There are various ways to sharpen this of course.)

One way to do this is via Skolemization: given a first-order-arithmetic sentence $\varphi$ in prenex normal form, let $\hat{\varphi}$ be its Skolemization. This $\hat{\varphi}$ has the form $\exists \overline{F}\forall\overline{x}\theta$ for some tuple of function symbols $\overline{F}$, some tuple of variables $\overline{x}$, and some first-order quantifier-free formula $\theta$ in the language of arithmetic + the $\overline{F}$s. The transition from $\varphi$ to $\hat{\varphi}$ is appropriately simple, and the property "The tuple of functions $\overline{f}$ witness $\hat{\varphi}$ in $\mathbb{N}$" is expressible by a universal formula in the language of $\mathsf{Z}_2$, so we get the desired $\Sigma^1_1$ definition.

(Another approach, which I actually prefer since for more complicated structures than $\mathbb{N}$ it avoids choice, is via trees. Basically, each $\varphi$ has a corresponding "big syntax tree" $T_\varphi$, with the truth of $\varphi$ in $\mathbb{N}$ corresponding to the existence of a subtree of $T_\varphi$ satisfying a certain $\Pi^0_1$ property. Again, we get a $\Sigma^1_1$ definition. Here the syntactic structure of $\varphi$ is more visible: it corresponds roughly to the height of $T_\varphi$. For example, if $\varphi\equiv \theta\vee\psi$ - and re: your quesiton, note that implications are just disjunctions in classical logic - then $T_\varphi$ consists of a root node labelled "$\vee$," copy of $T_\theta$ on the "left" of the root, and a copy of $T_\psi$ on the "right" of the root.)

Call this $\Sigma^1_1$ property "witnessability." We can prove in $\mathsf{RCA_0}$ alone that for every sentence $\varphi$ at most one of $\varphi$ and $\neg\varphi$ is witnessable, and that the inference rules of first-order logic preserve witnessability. More substantively, we can prove in $\mathsf{RCA_0}$ + "For all sets $A$ and numbers $n$, the $n$th jump of $A$ exists" (this is actually a bit stronger than $\mathsf{ACA_0}$) that each $\mathsf{PA}$-axiom is witnessable and that if $\varphi$ is not witnessable then $\neg\varphi$ is. Finally, using $\Sigma^1_1$ comprehension you can prove that the set of witnessable sentences exists, and thus we have a negation-complete consistent theory extending $\mathsf{PA}$, so $\mathsf{PA}$ is consistent.

(In fact, the appeal to $\Sigma^1_1$ comprehension is totally unnecessary here, but I think it helps make things more intuitive.)

Answer 2

$\let\eq\leftrightarrow\def\p#1{\langle#1\rangle}$Fix a Gödel numbering of formulas such that a subformula of $\phi$ has a smaller number than $\phi$. Let a truth predicate up to $n$ be a set $T$ of tuples $\p{\phi,\vec a}$, where $\phi$ is a formula of PA, and $\vec a$ an assignment to its free variables, which satisfies the usual Tarski definition for formulas $\phi\le n$:

• If $\phi\le n$ is of the form $t=s$ for some terms $t$ and $s$, then $\forall\vec a\,(\p{\phi,\vec a}\in T\eq t(\vec a)=s(\vec a))$. (So you need an evaluation function for terms here. I leave this to the reader.)

• If $\phi\le n$ has the form $\psi\land\chi$, then $\forall\vec a\,(\p{\phi,\vec a}\in T\eq\p{\psi,\vec a}\in T\land\p{\chi,\vec a}\in T)$, and similarly for $\lor$, $\to$, $\neg$.

• If $\phi\le n$ has the form $\exists x_i\,\psi$, then $\forall\vec a\,(\p{\phi,\vec a}\in T\eq\exists b\,\p{\psi,\vec a[i\mapsto b]}\in T)$, where $\vec a[i\mapsto b]$ is the sequence that differs from $\vec a$ such that the $i$th element is $b$, and similarly for $\forall x_i\,\psi$.

These conditions can be written as a $\Delta^1_0$ formula $\def\trp{\mathrm{TrPred}}\trp(T,n)$.

$\def\aca{\mathrm{ACA}_0}\aca$ proves $\exists T\,\trp(T,n)\to\exists T\,\trp(T,n+1)$: if $\trp(T,n)$, and, say, $n+1$ is the Gödel number of $\phi=\exists x_i\,\psi$, then $\trp(T',n+1)$, where $$T'=\{\p{x,\vec y}\in T:x\le n\}\cup\{\p{n+1,\vec a}:\exists b\,\p{\psi,\vec a[i\mapsto b]}\in T\}.$$

Thus, $\aca+\Sigma^1_1$-induction proves $\forall n\,\exists T\,\trp(T,n)$.

Now, given a PA-proof $\phi_0,\dots,\phi_s$, let $n$ be larger than the Gödel numbers of all $\phi_i$, and let $T$ satisfy $\trp(T,n)$. Then prove by induction on $i$ that $\forall\vec a\,\p{\phi_i,\vec a}\in T$. But if $\phi_s$ is a simple contradiction such as $0\ne0$, the definition of $\trp$ implies $\p{\phi_s,\varnothing}\notin T$. This is a contradiction. Thus, $\aca+\Sigma^1_1$-induction proves the consistency of PA.

You can easily upgrade this to a bona fide satisfaction predicate $\models$ for all formulas: you can prove by induction that any two truth predicates up to $n$ agree an all formulas $\phi\le n$, and then you can define $$\mathbb N\models\phi[\vec a]\iff\exists T,n\,(n\ge\phi\land\trp(T,n)\land\p{\phi,\vec a}\in T),$$ which is, due to uniqueness of the truth predicates, equivalent to $$\mathbb N\models\phi[\vec a]\iff\forall T,n\,(n\ge\phi\land\trp(T,n)\to\p{\phi,\vec a}\in T),$$ and satisfies the Tarski definition for all formulas, provably in $\aca+\Sigma^1_1$-induction. (If you want $\models$ to exist as a set, use $\Delta^1_1$-comprehension on top of this.)