What subsystem of third order arithmetic proves the real numbers are Dedekind complete? 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.
 A: 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.
