First, let me address your question about provability. It is in fact quite easy to exhibit a pair of sequences of rationals $C_1, C_2$ such that
ZFC (indeed, much less) proves that exactly one is a Cauchy sequence, but
ZFC doesn't prove that $C_1$ is Cauchy and ZFC doesn't prove that $C_2$ is Cauchy.
Semantically speaking, in every model of ZFC, one of $C_1$ and $C_2$ is Cauchy, but both possibilities can occur.
Specifically:
Let the $i$th term of $C_1$ be $i$ if the continuum hypothesis holds, and $0$ if the continuum hypothesis fails.
Let the $i$th term of $C_2$ be $i$ if the continuum hypothesis fails, and $0$ if the continuum hypothesis holds.
ZFC proves that $C_1$ is Cauchy iff CH fails, and ZFC proves that $C_2$ is Cauchy iff CH holds, but ZFC does not decide CH so ZFC cannot tell which of $C_1$ and $C_2$ is Cauchy.
Next, let's sketch a ZFC proof (indeed, vastly less than ZFC) that the set of equivalence classes of Cauchy sequences - which I'll denote "$\mathbb{R}_C$" - is indeed uncountable. This is just Cantor's first argument superficially rephrased, but you might find this rephrasing helpful.
Specifically, for a Cauchy sequence $C=(c_i)_{i\in\mathbb{N}}$ and rationals $p<q$, say that $C$ avoids the interval $[p, q]$ if for some $n\in\mathbb{N}$ we have $$\forall m>n(c_m\not\in [p,q])$$ (that is, if $C$ eventually leaves $[p,q]$ and never comes back). It's a good exercise to show that whenever $p<q, r<s$ are rationals with $[p,q]\cap [r,s]=\emptyset$ (that is, either $p<q<r<s$ or $r<s<p<q$) we either have $C$ avoids $[p,q]$ or $C$ avoids $[r,s]$ (or both).
Next, we'll define a pair of operations on closed intervals with rational endpoints: for $[a, b]$ a closed interval with rational endpoints, let $$Left([a,b])=[a, a+{b-a\over 3}]\quad\mbox{and}\quad Right([a,b])=[b-{b-a\over 3}, b].$$ (Think about the construction of the Cantor set.)
Now we're ready to diagonalize (if we assume Choice; if not, we neeed an extra step, which I've outlined below). Suppose $(\mathbb{E}_i)_{i\in \mathbb{N}}$ is a sequence of equivalence classes of Cauchy sequences. Pick (via Choice) a representative $C_i=(c_j^i)_{j\in\mathbb{N}}$ of each $\mathbb{E}_i$.
We now define a sequence of closed intervals $(I_i)_{i\in\mathbb{N}}$ as follows:
Now let $a_n$ be the left endpoint of $I_n$, and consider the sequence $A=(a_n)_{n\in\mathbb{N}}$. It's easy to check that this is Cauchy and not equivalent to any $C_i$; thus, the equivalence class $\mathbb{A}$ of $A$ is not in $\mathbb{E}$, and this completes the proof.
If we didn't assume choice, the passage from $(\mathbb{E}_i)_{i\in\mathbb{N}}$ to $(C_i)_{i\in\mathbb{N}}$ appears problematic at first. However, we do in fact have a canonical way to pick representatives of equivalence classes.
Namely, suppose $\mathbb{E}$ is an equivalence class of Cauchy sequences. Fix an enumeration $(q_i)_{i\in\mathbb{N}}$ of $\mathbb{Q}$, let $p_i$ be the rational with minimal index such that some (equivalently, every) element of $\mathbb{E}$ does not avoid $[p_i, p_i+{1\over i}]$, and let $C=(p_i)_{i\in\mathbb{N}}$. It's a good exercise to check that this is well-defined and is a Cauchy sequence in $\mathbb{E}$.
Finally, a comment on definability and models.
What the above shows is that ZFC (indeed, much less) proves that the set of equivalence classes of Cauchy sequences of rationals is uncountable. This means that whenever $M$ is a model of ZFC (externally countable or not), there is no bijection in $M$ between what $M$ thinks is the set of Cauchy sequences and what $M$ thinks is $\mathbb{N}$. Of course, such a bijection might exist in reality (= externally).
Moreover, this does not contradict the possibility of every Cauchy sequence in $M$ being definable in $M$; this is a special case of the fact that pointwise definable models (which you mention) can exist. The map sending a Cauchy sequence in $M$ to a definition in $M$ of that Cauchy sequence is not definable in $M$ (per Tarski), and so we don't get a contradiction with the internal uncountability of the set of equivalence classes of Cauchy sequences.
One way to start, is to naively try to make completion by cuts "work" and see how the need for a new concept naturally comes up. So let's consider the set $C$ of all cuts of $A^+$ under the $\subseteq$ order and try to find a Boolean completion in there somewhere.
A couple easy facts make us immediately optimistic. First off, a union of cuts is a cut, as is the intersection of cuts, so we are in good shape for meets and joins. And moreover, we have $U_p\cap U_q=U_{p\cdot q}$ and $U_p\cup U_q = U_{p+q},$ so an embedding of $A$ embedding is shaping up nicely too.
Where things stop working so nicely is when we consider complements: the complement of a cut is not necessarily a cut and it's not generally the case that $A^+-U_p = U_{-p}.$ We have a nice structure (in fact, it is a complete Heyting algebra!), but it falls short of being a Boolean algebra. Nonetheless, let's see what we can do to make it work.
We know that if our embedding is to work, we need $-U_p=U_{-p}$. As we remarked previously, using set-theoretic complement $-U_p \ne A^+-U_p$ is wrong... we don't want $-U_p$ to contain literally everything that is not $\le p,$ rather we want it to consist of things that are incompatible with $p$. This is is made more clear by the identity $U_{-p}=\{q\in A^+: q\cdot p = 0 \}$, which just comes from the fact that $q\le - p$ if and only if $q\cdot p = 0.$ The natural generalization of this operation to arbitrary cuts is to let $-U = \{q\in A^+: \forall p\in U\; q\cdot p = 0\},$ or more succinctly, $-U = \{q\in A^+: U_q \cap U = \emptyset\}.$
We want our join operation to give us $U+ - U = A^+,$ but it not necessarily true that $U\cup -U=A^+,$ so the join operation needs to do more than just take the union. The key observation is that while $U_p\cup U_{-p}$ might not contain all of $A^+,$ there is a weaker sense in which it is big: it is dense in $A^+$. This suggests that the correct definition of addition is that $U+V$ is the set of all $p\in A^+$ such that $U\cup V$ is dense below $p$.
Finally, we need addition to satisfy $U+U= U,$ so since $U+U$ is the set of all $p$ that $U$ is dense below, it better be the case that $U$ contains every point it is dense below. That's not true for arbitrary cuts, so we restrict our set of cuts to just the ones for which it is true. These are the regular cuts! (Check that Jech's definition of regular cut is indeed equivalent to the statement that the cut contains every point it is dense below.)
Now we check that it works. Are the $U_p$ regular? Yes, any $q\nleq p$ has an extension incompatible with $p$ (this is just the statement that $A^+$ is a separative partial order), so $U_p$ is not dense below $q$ for any $q\notin U_p.$ Is $U+V$ necessarily regular? Yes, if $U+V$ is dense below $p,$ so is $U\cup V$ so if $p\notin U+V$ then $U+V$ is not dense below $p$. What about if we just let $U\cdot V=U\cap V$? That works fine since if $U\cap V$ is dense below $p$, so are $U$ and $V.$ We can likewise confirm that negation works like we expect, and that Jech's statement that $\overline U$ (the collection of all points $U$ is dense below) is the least regular cut containing $U$ and use that to show that joins (finite or infinite) exist and match up to our definition.
That was more than I planned to write... in case all that the motivation has the opposite of the intended effect, the headline news is:
A cut is regular if it contains every point it is dense below.
A couple closing notes
- While our motivation made substantial use of the fact that $A$ is a Boolean algebra, this generalizes to show that any separative partial order densely embeds into a complete Boolean algebra. As remarked above, separativity is what guarantees each $U_p$ is regular.
- The construction of the completion is a special case of a more general construction called the regular open algebra. For any topological space $X$, we say that $U\subseteq X$ is regular open if it is equal to the interior of its closure. The collection of all regular open subsets of $X$, ordered by $\subseteq$, is a complete Boolean algebra. Here, the relevant topological space is $P,$ where $U\subseteq P$ is open if and only if $U$ is a cut. The operation $U\mapsto \overline U$ is taking the interior of the closure.
Best Answer
Here is a partial answer.
For any infinite cardinal $\kappa$, we write $\mathrm{ded}(\kappa)$ for the supremum, over all linear orders $X$ of size $\kappa$, of the cardinality of the set of Dedekind cuts in $X$. We always have $\kappa<\mathrm{ded}(\kappa)\leq 2^\kappa$.
Now suppose $S$ is a saturated dense linear order of cardinality $\kappa$. I claim that $S$ has the maximal number of Dedekind cuts, i.e., the number of Dedekind cuts in $S$ is $\mathrm{ded}(\kappa)$.
Since $\mathrm{ded}(\kappa)$ is defined as a supremum, and $\kappa<\mathrm{ded}(\kappa)$, it suffices to show that for any $\lambda$ with $\kappa<\lambda\leq \mathrm{ded}(\kappa)$, if there is a linear order $X$ with $\lambda$-many Dedekind cuts, then $S$ has at least $\lambda$-many Dedekind cuts.
Now since $S$ is a saturated dense linear order and $|X|\leq |S|$, there is an order embedding $e\colon X\to S$. For each Dedekind cut $(L,R)$ in $X$, $(e(L),e(R))$ generates a Dedekind cut in $S$, unless it is "filled", i.e., there are elements of $S$ between $e(L)$ and $e(R)$. But since $|S| = \kappa$, at most $\kappa$-many of the images of the cuts in $X$ are filled in $S$. Since $\lambda>\kappa$, $\lambda$-many cuts in $X$ have images that are cuts in $S$. This completes the proof that $S$ has $\mathrm{ded}(\kappa)$-many Dedekind cuts.
How is this relevant to the hyperreals? Let $^*\mathbb{R}$ be an ultrapower of $\mathbb{R}$ by a non-principal ultrafilter on $\omega$. Then $^*\mathbb{R}$ is $\aleph_1$-saturated. If we assume CH, $|^*\mathbb{R}| = \aleph_1$, so the underlying linear order of $^*\mathbb{R}$ is $\aleph_1$-saturated and dense. By the result above, the number of Dedekind cuts in $^*\mathbb{R}$ is $\mathrm{ded}(\aleph_1)>\aleph_1$.
Thus, assuming CH, $|\overline{^*\mathbb{R}}|>\aleph_1$. And if we also assume $2^{\aleph_1} = \aleph_2$, then $|\overline{^*\mathbb{R}}|\leq 2^{|\mathbb{R}|} = \aleph_2$, so we obtain that $|\overline{^*\mathbb{R}}| = \aleph_2 = 2^{|\mathbb{R}|}$.
I suspect it is consistent that CH holds but $\mathrm{ded}(\aleph_1)<2^{\aleph_1}$ (can anyone confirm?). If so, then there is a model of ZFC in which $2^{\aleph_0} = \aleph_1 < \mathrm{ded}(\aleph_1) < 2^{2^{\aleph_0}}$, so $|\mathbb{R}| <|\overline{^*\mathbb{R}}| < 2^{|\mathbb{R}|}$.
I have no idea what happens if CH fails. It seems likely that without CH, the cardinality of $\overline{^*\mathbb{R}}$ depends on the ultrafilter you use to take the ultrapower.