Can a finite axiomatization of PA be expressed in a finitely axiomatizable first order set theory?

Question

Peano Arithmetic has an infinite number of axioms because of its induction schema; Likewise $\sf ZFC$ has an infinite number of axioms because of its axiom schema of replacement. $\sf NBG$ however admits a finite axiomatization because of its ontology of classes. Can this class machinery be leveraged to implement a finite axiomatization of $\sf PA$ in first order logic, or does the induction schema require more, like higher order logic?

Answer 1

Yes. There is a theory of second-order arithmetic known as $\mathsf{ACA}_0$ which is to PA just as NBG is to ZFC. $\mathsf{ACA}_0$ is a finitely axiomatizable theory in first-order logic. It has two types of objects: natural numbers and sets of natural numbers (much as NBG has sets and classes of sets).

And it is a conservative extension: the sentences in the original language of Peano arithmetic that are provable in $\mathsf{ACA}_0$ are all provable in PA, just as the sentences in the language of set theory that are provable in NBG are all provable in ZFC.

Moreover, the proofs of conservativity are very similar. In each case one extends a model of the one-sorted theory (PA, ZFC) to a model of the two-sorted theory ($\mathsf{ACA}_0$, NBG) by adding only those new objects (sets of numbers, classes of sets) that are definable over the original model.

Answer 2

See Herbert Enderton, Elements of Set Theory (1977), page 70-on : PEANO'S POSTULATES for a proof of Peano's axioms in $\mathsf {ZFC}$.

In first-order languages, individual variables range over "objects" of the domain of interpretation.

In first-order $\mathsf {PA}$ the "objects" are numbers; thus, we need the axiom schema of induction because in this theory it is not possible to quantify over sets of natural numbers.

In set theory The "objects" are sets, i.e. the individual variables range over sets; thus the induction principle is "naturally" expressible and it is provable from $\mathsf {ZFC}$'s axioms.