8
$\begingroup$

Reverse mathematics is mainly about subsystems of second-order arithmetic, but in recent years it’s expanded to cover subsystems of third-order arithmetic as well. Now the fact that the real numbers are Dedekind complete is (encodable as) a statement in the language of third order arithmetic. And I think it’s probably provable using full third order arithmetic.

But my question is, what is the weakest subsystem of third-order arithmetic capable of proving that the real numbers are Dedekind complete?

By the way, the fact that the real numbers form a real closed field is provable even in $RCA_0$, so my question is really about the interpretability of the second-order theory of real numbers.

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ $\Pi^1_1$-CA (allowing third order parameters) is surely enough. Given a nonempty $X \subseteq \mathbb{R}$ which is bounded above, we can form the set $U = \{ q \in \mathbb{Q} : (\forall x \in \mathbb{R})(r \in X \to r \leq q)\}$ of all rational upper bounds of $X$ using $\Pi^1_1$-comprehension with parameter $X$. Note that $U$ is really just a second-order object, so $\inf U$ exists (by arithmetic comprehension) and $\sup X = \inf U$. So there is no need for any third-order axioms per se. $\endgroup$
    – François G. Dorais
    Commented Jul 22, 2020 at 15:14
  • 2
    $\begingroup$ It is fairly easy to show that over $\mathsf{ACA}_0$ Dedekind completeness for $\Pi^0_\infty$-sets of reals is equivalent to $\Pi^1_1\textsf{-CA}_0$. It is possible to derive $\Pi^1_1\textsf{-CA}_0$ from this form of Dedekind completeness using the fact that $\Pi^1_1\textsf{-CA}_0$ equivalent over $\mathsf{ACA}_0$ to the principle "every ill-founded tree $T\subseteq \omega^{<\omega}$ has a leftmost path." The latter equivalence could be proved using Kleene's normal forms for $\Pi^1_1$-sets. $\endgroup$
    – Fedor Pakhomov
    Commented Jul 23, 2020 at 9:35
  • 1
    $\begingroup$ It seems to me that in a similar way it is possible to show that over some some reasonable base system of higher-order reverse math (I guess something like $\mathsf{RCA}_0^{\omega}+\exists^2$ would work here) the third-order Dedekind completeness principle will be equivalent to the variant of $\Pi^1_1\textsf{-CA}_0$ that allows higher order parameters. Unfortunately, I am not comfortable enough with higher-order reverse math to write an answer. $\endgroup$
    – Fedor Pakhomov
    Commented Jul 23, 2020 at 9:39
  • $\begingroup$ @Pakhomov: one has to be very careful with the combination of $\exists^2$ and principles that allow for third-order parameters. See my "Plato and the foundations of mathematics" paper on arxiv. $\endgroup$
    – Sam Sanders
    Commented Aug 13, 2020 at 15:34

1 Answer 1

Reset to default
3
$\begingroup$

The answer to your question (unsurprisingly) depends on the formalisation of "being a subset of $\mathbb{R}$". Alex Kreuzer [1] has used characteristic functions to represent subsets of Cantor space $2^\mathbb{N}$. Dag Normann and I have adopted this formalism in e.g. [2, 3] for subsets of $\mathbb{R}$, as it yields nice results that generalise the notion of open/closed set from Reverse Mathematics.

Using the "sets as characteristic functions" formalism, Kohlenbach'ssystem RCA$_0^\omega$ from [0] plus Every bounded subset of $\mathbb{R}$ has a surpremum

is a conservative extension of WKL$_0$. One uses the intuitionistic fan functional from [0] to establish this.

References

[0] Kohlenbach, U., Higher order reverse mathematics, Reverse mathematics 2001, Lect. Notes Log., vol. 21, ASL, 2005, pp. 281–295.

[1] Kreuzer, A., Measure theory and higher order arithmetic. Proc. Amer. Math. Soc. 143 (2015), no. 12, 5411–5425.

[2] Normann D. and Sanders S., Open sets in Reverse Mathematics and Computability Theory, Journal of Logic and Computability 30 (2020), no. 8, pp. 40.

[3]____, On the uncountability of R, Submitted, arxiv: https://arxiv.org/abs/2007.07560 (2020), pp. 29.

Improve this answer
$\endgroup$

You must log in to answer this question.

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