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

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.


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.