The goal of the Hilbert program was to find a complete and consistent formalization of mathematics. Gödel's first incompleteness theorem establishes that completeness is impossible with first-order logic, and the halting problem shows that, more generally, there is no 100% accurate method for solving all mathematical problems.

It is usually regarded that Gödel's second incompleteness theorem means we can't prove consistency. However, I'd argue that proving a foundation equiconsistent with Peano Arithmetic should be "good enough". Hilbert's goal was to prove the system consistent by finitary means, but I imagine that being able to translate contradictions in the foundation into a finitary proof of contradiction accomplishes basically the same goal (even if it's technically different).

Even better is proving the foundation conservative over Peano Arithmetic (one of Hilbert's goal was also that the foundation should be conservative over finitary proofs) and implies equiconsistency (since $0=1$ is an arithmetical statement).

My question is **what are some candidates for a foundation of mathematics that is conservative over first-order Peano Arithmetic?**

As a first answer, consider ACA₀. It is a theory of second-order arithmetic, and so is suitable for doing a fair bit of analysis. Despite being able to deal with real numbers and infinite sets (it is even able to interpret hereditarily countable sets), it is in fact conservative over Peano Arithmetic. A proof can use infinite sets and other ideal objects, and the resulting proof can be converted to one using only the natural numbers and the Peano Axioms.

That being said, ACA₀ is a pretty weak answer. As a foundation, it wouldn't even let you do much set theory (the continuum hypothesis can't even be expressed) and I'm sure there are other branches of math it would struggle with as well.

Here are some additional desiderata (not strictly necessary):

- The non-arithmetical part should be as strong and convenient as possible. (ACA₀ is a pretty low-bar in this regard. A foundation should at least have sets like $\mathbb R^\mathbb R$ in it.)
- Ideally the proof of conservativeness can be formalized in Peano Arithmetic itself. (For example, you can prove in Peano Arithmetic that "for all $\phi$. If $\phi$ is a sentence in first-order arithmetic and there exists a proof of $\phi$ in ACA₀, then there exists a proof of $\phi$ in PA". So ACA₀ passes.)
- Ideally the foundation should make it
*easier*to prove things about the natural numbers. For example, ideally it proves induction for all formulas in its language (not just the arithmetical formulas as demanded by PA). That is, for every formula $\phi(n)$ (with parameters), the universal closure of $$(\phi(0) \land \forall k \in \mathbb N. (\phi(k) \implies \phi(k+1))) \implies \forall n \in \mathbb N. \phi(n)$$ is a theorem. ACA₀ fails this (adding this as an axiom schema makes it have higher consistency strength than PA), but at least proves the second-order induction axiom $$\forall X. (0 \in X \land \forall k. (k \in X \implies k + 1 \in X)) \implies \forall n. n \in X$$ For example, a strong foundation that barely interacts with the natural numbers and just postulates that the natural numbers satisfy PA would be a poor choice.

If you prefer constructive mathematics, I'd also accept foundations conservative over Heyting Arithmetic.

partof what you want (full function spaces, e.g.). Adding EM to it is fiddly though, since (at least in the presence of choice) it implies full 2nd-order comprehension. $\endgroup$conservativeextension goes beyond the issue pointed out by Emil (namely that it won't be able to prove the consistency of PA), but that it won't be able to prove many results that are viewed as true (e.g. Goodstein's theorem) and indispensable (many basic results in analysis that depend not only on ZF but also mild forms of choice, such as the $\sigma$-additivity of the Lebesgue measure). $\endgroup$notlose the axiom of choice since it is conservative over first-order arithmetic (generally speaking), so answers may include foundations with the axiom of choice. $\endgroup$12more comments