consistency strength of PA

Question

Why does PA prove the syntactic consistency of its finite subtheories? Please try to give a self-contained explanation (or good outline), or point me to a reference with a good explanation. Thanks.

Answer 1

This is a good question, because a priori $\mathsf{PA}$ lacks the flexibility of $\mathsf{ZFC}$ that allows us to deal with consistency problems semantically (by building models) and, anyway, the obvious model of most subtheories of $\mathsf{PA}$ is just the standard model.

The way this is done in the context of $\mathsf{ZFC}$ is using the reflection theorem: We show that for any finite subtheory $T$ of $\mathsf{ZFC}$ there is an $\alpha$ such that the level $V_\alpha$ of the cumulative hierarchy is a model of $T$. Accordingly, we say that $\mathsf{PA}$ is essentially reflexive, because it proves, for any finite subtheory $T$, the theory $\mathrm{Ref}_T$ consisting of all formulas of the form $\mathrm{Prov}_T(\varphi)\to\varphi$ for $\varphi\in T$. Here $\mathrm{Prov}_T(\psi)$ is the formalization of the statement that $\psi$ is provable in $T$. Hence, $\mathrm{Ref}_T$ can be seen as stating that anything provable in $T$ is true. (And the same holds not just for $\mathsf{PA}$, but for any extension of it.)

The point is that, as in the setting of set theory, reflection gives us consistency: For any recursive $T$ (in the language of arithmetic), we have that $\mathsf{PA}+\mathrm{Ref}_T$ proves $\mathsf{Con}(T)$, the formal statement asserting the consistency of $T$ (say, that $T$ does not prove $0=1$).

In fact, more is true. Via universal formulas, we can prove that $\mathsf{PA}$ establishes the consistency of $I\Sigma_n$ for all $n$, where $I\Sigma_n$ is the fragment of $\mathsf{PA}$ where the schema of induction is restricted to $\Sigma^0_n$ statements. In fact, $I\Sigma_{n+1}$ proves the consistency of $I\Sigma_n$.

An excellent reference for these results and generalizations is

Per Lindström. Aspects of incompleteness. Second edition. Lecture Notes in Logic, 10. Association for Symbolic Logic, Urbana, IL; A K Peters, Ltd., Natick, MA, 2003. MR2014250 (2004i:03095).

Specifically, Chapter 4 deals with reflection principles in general, though already Chapter 1 has sketched that $\mathsf{PA}$ is essentially reflexive. The problem is that Lindström assumes a strong background from the reader, and in order to get quickly to were he wants to start, he leaves unproved some of these "preliminaries". In particular, the key Fact 11 that gives us reflexivity is offered without proof. This result is due to

Georg Kreisel, and Hao Wang. Some applications of formalized consistency proofs, Fund. Math., 42 (1), (1955), 101–110. MR0073539 (17,447g).

Two other essential references for these matters are

Petr Hájek, and Pavel Pudlák. Metamathematics of first-order arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1993. MR1219738 (94d:03001),

and (though its emphasis is on other matters)

Richard Kaye. Models of Peano arithmetic. Oxford Logic Guides, 15. Oxford Science Publications. The Clarendon Press, Oxford University Press, New York, 1991. MR1098499 (92k:03034).

The Hájek-Pudlák book provides full details. See in particular I.4.(b) (where "satisfiability" is formalized) and subsequent sections. Their approach at this stage is syntactic.

Kaye's book does not quite give a full proof. One can show that $\mathsf{ACA}_0$, a subsystem of second order arithmetic, is conservative over $\mathsf{PA}$ for arithmetic statements (and both theories are equiconsistent). This is provable in $\mathsf{PA}$, and allows us to argue "semantically" in $\mathsf{PA}$ since $\mathsf{ACA}_0$ suffices to prove some versions of the completeness theorem. This can be used to formalize in $\mathsf{PA}$ the model theoretic arguments in Kaye's book, and hence show that $\mathsf{PA}+\mathrm{Con}(I\Sigma_1)$ proves $\mathrm{Con}(I\Sigma_n)$ for all $n$; at the moment I do not see how to adapt directly Kaye's methods to also show the consistency of $\mathrm{Con}(I\Sigma_1)$ in $\mathsf{PA}$. But Hájek-Pudlák includes all of this.

Note that some care is needed at the beginning, since our weak theories ought to be able to carry out all relevant recursive arguments via coding. In particular, although $I\Sigma_1$ proves the consistency of $I\Sigma_0$, we have that $I\Sigma_0+\mathrm{Exp}$ does not even prove the consistency of Robinson's $Q$. Here, $\mathrm{Exp}$ is the formula stating that exponentiation is total (and $I\Sigma_0+\mathrm{Exp}$ is essentially the first natural system where we can comfortably express elementary number theory and carry out basic coding arguments). For this, see

Alex J. Wilkie, and Jeff B. Paris. On the scheme of induction for bounded arithmetic formulas, Ann. Pure Appl. Logic, 35 (3), (1987), 261–302. MR0904326 (89g:03087).