It is "well-known" (e.g. stated [here](https://math.stackexchange.com/a/56117/27659) without proof and sketched [here](https://math.stackexchange.com/a/123660/27659)) 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?



How does one prove the consistency of $\mathrm{PA}$ in $\mathrm{Z_2}$?
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.)


