TransWikia.com

What subsystem of third order arithmetic proves the real numbers are Dedekind complete?

MathOverflow Asked on November 26, 2021

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.

One Answer

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.

Answered by Sam Sanders on November 26, 2021

Add your own answers!

Ask a Question

Get help from others!

© 2024 TransWikia.com. All rights reserved. Sites we Love: PCI Database, UKBizDB, Menu Kuliner, Sharing RPP