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.


1 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).

  • $\begingroup$ I am looking at the first edition of Lindstrom from project euclid online. The key fact is as you state sbove, that for a formula $\varphi$ of complexity bounded by $n$, PA proves "$Pr(\varphi) \rightarrow \varphi$". This is fact 11 in the text, stated without proof. I am having trouble seeing why this is true. How do you deal with formulas used in the course of a formal proof of $\varphi$ whose complexity is larger than $n$? Naively we would use induction on the length of the proof and say the last line is "true," but you cannot have a truth definition for unbounded complexity. $\endgroup$
    – mbsq
    Sep 3, 2013 at 17:08
  • 1
    $\begingroup$ You are right, Lindström leaves a bit of background as black boxes. (He calls them facts, but this does not mean they are easy.) For this it may be best to look at Hájek-Pudlák, then. They prove all the relevant details, and end up establishing a bit more, namely that $I\Sigma_{k+1}$ proves the consistency of $I\Sigma_k$. You want to look at the material from I.4.(b) on (where satisfiability is defined). I'll adjust the text to make this explicit. $\endgroup$ Sep 3, 2013 at 17:50
  • 1
    $\begingroup$ (I've made the relevant changes, and added some references and links.) $\endgroup$ Sep 3, 2013 at 18:22
  • $\begingroup$ Below $I\Sigma_0+\mathrm{Exp}$, we enter the realm of self-verifiability. See here and here. $\endgroup$ Sep 3, 2013 at 19:01

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .