11.4 Comparison of Cauchy and Dedekind reals
Let us also say something about the relationship between the Cauchy and Dedekind reals. By
\autorefRC-archimedean-ordered-field, is an archimedean ordered field. It is also
admissible for , as can be easily checked. (In case is the initial
-frame
it takes a simple induction
, while in other cases it is immediate.)
Therefore, by \autorefRD-final-field there is an embedding
of ordered fields
which fixes the rational numbers.
(We could also obtain this from \autorefRC-initial-Cauchy-complete,\autorefRD-cauchy-complete.)
In general we do not expect and to coincide
without further assumptions.
Lemma 11.4.1.
If for every there merely exists
(11.4.1) |
then the Cauchy and Dedekind reals coincide.
Proof.
Note that the type inΒ (11.4.1) is an untruncated variant
ofΒ (LABEL:eq:RD-linear-order), which states thatΒ is a weak linear order.
We already know that embeds into , so it suffices to show that every Dedekind
real merely is the limit of a Cauchy sequence of rational numbers.
Consider any . By assumption there merely exists as in the statement of the
lemma, and by inhabitation of cuts there merely exist such that .
We construct a sequence by
recursion:
-
1.
Set .
-
2.
Suppose is already defined as such that . Define and . Then decides between and . If it decides then we set , otherwise .
Let us write for the -th term of the sequenceΒ . Then it is easy to see that and for all . Therefore and are both Cauchy sequences converging to the Dedekind cutΒ . We have shown that for every there merely exists a Cauchy sequence converging to . β
The lemma implies that either countable choice or excluded middle suffice for coincidence of and .
Corollary 11.4.3.
If excluded middle or countable choice holds then and are equivalent.
Proof.
If excluded middle holds then can be proved: either or . In the former case we are done, while in the latter we get because . Therefore, we getΒ (11.4.1) so that we can apply \autoreflem:untruncated-linearity-reals-coincide.
Suppose countable choice holds. The set is equivalent to , so we may apply countable choice to the statement that is located,
Note that is expressible as an existential statement . The (curried form) of the choice function is then preciselyΒ (11.4.1) so that \autoreflem:untruncated-linearity-reals-coincide is applicable again. β
Title | 11.4 Comparison of Cauchy and Dedekind reals |
\metatable |