Completing half of Hilbert's program: Foundations that are conservative over Peano Arithmetic

Question

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):

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

Answer 1

The foundation in this answer is probably a bit weird to work in, but I think it is interesting meta-mathematically and would at least be interesting to compare other foundations too. Perhaps it is bi-interpretable with a less weird theory. I described it in this comment as a "bit lazy" but figured it would still be worth it to post.

Take the language of first-order set theory and add a constant symbol $\mathcal N$. The theory $T$ is $$\text{ZFC} + (\mathcal N \vDash \text{PA})$$ and an arithmetical formula $\phi$ is intended to be interpreted in $T$ as $$\mathcal N \vDash \phi$$

When $T$ proves $\mathcal N \vDash \phi$, then ZFC proves $\forall M. M \vDash \text{PA} \implies M \vDash \phi$ and thus $\text{PA} \vdash \phi$ by Gödel's completeness theorem. Thus $T$ is conservative over PA. It also satisfies the first desiderata very well, containing all of ZFC.

However, it does very poorly on the other two desiderata. Conservativeness cannot be proved within PA, but requires that ZFC is $\Sigma^0_1$-sound. In particular, $T$ is equi-consistent with ZFC. And converting $T$ proofs into PA proofs algorithmically can only be done with brute-force search (or some sort of proof mining). It is also a bit weird since we are treating the domain of $\mathcal N$ like it is the set of natural numbers, but $\omega$ (the way the set of natural numbers is usually represented in set theory) is still around.

Some improvements would be if we could weaken ZFC so that structures isomorphic to $\omega$ don't exist (just getting rid of the axiom of infinity doesn't work, the intersection of all the inductive subsets of $\mathcal N$ is isomorphic to $\omega$, so we need to weaken the axiom schema of separation) and so that only arithmetically definably elements of $P(\mathcal N)$ exist (so that we can at least get the second order induction axiom).

I think meta-mathematically $T$ is quite interesting, with the stipulation of how arithmetic should be interpreted. I have never seen someone analyze ZFC with an interpretation of arithmetic other than $\omega$ (EDIT: turns out it has been done before. See Can we interpret arithmetic in set theory, with exactly PA as the ZFC provable consequences?). By changing it, you can weaken the arithmetic significantly! For example, notice how $T$ is able to prove that models of PA exist (both $\omega$ and $\mathcal N$ are examples). But it doesn't prove PA consistent syntactically, because that statement gets interpreted relative to $\mathcal N$, and it is consistent with $T$ that $$\mathcal N \vDash \lnot \text{Con}(\text{PA})$$

So in particular, $T$ doesn't prove the statement "every theory with a model is syntactically consistent". Surely that is interesting!

Generalizing, we can imagine models of set theory that "come equipped" with an interpretation of arithmetic. Models of ZFC can be naturally equipped with an interpretation using $\omega$ and models of $T$ can be naturally equipped with interpretations using $\mathcal N$.

This of course extends to other foundations, not just ZFC. For example, we can imagine type theories or toposes that have an interpretation of arithmetic bolted on that doesn't necessarily need to use the natural number object.

Answer 2

One possible such theory is described by Solomon Feferman in chapter 13 (“Weyl vindicated: Das Kontinuuum seventy years later”) of his book In the Light of Logic (Oxford University Press 1998); specifically, I am referring to the formal system denoted $W$ and described in §8 (“A Theory of Flexible Finite Types for Weyl's Program”) of the aforementioned chapter.

This system $W$ is intended by Feferman to be a precise formalization of a proposed foundation for analysis set forth in Hermann Weyl's 1918 monograph Das Kontinuum, kritische Untersuchungen über die Grundlagen der Analysis.

It is analyzed metamathematically in two papers by Feferman & Jäger, “Systems of explicit mathematics with non-constructive $\mu$-operator” parts I & II (1993 & 1996), in which it is proved (IIUC, because the notation is very confusing) that $W$ is a conservative extension of $\mathrm{PA}$.

In §9 of the same chapter, as well as in the next chapter (“Why a Little Bit Goes a Long Way: Logical Foundations of Scientifically Applicable Mathematics”), Feferman argues that “scientifically applicable” mathematics can be formalized in $W$, and discusses some possible issues, and the relation with other foundational frameworks and ideas.

(I think there is also a constructive version of $W$, which would make sense as Weyl was IIUC at least somewhat sympathetic to constructive mathematics, but Feferman seems to only allude to it, so I don't know if it has been described or studied in any detail. I'm also unsure about the relation between the system $W$ described in the aforementioned 1998 book and the one described in another of Feferman's papers, The significance of Hermann Weyl's Das Kontinuum — which is also based on Weyl's monograph, but maybe not exactly identical to $W$ in all details, and which he mostly compares to $\mathrm{ACA}_0$. I'm afraid I can't say much more, because I only looked at this a long time ago and not too carefully even then, and now I'm very confused as to the exact relation between the various systems described by Feferman. I'm not even sure whether there is consensus on whether this is a faithful reformulation of Weyl's intended system.)