Return to Answer

Regarding Cauchy and Dedekind reals. The fact that every Dedekind real has a Cauchy representation is provable in very weak systems of intuitionistic analysis. The converse fact that every Cauchy real has a Dedekind representation is equivalent to the Weak König Lemma (WKL) — that every infinite tree of $\lbrace0,1\rbrace$-sequences has an infinite path. (See note.) This very weak form of König's lemma is provable in ZF, so there is no difference between Cauchy reals and Dedekind reals in ZF.

Breaking this down further, the ability to compare a Cauchy real to a given rational number is equivalent to the Lesser Limited Principle of Omniscience (LLPO), which can be formulated as follows $$\lnot(\exists n A(n) \land \exists n B(n)) \rightarrow (\forall n \lnot A(n) \lor \forall n \lnot B(n)),$$ where $A(n)$ and $B(n)$ are simple decidable statements (e.g., primitive recursive predicates). Note that LLPO is a consequence of the Law of Excluded Middle, and therefore true in every classical system such as ZF, but not necessarily in intuitionistic systems such as topoi. To extract a Dedekind cut from a Cauchy real, it is necessary to simultaneously compare a real with every rational number, so we need to repeat LLPO countably many times. WKL is precisely equivalent to countably many repetitions of LLPO. In set theory and topos theory, such repetitions come for free through comprehension. So the only thing that can prevent every Cauchy real to have a Dedekind cut in a topos is the failure of LLPO.

This is not quite true as I originally stated it. It is the existence of a "uniform method" for converting Cauchy reals into Dedekind reals which is equivalent to WKL. In classical systems, one can get around the uniformity requirement through clever use of the Law of Excluded Middle. In weak classical systems such as RCA₀ one can prove that every Cauchy real has a Dedekind cut by providing separate methods for rational and irrational numbers, thus sweeping a lot of the computation cost in deciding whether a real is rational or not. The equivalence with WKL is recovered when one asks to simultaneously find Dedekind cuts for an infinite sequence of Cauchy reals, as demonstrated by Hirst [Representations of reals in reverse mathematics, Bull. Pol. Acad. Sci. Math. 55 (2007), 303–316; MR2369116].

Regarding Cauchy and Dedekind reals. The fact that every Dedekind real has a Cauchy representation is provable in very weak systems of intuitionistic analysis. The converse fact that every Cauchy real has a Dedekind representation is equivalent to the Weak König Lemma (WKL) — that every infinite tree of $\lbrace0,1\rbrace$-sequences has an infinite path. (See note.) This very weak form of König's lemma is provable in ZF, so there is no difference between Cauchy reals and Dedekind reals in ZF.

Breaking this down further, the ability to compare a Cauchy real to a given rational number is equivalent to the Lesser Limited Principle of Omniscience (LLPO), which can be formulated as follows $$\lnot(\exists n A(n) \land \exists n B(n)) \rightarrow (\forall n \lnot A(n) \lor \forall n \lnot B(n)),$$ where $A(n)$ and $B(n)$ are simple decidable statements (e.g., primitive recursive predicates). Note that LLPO is a consequence of the Law of Excluded Middle, and therefore true in every classical system such as ZF, but not necessarily in intuitionistic systems such as topoi. To extract a Dedekind cut from a Cauchy real, it is necessary to simultaneously compare a real with every rational number, so we need to repeat LLPO countably many times. WKL is precisely equivalent to countably many repetitions of LLPO. In set theory and topos theory, such repetitions come for free through comprehension. So the only thing that can prevent every Cauchy real to have a Dedekind cut in a topos is the failure of LLPO.

This is not quite true as I originally stated it. It is the existence of a "uniform method" for converting Cauchy reals into Dedekind reals which is equivalent to WKL. In classical systems, one can get around the uniformity requirement through clever use of the Law of Excluded Middle. In weak classical systems such as RCA₀ one can prove that every Cauchy real has a Dedekind cut by providing separate methods for rational and irrational numbers, thus sweeping a lot of the computation cost in deciding whether a real is rational or not. The equivalence with WKL is recovered when one asks to simultaneously find Dedekind cuts for an infinite sequence of Cauchy reals, as demonstrated by Hirst [Representations of reals in reverse mathematics, Bull. Pol. Acad. Sci. Math. 55 (2007), 303–316; MR2369116].

Regarding Cauchy and Dedekind reals. The fact that every Dedekind real has a Cauchy representation is provable in very weak systems of intuitionistic analysis. The converse fact that every Cauchy real has a Dedekind representation is equivalent to the Weak König Lemma (WKL) — that every infinite tree of $\lbrace0,1\rbrace$-sequences has an infinite path. (See note.) This very weak form of König's lemma is provable in ZF, so there is no difference between Cauchy reals and Dedekind reals in ZF.

Breaking this down further, the ability to compare a Cauchy real to a given rational number is equivalent to the Lesser Limited Principle of Omniscience (LLPO), which can be formulated as follows $$\lnot(\exists n A(n) \land \exists n B(n)) \rightarrow (\forall n \lnot A(n) \lor \forall n \lnot B(n)),$$ where $A(n)$ and $B(n)$ are simple decidable statements (e.g., primitive recursive predicates). Note that LLPO is a consequence of the Law of Excluded Middle, and therefore true in every classical system such as ZF, but not necessarily in intuitionistic systems such as topoi. To extract a Dedekind cut from a Cauchy real, it is necessary to simultaneously compare a real with every rational number, so we need to repeat LLPO countably many times. WKL is precisely equivalent to countably many repetitions of LLPO. In set theory and topos theory, such repetitions come for free through comprehension. So the only thing that can prevent every Cauchy real to have a Dedekind cut in a topos is the failure of LLPO.

This is not quite true as I originally stated it. It is the existence of a "uniform method" for converting Cauchy reals into Dedekind reals which is equivalent to WKL. In classical systems, one can get around the uniformity requirement through clever use of the Law of Excluded Middle. In weak classical systems such as RCA₀ one can prove that every Cauchy real has a Dedekind cut by providing separate methods for rational and irrational numbers, thus sweeping a lot of the computation cost in deciding whether a real is rational or not. The equivalence with WKL is recovered when one asks to simultaneously find Dedekind cuts for an infinite sequence of Cauchy reals, as demonstrated by Hirst [Representations of reals in reverse mathematics, Bull. Pol. Acad. Sci. Math. 55 (2007), 303–316].

Regarding Cauchy and Dedekind reals. The fact that every Dedekind real has a Cauchy representation is provable in very weak systems of intuitionistic analysis. The converse fact that every Cauchy real has a Dedekind representation is equivalent to the Weak König Lemma (WKL) — that every infinite tree of $\lbrace0,1\rbrace$-sequences has an infinite path. (See note.) This very weak form of König's lemma is provable in ZF, so there is no difference between Cauchy reals and Dedekind reals in ZF.

Breaking this down further, the ability to compare a Cauchy real to a given rational number is equivalent to the Lesser Limited Principle of Omniscience (LLPO), which can be formulated as follows $$\lnot(\exists n A(n) \land \exists n B(n)) \rightarrow (\forall n \lnot A(n) \lor \forall n \lnot B(n)),$$ where $A(n)$ and $B(n)$ are simple decidable statements (e.g., primitive recursive predicates). Note that LLPO is a consequence of the Law of Excluded Middle, and therefore true in every classical system such as ZF, but not necessarily in intuitionistic systems such as topoi. To extract a Dedekind cut from a Cauchy real, it is necessary to simultaneously compare a real with every rational number, so we need to repeat LLPO countably many times. WKL is precisely equivalent to countably many repetitions of LLPO. In set theory and topos theory, such repetitions come for free through comprehension. So the only thing that can prevent every Cauchy real to have a Dedekind cut in a topos is the failure of LLPO.

This is not quite true as I originally stated it. It is the existence of a "uniform method" for converting Cauchy reals into Dedekind reals which is equivalent to WKL. In classical systems, one can get around the uniformity requirement through clever use of the Law of Excluded Middle. In weak classical systems such as RCA₀ one can prove that every Cauchy real has a Dedekind cut by providing separate methods for rational and irrational numbers, thus sweeping a lot of the computation cost in deciding whether a real is rational or not. The equivalence with WKL is recovered when one asks to simultaneously find Dedekind cuts for an infinite sequence of Cauchy reals, as demonstrated by Hirst [Representations of reals in reverse mathematics, Bull. Pol. Acad. Sci. Math. 55 (2007), 303–316; MR2369116].

Regarding Cauchy and Dedekind reals. The fact that every Dedekind real has a Cauchy representation is provable in very weak systems of intuitionistic analysis. The converse fact that every Cauchy real has a Dedekind representation is equivalent to the Weak König Lemma (WKL) — that every infinite tree of $\lbrace0,1\rbrace$-sequences has an infinite path. This very weak form of König's lemma is provable in ZF, so there is no difference between Cauchy reals and Dedekind reals in ZF.

Breaking this down further, the ability to compare a Cauchy real to a given rational number is equivalent to the Lesser Limited Principle of Omniscience (LLPO), which can be formulated as follows $$\lnot(\exists n A(n) \land \exists n B(n)) \rightarrow (\forall n \lnot A(n) \lor \forall n \lnot B(n)),$$ where $A(n)$ and $B(n)$ are simple decidable statements (e.g., primitive recursive predicates). Note that LLPO is a consequence of the Law of Excluded Middle, and therefore true in every classical system such as ZF, but not necessarily in intuitionistic systems such as topoi. To extract a Dedekind cut from a Cauchy real, it is necessary to simultaneously compare a real with every rational number, so we need to repeat LLPO countably many times. WKL is precisely equivalent to countably many repetitions of LLPO. In set theory and topos theory, such repetitions come for free through comprehension. So the only thing that can prevent every Cauchy real to have a Dedekind cut in a topos is the failure of LLPO.

Regarding Cauchy and Dedekind reals. The fact that every Dedekind real has a Cauchy representation is provable in very weak systems of intuitionistic analysis. The converse fact that every Cauchy real has a Dedekind representation is equivalent to the Weak König Lemma (WKL) — that every infinite tree of $\lbrace0,1\rbrace$-sequences has an infinite path. (See note.) This very weak form of König's lemma is provable in ZF, so there is no difference between Cauchy reals and Dedekind reals in ZF.

Breaking this down further, the ability to compare a Cauchy real to a given rational number is equivalent to the Lesser Limited Principle of Omniscience (LLPO), which can be formulated as follows $$\lnot(\exists n A(n) \land \exists n B(n)) \rightarrow (\forall n \lnot A(n) \lor \forall n \lnot B(n)),$$ where $A(n)$ and $B(n)$ are simple decidable statements (e.g., primitive recursive predicates). Note that LLPO is a consequence of the Law of Excluded Middle, and therefore true in every classical system such as ZF, but not necessarily in intuitionistic systems such as topoi. To extract a Dedekind cut from a Cauchy real, it is necessary to simultaneously compare a real with every rational number, so we need to repeat LLPO countably many times. WKL is precisely equivalent to countably many repetitions of LLPO. In set theory and topos theory, such repetitions come for free through comprehension. So the only thing that can prevent every Cauchy real to have a Dedekind cut in a topos is the failure of LLPO.

This is not quite true as I originally stated it. It is the existence of a "uniform method" for converting Cauchy reals into Dedekind reals which is equivalent to WKL. In classical systems, one can get around the uniformity requirement through clever use of the Law of Excluded Middle. In weak classical systems such as RCA₀ one can prove that every Cauchy real has a Dedekind cut by providing separate methods for rational and irrational numbers, thus sweeping a lot of the computation cost in deciding whether a real is rational or not. The equivalence with WKL is recovered when one asks to simultaneously find Dedekind cuts for an infinite sequence of Cauchy reals, as demonstrated by Hirst [Representations of reals in reverse mathematics, Bull. Pol. Acad. Sci. Math. 55 (2007), 303–316].