Set-theoretical reverse mathematics of the reals

Question

While reading through a nice old question/answer about the behavior of measures on the reals in $ZFC$ that popped back up today, I began to wonder how much of $ZFC$ is required for various things we care about to behave the way we're familiar with them behaving.

This is nothing new to wonder about; Friedman and Simpson's whole program of reverse mathematics aims to understand exactly what set-theoretical axioms correspond to classical theorems of analysis being provable.

Unfortunately for me, most of the results I see in this area list the 'big five' subsystems of second order arithmetic that correspond the the reals 'behaving well'; it makes good intuitive sense that determining increasing chunks of the second order theory of the naturals would pin down increasing chunks of the behavior of the reals, considering $\mathbb{R}$ as a higher order object over $\mathbb{N}$ (Dedekind/Cauchy), but I have no intuitive sense of how these theories relate to $ZFC$ in consistency strength other than 'much weaker'.

Some light searching revealed Tim's excellent question about the relationship between proof theoretic strength, implication strength and consistency strength, but Noah's enlightening answer deepened my impression that I don't have a good intuitive understanding of the fruits of reverse mathematical research as they pertain to the question the program was intended to answer: which axioms of set theory are required to make the reals 'behave well'?

Consider the theory $Z-{\sf infinity}$; we have that $V_\omega$ is a model of $Z-{\sf infinity}$ in $ZF$ and $\mathbb{R}$ doesn't appear until $V_{\omega+1}$, so $Z-{\sf infinity}$ can't even define $\mathbb{R}$ let alone prove anything about it. Adding infinity we get up to $V_{\omega+\omega}$ so $\mathbb{R}$ can be defined and behaves well; somewhere in this delta the behavior of $\mathbb{R}$ is determined. (Further confounding things for me is the fact that $ZF-{\sf infinity}$ is equiconsistent with $PA$ again, so if we add replacement and remove infinity we lose all information back down to $ACA_0$.)

All of this leads me to wonder

Has there been any exploration of reverse mathematics in terms of 'theories over $Z-{\sf infinity}$'? Specifically, has any effort been made to identify 'minimal' 'set theoretical' axioms to add to $Z-{\sf infinity}$ allowing us to define $\mathbb{R}$ and prove that it behaves well?

From what I understand, $\Pi_1^1+CA_0$ is sufficient to prove everything considered a 'classical' theorem of analysis, with $ATR_0$, $ACA_0$, $WKL_0$ and $PRA_0$ serving as canonical descending 'ignorance points' regarding behavior of the reals. Accordingly, a translation between these theories of second order arithmetic and theories of the form $Z-{\sf infinity}+\psi$ would provide an answer. The nlab page on reverse mathematics seems to indicate that such a translation already partially exists with comments like "...the system $\Pi_1^1+CA_0$ corresponds to the system $ID_{<\omega}$ of finitely many generalized inductive definitions", but I am unfamiliar with this system and there don't seem to be any easily parsable references for a definition. Any pointers are appreciated.

---

In light of the fact that $Z-{\sf infinity}$ and $ZF-{\sf infinity}$ 'span the gap' from $PRA_0$ to $ACA_0$, canonical candidate 'weak set theories' corresponding to the bottom three ignorance points on the above list could be $Z-{\sf infinity}+\Sigma_n\ {\sf Replacement}$ or $Z-{\sf infinity}+\Pi_n\ {\sf Replacement}$ for appropriate $n$.

Answer 1

TL;DR: A most basic property of $\mathbb{R}$ is that it is not countable, which is surprisingly hard to prove (namely far beyond the Big Five you mention), as explored in [1, 2, 3].

The longer version. One readily shows that the reals are not denumerable via the usual diagonal proof; the latter goes through in weak logical systems, including RCA$_0$, the base theory of second-order Reverse Mathematics.

Dag Normann and I have explored how hard it is to prove that the reals are not countable, i.e. cannot be mapped injectively to the naturals. The following statement turns out to be interesting:

NIN: there is no injection from $[0,1]$ to $\mathbb{N}$.

Note that this is a statement of third-order arithmetic and we work in Kohlenbach's higher-order Reverse Mathematics ([0]), with base theory RCA$_0^\omega$.

First of all, NIN is hard to prove as follows: there are two conservative extensions of second-order arithmetic Z$_2$, called Z$_2^\omega$ and Z$_2^\Omega$, with definitions below. The system Z$_2^\omega$ cannot prove NIN, while Z$_2^\Omega$ can.

Secondly, the aforementioned hardness remains if we restrict NIN to nice/well-known function classes ([2]), including bounded variation and regulated functions.

Thirdly, a slight strengthening of NIN boasts many robust equivalences, as explored in [3]. This includes basic properties of functions of bounded variation, Fourier series, etc.

REFERENCES

[0] Ulrich Kohlenbach, higher-order Reverse Mathematics, Reverse Mathematics 2001, ASL, 2005.

[1] Dag Normann and Sam Sanders, On the uncountability of the reals, Journal of Symbolic Logic, 2022.

[2] Sam Sanders, On the Reverse Mathematics of the reals, LNCS, Proceedings of CiE22.

[3] Sam Sanders, Big in Reverse Mathematics: the uncountability of the reals, arxiv.

DEFINITIONS

The system Z$_2^\omega$ is RCA$_0^{\omega}$ plus, for every $k\in \mathbb{N}$, the existence of a functional S$_k^2$ that decides $\Sigma_k^1$-formulas.

The system Z$_2^\Omega$ is RCA$_0^\omega$ plus Kleene's quantifier $(\exists^3)$ as follows

$$ (\exists E)(\forall Y:\mathbb{N}^\mathbb{N}\rightarrow \mathbb{N})(E(Y)=0 \leftrightarrow (\exists f\in \mathbb{N}^\mathbb{N})(Y(f)=0)). $$

Note that NIN and Z$_2^\omega$ are essentially third-order, while Z$_2^\Omega$ is fourth-order.

On a historical note, in their Grundlagen der Mathematik, Hilbert and Bernays introduce a functional $\nu$ which is essentially $\exists^3$. The latter and similar third-order constructs are used to formalise real analysis; there is essentially no development based on second-order arithmetic.