This started out as a question about Dedekind cuts and determining which of two interpretations of the definition of "Dedekind cut" is correct. While writing that question, I realized that I had unwittingly assumed that every real number is the limit of a convergent sequence of rationals.
This is a problem because 1) the set of such sequences may be countable depending on the definition of "convergence" and 2) "limits" define equivalence classes of such sequences, and the set of said equivalence classes may be countable even if the set of convergent sequences is not.
To lay down some ground rules, I know the set of all sequences of rational numbers ($\Bbb{Q}^\Bbb{N}$)to be uncountable, with cardinality equal to that of the power set of the integers ($2^{\aleph_0}$).$^{1}$
Now, the subset $S_Q$ of convergent sequences of rationals is a proper subset of $\Bbb{Q}^\Bbb{N}$ under all but one definition of "convergence" (that being "a sequence in $\Bbb{Q}$ converges iff it exists") so the possibility that the cardinality of the set of convergent sequences is strictly less than that of $\Bbb{Q}^\Bbb{N}$ – and potentially countable – is open.
If we restrict ourselves to either the set of definable or provably convergent sequences, then $S_Q$ is necessarily countable (proof sketch upon request). With that in mind, it seems reasonable that the set of convergent sequences of rationals must contain uncountably many undefinable members in order that the reals should remain uncountable.
Edit: I would add that "definable" here assumes a first-order theory in a countable language. I don't know anywhere near enough about pointclasses or hierarchies to discuss them in detail. For those interested, there are pointwise-definable models of ZFC in which every sequence of rationals is definable.
That being said, this doesn't help me unless I can figure out a way to prove the existence of convergent but not provably convergent sequences of rationals (even then, I would prefer to have a "witness").
Edit: the existence of convergent but not provably convergent sequences is equivalent to the existence of Cauchy but not provably Cauchy sequences of rationals that converge in $\Bbb{R}$. The existence of such sequences is implied by the uncountability of the set of Cauchy sequences which converge to $x$ for every real number $x$ (though no such sequence can be [directly] defined). This can be proven in ZF by modifying the diagonal argument as long as $\forall p\in\Bbb{Q}.\forall 0<\varepsilon.\exists q\in\Bbb{Q}.0<|p-q|<\varepsilon$ (which ought to follow from any proof that the rationals, under their usual ordering, are a dense subset of the reals).
Setting this aside and assuming that the set of all convergent sequences of rationals is uncountable, and that each real number is the limit of at least one such sequence, I encounter another problem. The sequence of rationals defining a particular real number is not unique – that is, two or more distinct sequences may have the same limit and thus represent the same real number (the proof is trivial).
If $R$ is an equivalence relation on $S_Q$ where $\displaystyle\forall\mathbf{a},\mathbf{b}\in S_Q.\mathbf{a}R\mathbf{b}\iff\lim_{n\to\infty}a_n=\lim_{n\to\infty}b_n$ then presumably $\Bbb{R}\cong S_Q/R$. For each $x\in\Bbb{R}$ the set of sequences in $\Bbb{Q}$ converging to $x$ is – admitting the aforementioned unprovably convergent sequences – uncountable. Because $S_Q=\bigcup (S_Q/R)$, $S_Q$ remains uncountable even if $S_Q/R$ is countable (since the countable union of uncountable sets is uncountable).
I'm not sure how to go about proving that $S_Q/R$ is uncountable, especially given that assuming $S_Q/R$ is countable without first assuming that $\Bbb{R}$ is uncountable fails to produce a contradiction.$^2$
Next Step
It at least seems plausible that $S_Q/R$ might be countable, but that my original premise (that every real is the limit of at least one convergent sequence of rationals) is false. If nothing else, we might consider that $S_Q/R$ represents something between the set of definable real numbers and the set of real numbers.
I would like to think that this is the case and that the number line can be filled in by adding nonconvergent sequences to $S_Q$. Intuitively, it would seem that the limit of a nonconvergent sequence cannot be a real number. However, since most real numbers are undefinable, and most such limits are undefined, it is in some ways more intuitive to think that equivalence classes of such nonconvergent sequences account for the remaining [undefinable] real numbers. Since the set of nonconvergent sequences has uncountably many uncountable subsets, the equivalence classes of nonconvergent sequences could account for the uncountability of the real numbers if $S_Q$ were countable.
While the construction of such equivalence classes is completely impossible in any sort of recursively definable sense, it might be possible to get a glimpse by assigning stages in the construction to a net over some uncountable space (think of something like an analogue Turing machine).
Footnotes:
$^1$I'm leaving continuum hypothesis and choice out of this question because that dead horse has been beaten enough and I'm not trying to start a war.
$^2$The easy way out would of course be to say that because $\Bbb{R}$ is uncountable, $S_Q/R$ must be uncountable. However, the purpose of this endeavor was to show that the real numbers, constructed using Dedekind cuts, are uncountable – at least, given a particular understanding of "Dedekind cut". Asserting that $S_Q/R$ is uncountable because the real numbers are and using this to show that the set of Dedekind cuts is uncountable ultimately amounts to saying "the reals are uncountable because the reals are uncountable" – which, while not strictly false, is not particularly insightful.
Best Answer
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:
$I_0=[0,1]$.
$I_{n+1}=Left(I_n)$ if $C_n$ avoids $Left(I_n)$, and $Right(I_n)$ otherwise.
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.