Timothy Chow writes in a MathOverflow answer

[...] here is a classical fact: for any finite subset of the axioms of PA (remember that PA contains an axiom schema and hence has infinitely many axioms), PA can prove that that finite set of axioms is consistent. That sure seems close to proving consistency, doesn't it? After all, if there is an inconsistency in PA, only finitely many axioms will be needed to derive that inconsistency.

What is this result called, and, more broadly, where does one go to get introduction to all these concepts?


1 Answer 1


Let $T \supseteq I \Sigma_1$, we say that $T$ is reflexive if for each finite substheory $T_0$ of $T$, $T$ proves the consistency of $T_0$.

The result is then that $\sf PA$ is (essentially) reflexive. The proof goes through the arithmetization of some of its model theory, particularly partial truth predicates for $\sf PA$.

The standard reference is Hájek P, Pudlák P. Metamathematics of First-Order Arithmetic. Cambridge University Press; 2017, especially Part I.4.

Kaye, Richard, Models of Peano Arithmetic (Oxford, 1991; online edn, Oxford Academic, 31 Oct. 2023) is also a classic with a good amount of details on the arithmetization, Chap 9.


You must log in to answer this question.

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