How to prove that first-order PA proves the consistency of each of its finite sub-theories?

Question

The locus classicus of this theorem (the ''reflexivity'' of PA) is Mostowski's 1952 On models of axiomatic systems. I freely admit that I can't read the rather archaic formalism of this paper. Is there a more accessible, modern source where this theorem is proven? Or alternatively, does somebody know the proof, and would like to carry it out here? Furthermore, can the theorem be formally reproduced inside PA? I.e., can PA itself verify that it verifies the consistency of each of its finite sub-theories?

Many thanks in advance.

Answer 1

This is a somewhat standard result. One way to approach it is:

• Stratify the induction scheme into a sequence $I\Sigma_n$ of stronger and stronger schemes. For each $n$ the scheme $I\Sigma_n$ includes induction for $\Sigma_n$ formulas only.

• Show that $I\Sigma_{n+1}$ (and thus PA) proves the consistency of $I\Sigma_n$ for each $n \geq 0$. A proof of this is sketched on page 140 of Kaye's Models of Peano Arithmetic. The proof uses a universal $\Sigma_n$ formula, also known as a "truth predicate" or "partial truth predicate". This method is also used to show that each scheme $I\Sigma_n$ is itself finitely axiomatizable, for $n \geq 1$, as sketched by Kaye on p. 134. The construction of a universal $\Sigma_n$ formula is standard, but tedious. Kaye's book has the details.

• Because there are only a finite number of non-induction axioms on PA, every finite subtheory of PA is included in $I\Sigma_n$ for some $n$. Hence PA proves the consistency of each of its finite subtheories.

The overall results

• "for all $n$, $I\Sigma_n$ is consistent" and
• "every finite subtheory of PA is consistent"

cannot be proved in PA, because PA proves "If every finite subtheory of PA is consistent then PA is consistent", because given a derivation of $0=1$ in PA the finite subtheory consisting of only the axioms used in that derivation will also be inconsistent.

Answer 2

A quick comment building on Carl's answer:

While - as Carl says - PA does not prove

$(*)\quad$"For all $n$, $I\Sigma_n$ is consistent,"

I believe PA does indeed prove

$(**)\quad$"For all $n$, PA proves that $I\Sigma_n$ is consistent"

just by checking that the usual proof goes through in PA with a bit of care re: how we talk about models, which PA can't actually directly handle. This is of course a nontrivial task; I'll put in a reference to it when I have time to find it (but see below).

These two facts aren't in contradiction: perhaps surprisingly, theories rarely prove that provability implies truth!

---

Above I kind of punted on the issue of whether $(**)$ is in fact true. It is however quite easy to show that $(**)$ is plausible, as follows:

Define a sequence of theories $(T_i)_{i\in\mathbb{N}}$ recursively as $$T_0=PA, \quad T_{i+1}=T_i\cup\{Con(F): F\subseteq_{fin} T_i\}$$ (where "$X\subseteq_{fin}Y$" means "$X$ is a finite subset of $Y$"). Let $T=\bigcup_{i\in\mathbb{N}}T_i$; then $T$ is recursive and (by induction) sound. But clearly $T$ proves that $T$ proves the consistency of each of its finite subtheories.

• Incidentally, the soundness of $T$ can be proved from the soundness of PA (in an appropriately weak base theory). So the "soundness strength" of $T$ is no greater than that of PA.

So even before we check whether the specific theory PA proves its own reflection, we can quickly show that a theory "very similar" to PA has this property. In particular, no "coarse" argument will show that PA doesn't prove that PA has the reflection property.