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.
If for every there merely exists
then the Cauchy and Dedekind reals coincide.
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.
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 .
If excluded middle or countable choice holds then and are equivalent.
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|