We need something more than the axioms of ZFC to prove the Dedekind completeness?

Question

The Dedekind completeness is defined in many ways. Let show one of them to discuss the question.

We define a Dedekind cut $R$ as a non-empty subset of $\Bbb Q$ with this structure:

1. $R$ dont have a minimum

2. If $q\in R$ then $r\in R$ for all $r>q$

3. $\Bbb Q\setminus R\neq\emptyset$

We define $\Bbb R$ as the set of Dedekind cuts. Then we can check that $R\ge R'\iff R\subseteq R'$ define a total order in $\Bbb R$.

Then, from this definition of order, if we have some collection of Dedekind cuts $R_j$ bounded below by $A$ and bounded above by $B$, that is there is a Dedekind cut $A$ such that $R_j\subseteq A$ for all $j$ and a Dedekind cut $B$ such that $B\subseteq R_j$ for all $j$, then we can see that

$$I:=\bigcup_j R_j\quad\text{ and }\quad S:=\bigcap_j R_j$$

defines the infimum and the supremum of the collection of the $R_j$. As @AndreasBleas pointed in the commentaries for the case that $\min(S)=m$ exists, then we take $S\setminus\{m\}$ as the supremum of the collection of $R_j$.

Then my question: I cant see, for this definition, that we need some special axiom as Cauchy sequences or the nested intervals axiom to prove the existence of the infimum and supremum for bounded set of reals.

Then, my question, we need something more than the axioms of ZFC (by example in this case) to prove that $I$ and $S$ are the infimum or supremum respectively? The unique thing that we used here is the arbitrary union or intersection of sets, with nothing special in it. Thank you in advance.

Answer 1

The point here is that "a bounded collection of Dedekind cuts" is just a set of Dedekind cuts. The union of any set is guaranteed by the axiom of union, and since the set is not empty, the intersection of this set is guaranteed to exist by the axiom [schema] of separation.

So indeed, to prove that $\Bbb R$ [exists and that it] is complete we need far less than $\sf ZFC$. We needed extensionality, power set, infinity, union and separation.

This can be pushed even lower by restricting the power set axiom (to say something along the lines "the set of natural numbers has only two power sets", or some other finite number of iterations that is needed here), and to restrict which separation axioms we use. But let's not get ahead of ourselves.