If the Axiom of Countable Choice (ACC)

$$ \forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: \mathbb{N} \longrightarrow X . \forall n \in \mathbb{N} . \varphi [n, f(n)] $$

is not assumed in constructive mathematics, Dedekind and Cauchy real numbers are not equivalent in general. Even worse, Dedekind real numbers might not even form a set. Besides that, Dedekind cuts are notoriously unpleasant in terms of actual computation which is one of the most attractive parts of constructive mathematics. However, see Efficient Computation with Dedekind Reals by Bauer.

If we think of a Cauchy real as an algorithm that contains a convergence modulus $M_x: \mathbb{Z} \rightarrow \mathbb{N}$ and outputs rational approximations as:

$$ \left( x \in \mathbb{R} \right) \triangleq \left( \forall k \forall n,m \geq M_x(k) . \big| x(n) - x(m) \big| \leq 2^{-k} \right), $$

we then have a straightforward and transparent framework for computations (see, for instance, Schwichtenberg). On the other hand, in presence of the ACC, program extraction from proofs may get more difficult.

Dedekind reals are often used instead of Cauchy reals when ACC does not hold.

A Dedekind real is a defined as a pair $(L, U)$ of located sets of rational numbers satisfying:

  1. $q \in L \iff \exists r.(q < r \land r \in L)$ and $q \in U \iff \exists r.(r < q \land r \in U)$
  2. Both sets are inhabited: $\exists q. q \in L$ and $\exists q. q \in U$
  3. Sets are disjoint: $ \neg (q \in U \land q \in L)$
  4. (locatedness): $q < r \implies q \in L \lor r \in U$

What is the actual computational content of a Dedekind real in comparison to a (straightforward) Cauchy real? Can an efficient algorithm be derived for every constructive Dedekind real that outputs rational approximations with predictable accuracy (cf. modulus of convergence)? If yes, what is the difference between Cauchy and Dedekind algorithms?

  • $\begingroup$ Can you remind me exactly what a Dedekind and Cauchy real is in this context? Are the Dedekind reals one or two-sided Dedekind cuts? From your question, it also seems the Cauchy sequences need rates of convergence. $\endgroup$
    – Jason Rute
    Apr 17, 2016 at 20:01
  • 1
    $\begingroup$ @James, I think the located condition ensures downward (and upward) closer. If q' < q and q in L, then since the sets are disjoint, q' in L by the locatedness condition. $\endgroup$
    – Jason Rute
    Apr 17, 2016 at 22:51
  • 2
    $\begingroup$ @Paul Taylor: there is no algorithm that, given any two left sides of Dedekind cuts, computes the left side Dedekind cut of their difference. The arithmetical operations on Dedekind cuts have several issues of this sort. This is why the formalization in Reverse Mathematics uses quickly converging Cauchy sequences, and why some other formulations use a kind of binary expansion with bits for $1$, $0$, and $-1$. $\endgroup$ Apr 19, 2016 at 11:49
  • 1
    $\begingroup$ @CarlMummert - If the cut is "decidable" then it has a decision procedure, which is extra structure, not just a property, and that amounts to providing the right cut. Also, the two parts of the cut are not complementary if the real number that they define is rational. (The comment to which I was replying has vanished.) $\endgroup$ Apr 19, 2016 at 18:16
  • 2
    $\begingroup$ @Paul Taylor: the example is for decidable cuts, so the right side is just the complement of the left side, modulo possibly the rational value of the cut. But the example has open cuts. (You responded to that part of the comment). In any case, I do believe that people have seriously considered computing with Dedekind cuts in computable analysis and Reverse Mathematics, at least, and that cuts were abandoned exactly because they were not as convenient a framework as quickly converging Cauchy sequences. Whether cuts are more convenient in other areas is most likely a matter of opinion. $\endgroup$ Apr 19, 2016 at 18:20

5 Answers 5


In line with what is actually asked in the bold part of the question, I have taken the liberty of changing the title from constructive mathematics to computation. As it stood it was essentially a duplicate of another one, which already contains a lot about constructive but non-computational mathematics and so that would be the appropriate forum for further such discussion.

In fact Valery tagged the answer to the end of his first paragraph, namely @AndrejBauer's Efficient Computation with Dedekind Reals, which describes the ideas behind his Marshall calculator, whilst being based on our Dedekind Reals in Abstract Stone Duality and my Lambda Calculus for Real Analysis.

The setting for this answer is my ASD programme. I refuse to carry the baggage of obsolete programming languages (Turing Machines and Gödel Codings), any form of set theory (CZF, which I think is the setting for Lubarsky and Rathjen's paper, or even a topos) or the two bolted together (computable analysis in Weihrauch's TTE).

Valery's definition of a Dedekind cut is correct, but (to underline my rejection of any form of set theory) I write $\delta d$ and $\upsilon u$ for the down and up predicates instead of his $q\in L$ and $q\in U$ for lower and upper sets.

The predicate $\delta d$ says that (we so far know that) $d\lt x$ where $x$ is the real number being defined and similarly $\upsilon u$ means that (we so far know that) $x\lt u$.

Where this knowledge is incomplete, the pair $(\delta,\upsilon)$ satisfies all but the last axiom (locatedness) and is equivalent to an interval.

In particular, Dedekind cuts are two-sided. Taking the complement would amount to deducing knowledge or termination from ignorance or divergence.

There are plenty of examples of limiting processes that define "uncomputable" numbers that are best thought of as one-sided cuts. For example, the domain of definition of the solution of a differential equation is something that is only known from the inside; it is remarkable if we can obtain some knowledge from the outside, not that the boundary is "uncomputable" in this sense.

In the case where the cut defines a rational number, it should occur on neither side (Dedekind's choice was wrong here).

Defining the usual stuff in elementary real analysis is much easier and more natural using Dedekind cuts than with Cauchy sequences. Consider Riemann integration: $\delta d$ holds if there is some polygon (piecewise linear function) that lies below the curve and has area more than $d$; deducing the various properties from this is easy. This is gratuitously difficult if you insist in advance that the polygon have a particular shape of resolution $2^{-n}$ to make a Cauchy sequence.

The essential difference between a Dedekind cut and a Cauchy sequence as the representation of the solution of a mathematical problem is that Cauchy assumes that the problem has already been solved (to each degree of precision), whereas Dedekind merely combines all the formulae ("compiles" them into an "intermediate code", if you like), so that the problem remains to be solved.

This means that deriving a Cauchy sequence or decimal expansion from a Dedekind cut in general is just as difficult as solving a general real-valued mathematical problem. So I am under no illusion about the difficulty in implementing this proposal.

But it is a novel and so valuable way of looking at things.

The predicates define open subspaces of $\mathbb R$, so I would think that, in terms of recursion, they have to be $\Sigma^0_1$ or recursively enumerable. (I have thought a little bit about "descriptive set theory" (a name that needs to be changed) but haven't got very far with it.)

These predicates $\delta$ and $\upsilon$ are in the language of ASD and you will need to read the papers that I have linked to find out the details.

In the first instance, such predicates are built from $f(\vec x)\lt g(\vec x)$, where $f$ and $g$ are polynomials, using $\land$, $\lor$, $\exists$, recursion over $\mathbb N$ and universal quantification over closed bounded intervals.

We are given that $\delta d$ and $\upsilon u$ hold for certain rationals $d$ and $u$ and want to find some $d\lt m\lt u$ that is nearer to the result and whether $\delta m$ or $\upsilon m$.

In the case of $f(\vec x)\lt g(\vec x)$ we can use the (formal, interval) derivatives of $f$ and $g$ and the Newton--Raphson algorithm to do this. As is well known, this algorithm doubles the number of bits of precision at each step. This would justify the claim that the computation is efficient if we can extend it to more general formulae.

For more complicated logical expressions, Andrej developed a method of approximating these expressions with simpler ones. See his paper for details of this. This is quite closely analogous to methods of approximating real-valued functions by low(er) degree polynomials that have a very long history but have been developed in interval computation by Michal Konecny. Whilst Michal himself has used these computationally, they have not yet been incorporated into Andrej's calculator, but I hope that this will be done in future.

Computations like this with so-called "exact real arithmetic" are necessarily non-deterministic with regard to the Cauchy sequences tat they produce, which means that the existence of the completed sequence necessarily relies on Dependent Choice. This is entirely natural from a computational point of view and I don't see what use there is in discussing it as an issue of constructivity.

  • $\begingroup$ @ValerySaharov "If I do (correct) calculations I expect the algorithms to meet specific requirements." But there may be different results (steps and sequences) that both meet the requirements. In the example of representing real numbers by Cauchy sequences this is necessarily the case, for topological reasons. It is natural from the point of view of an ongoing calculation. ACC is needed if you consider the completed infinite calculation, turning a succession of choices of steps into a single choice of a sequence. $\endgroup$ Apr 20, 2016 at 13:37
  • $\begingroup$ @ValerySaharov You already have several good answers to your math.stackexchange question from people who are better qualified than me, whilst I am not subscribed. "Completed infinite calculation" doesn't relate to "real calculation" at all - it is an idealisation by "constructive mathematics". $\endgroup$ Apr 20, 2016 at 18:35

Once we look at computational content, rather than constructive content, things are easier to answer. When we work on the level of individual reals, all the representations are equivalent - a real is computable in one sense if and only if it is computable in the others. However, some of the conversions are not uniform (i.e. there is not usually an algorithm that can convert arbitrary reals from one representation to another). This lack of uniformity also presents issues in a constructive context.

A very thorough treatment of the uniformity issue was given by Jeffry L. Hirst, "Representations of reals in reverse mathematics", Bulletin of the Polish Academy of Sciences, Mathematics 55 (2007), 303–316 (PDF, eudml). Hirst summarized the known relationships and verified several relationships that had not been treated in the literature.

Here is a table from the paper. It shows the subsystem of second-order arithmetic necessary to (provably) convert a sequence of reals of one form to a sequence of reals of a second form. The use of sequences is a stand-in for uniformity, and has close connections to constructive analysis.

table of relationships between kinds of reals

The representations are:

  • $\rho$: rapidly converging Cauchy sequence
  • $\delta$: decimal expansion
  • $\lambda$: Dedekind cut
  • $\sigma$: open Dedekind cut

I suspect that similar kinds of results are in the literature on Weihrauch-style computable analysis, but I don't have a particular reference.

  • 1
    $\begingroup$ It is very unclear. I also find it hard sometimes because the notion of "Dedekind cut" varies so much from place to place (e.g. in computable analysis we would treat the cut as decidable, while in some other places the cut is only assumed to be enumerated). So comparing results becomes challenging. $\endgroup$ Apr 19, 2016 at 14:09
  • $\begingroup$ Is there, behind this answer, any work in which the "computational content" is actually contained in a computer? $\endgroup$ Apr 19, 2016 at 16:45
  • 2
    $\begingroup$ I am not sure if there is any evidence that can satisfy an opinion that computable analysis is not actually related to computational content, but at least I can point out that there are implementations of exact real arithmetic that are based on various representations from computable analysis. $\endgroup$ Apr 19, 2016 at 18:15
  • 1
    $\begingroup$ Moreover, the program of Proof Mining makes use of exactly the same framework, which is subsystems of higher-type classical and intuitionistic arithmetic, e.g. $\text{PA}^\omega$ and $\text{HA}^\omega$. $\endgroup$ Apr 19, 2016 at 18:22
  • $\begingroup$ I will mention at least in a comment that the linked PDF for Jeffry L. Hirst: Representations of reals in reverse mathematics can be now found here: appstate.edu/~hirstjl/bib/pdf/rrepsproof.pdf - the original link no longer works, but I did not want to bump the question just for this. $\endgroup$ Nov 28, 2022 at 9:03

As others have mentioned, there are many different variations in the exact notion of Cauchy reals and Dedekind reals which affect the answer.

I will choose variations so that I can offer a counterpoint to Paul Taylor's claim that Dedekind cuts represent a problem that "remains to be solved." If one uses the propositions-as-types correspondence to encode Dedekind cuts as "predicative subsets" $L, U : \mathbb{Q} \to \mathcal{U}$, where, $\mathcal{U}$ is the universe of types, and also reinterprets the rules of Dedekind cuts using propositions-as-types, for instance

  • inhabitedness: $\sum_{x : \mathbb{Q}} x \in L$ and $\sum_{x : \mathbb{Q}} x \in U$

  • locatedness: $\prod_{q, r : \mathbb{Q}} q < r \to (q \in L) + (r \in U)$

then Dedekind cuts do represent problems which have already been solved as well. In particular, the inhabitnedess and locatedness proofs above give the computational content. By inhabitedness, one can determine that a real number lies within some finite open interval. Then, by repeatedly using locatedness to cover this interval with several smaller ones, one can narrow down the interval where the real number must be to an arbitrarily small width.

Conversely, we can put the Cauchy definition on the same footing as the Dedekind definition by treating it as a "metric completion" in the sense of Steve Vickers's Localic completion of generalized metric spaces I. In this framework, a Cauchy real is a predicate $B : \mathbb{Q} \times \mathbb{Q}^+ \to \mathcal{U}$ on "formal balls", where $B(q, \varepsilon)$ holds if the real number is (strictly) within $\varepsilon$ from $q$. Then one of the rules which $B$ must satisfy is $$\prod_{\varepsilon : \mathbb{Q}^+} \sum_{q : \mathbb{Q}} B(q, \varepsilon),$$ which says topologically that for arbitrarily small $\varepsilon$, $\mathbb{R}$ is covered by balls with rational centers and radius $\varepsilon$, and computationally, that we can compute some $q$ within $\varepsilon$ of the real number.

The axioms defining valid Dedekind cuts as well as valid Cauchy predicates on formal balls provide a computational interface for computing with real numbers. The axioms also have a particular "geometric" form, which Vickers explains, and each suffices to define a topological space (or, more accurately, a space within the framework of locale theory or formal topology). Vickers proves (Theorem 26) that these two spaces, the order-theoretic (Dedekind) and metric (Cauchy), are homeomorphic, meaning that it is possible to use one computational interface to implement the other.

In general, the points of spaces formulated in this way may not be sets (predicatively), since one can vary the universe level of the predicative subsets. But $\mathbb{R}$ is in fact small (see Palmgren's Predicativity problems in point-free topology), so in fact the points of $\mathbb{R}$ form a set.

In terms of efficiency, one would probably consider metric API more "efficient", since approximating to a rational with a tolerance of $\varepsilon$ requires 1 "API call", whereas one needs a variable number of uses of the "locatedness" rule for Dededkind cuts, and each additional call provides only one more bit of information.


Dedekind reals are equivalent to multi-valued Cauchy reals

A (modulated) Cauchy real is represented by a set $S \subseteq \mathbb N \times \mathbb Q$ with the following properties:

  1. $$\forall n \in \mathbb N. \exists! q \in \mathbb Q. (n, q) \in S$$
  2. $$\forall (n, q) \in S, (m, r) \in S. |q - r| \le 2^{-n} + 2^{-m}$$

And sets $S_1$ and $S_2$ represent the same Cauchy real iff

  1. $$\forall (n, q) \in S_1, (m, r) \in S_2. |q - r| \le 2^{-n} + 2^{-m}$$

The multi-valued Cauchy reals are the same except we replace 1 with

1*. $$\forall n \in \mathbb N. \exists q \in \mathbb Q. (n, q) \in S$$

leaving 2 and 3 exactly the same. We just drop the requirement that there is only one $q$ for each $n$. The computational content is basically the same; a constructive proof of 1* gives an algorithm to rationally approximate the real number. There just might be multiple such proofs that give different approximations for the same $S$.

With the axiom of countable choice, every multi-valued Cauchy real is equal to an ordinary, single-valued Cauchy real.

But even without that axiom, the multi-valued Cauchy reals and the Dedekind reals are isomorphic, so you can give Dedekind reals computational meaning by treating them as multi-valued Cauchy reals.

In the other direction, if you modify the definition of the Dedekind reals to require that locatedness is witnessed by a function, the resulting object will be isomorphic to the Cauchy reals as originally defined. So the difference really is just "do you want functions or just existential statements", which is what choice principles conflate.

Here is the proof that the Dedekind reals are isomorphic to multi-valued Cauchy reals.


We embed the multi-valued Cauchy reals into the Dedekind reals as you might expect. For a multi-valued Cauchy real represented by $S$, we define:

$$L = \{ r \in \mathbb Q: \exists (n, q) \in S. q - r > 2^{-n} \}$$ $$U = \{ r \in \mathbb Q: \exists (n, q) \in S. q - r < -2^{-n} \}$$

Now we will show that every Dedekind real can be defined this way.

Let $y$ be a Dedekind real. We define $S$ as $$S = \{ (n, q) \in \mathbb N \times \mathbb Q : -2^{-n} \le q - y \le 2^{-n} \}$$

For an ordinary Cauchy real we'd need the axiom of countable choice to select $q$, but this is unnecessary for multi-valued Cauchy reals.

Verifying property (2) is just a little bit of algebra. Let's check property (1*).

Let $x, z \in \mathbb Q$ such that $x < y < z$. We prove that for any $k \in \mathbb N$, there is $q \in \mathbb Q$ such that $$-(\frac 23)^k (z - x) < q - y < (\frac 23)^k (z - x)$$ by induction on $k$.

  • Base case: For $k=0$ let $q = z$.
  • Induction step: Let $q'$ satisfy the theorem for $k$. To find $q$ for the $k+1$ case, we split into cases using locatedness:
    • $q' - y < \frac 13 (\frac 23)^k (z - x)$: Let $q = q' + \frac 13 (\frac 23)^k (z - x)$. We know that $- \frac 33 (\frac 23)^k (z - x) < q' - y < \frac 13 (\frac 23)^k (z - x)$ and thus $-(\frac 23)^{k+1} (z - x) < q - y < (\frac 23)^{k+1} (z - x)$.
    • $q' - y > - \frac 13 (\frac 23)^k (z - x)$: Let $q = q' - \frac 13 (\frac 23)^k (z - x)$. We know that $- \frac 13 (\frac 23)^k (z - x) < q' - y < \frac 33 (\frac 23)^k (z - x)$ and thus $-(\frac 23)^{k+1} (z - x) < q - y < (\frac 23)^{k+1} (z - x)$.

(Note, again, that we don't need countable choice since we don't need $q$ to be a function of $k$.)

Let $n \in \mathbb N$. Since $\lim_{k \to \infty} (\frac 23)^k (z - x) = 0$, there is a $k$ large enough that there is a $q \in \mathbb Q$ such that $-2^{-n} < q - y < 2^{-n}$. Then $(n,q) \in S$, demonstrating property (1*).

Verifying that the embedding into the Dedekind reals sends $S$ to $y$ is just a little bit of algebra.



(This is more of a comment than an answer, but I think the following caveat is indispensable whenever Cauchy reals are mentioned in constructive mathematics without Countable Choice.)

I'm puzzled by the fact that no answer to this question so far seems to mention the fact that (in the absence of Countable Choice) Cauchy reals can fail to be Cauchy-complete, so let me point to the paper “On the Cauchy Completeness of the Constructive Cauchy Reals” by Robert Lubarsky which explains this perplexing state of affairs well. (In contrast, the Dedekind reals are Cauchy-complete, and they are also Dedekind-complete.)

The situation about Cauchy reals is made very confused that, depending on authors, a “Cauchy sequence” of rationals may be a sequence $(r_n)$ such that $\forall N. \exists n. \forall p,q\geq n. (|r_p-r_q| < 2^{-N})$ or it may be one such that there exists $\nu\colon\mathbb{N}\to\mathbb{N}$ such that $\forall N. \forall p,q\geq \nu(N). (|r_p-r_q| < 2^{-N})$ (i.e., requiring a modulus of convergence). The two notions fail to coincide, so we actually have at least two different notions of Cauchy reals¹: Cauchy-reals-without-modulus and Cauchy-reals-with-modulus. When considering Cauchy sequences of Cauchy sequences, for the outer sequence we can demand a modulus or not, and for the inner sequences we can demand existence of a modulus for each one separately or the existence of a sequence of modulus sequences, and pretty much everything that can go wrong does; but in any case, a Cauchy real (with or without modulus) should be taken to be an equivalence class of Cauchy sequences of rationals (with or without modulus), and the main problem is that there is no way to choose a representative from each class in the sequence. This is all proved in Lubarsky's paper.

I don't know what happens if we define “Cauchy reals” as the smallest subset² of the Dedekind reals which contains the rationals and is closed under taking Cauchy sequences (with or without modulus). This would give two more notions of “Cauchy” reals to add to the mess.

  1. One piece of good news, however, is that if the difference between two Cauchy-reals-with-modulus converges-to-zero-without-modulus (viꝫ. $\forall N. \exists n. \forall k\geq n. (|r_k-s_k| < 2^{-N})$ where $(r_n)$ and $(s_n)$ are the two sequences), then it even converges-to-zero-with-modulus (viꝫ. there is $\mu\colon\mathbb{N}\to\mathbb{N}$ such that $\forall N. \forall k\geq \mu(N). (|r_k-s_k| < 2^{-N})$. This is very easy, but rarely well explained. So we don't have to distinguish two different equivalence relations on Cauchy-reals-with-modulus.

  2. I think this definition makes sense, but at this point I'm so terrified of lions lurking in the shadows that I wouldn't bet my hand on it.

  • 1
    $\begingroup$ The least Cauchy complete subfield of Dedekind reals that contains $\mathbb{Q}$ is also known as Escardó-Simpson reals. In homotopy type theory it coincides with the construction of Cauchy reals as a higher inductive-inductive type. See doi.org/10.1109/LICS.2001.932488 and arxiv.org/abs/1706.05956 $\endgroup$ Dec 27, 2023 at 19:33
  • $\begingroup$ @AndrejBauer Is this for “Cauchy complete” in the sense of “Cauchy-with-modulus” or in the sense of “Cauchy-without-modulus”? (I don't know how to unambiguously refer to these two notions in a more concise way.) Or have both notions been considered? Do the completions perhaps coincide? $\endgroup$
    – Gro-Tsen
    Dec 27, 2023 at 22:17
  • $\begingroup$ See section 11.3 of the HoTT book. We don't use Cauchy sequences but rather Cauchy approximations: a map $x : \mathbb{Q}_{+} \to \mathbb{Q}$ such that $\forall \delta, \epsilon \in \mathbb{Q}_{+} .\, |x_\delta - x_\epsilon| < \delta + \epsilon$. This corresponds to having a modulus of continuity as a map, cf. section 11.2.2. (You can pretty much read Chapter 11 without reading the rest of the HoTT book.) $\endgroup$ Dec 27, 2023 at 23:28
  • $\begingroup$ @AndrejBauer But, just to be clear, in a topos (or working within IZF), the reals you are talking about coincide with the smallest subset of the Dedekind reals that is closed under limits of Cauchy-sequences-with-modulus, correct? Not necessarily (or not obviously) with the a priori larger set defined as the smallest subset of the Dedekind reals that is closed under limits of Cauchy-sequences-without-modulus? (I think the latter definition makes sense, but maybe not, or maybe it's just widely believed to be uninteresting.) $\endgroup$
    – Gro-Tsen
    Dec 28, 2023 at 9:52
  • $\begingroup$ It's difficult to say what precisely the HoTT-style Cauchy reals correspond to in a topos, because a topos need not have higher inductive-inductive constructions. Nevertheless, the HoTT book shows that the Cauchy reals constructed therein are the smallest Cacuhy-complete archimedean ordered field. All the time, "Cacuhy" is defined in terms of Cauchy approximations (see comment above). In my head every Cauchy approximations gives a modulus, and ever modulus gives a Cauchy approximation, but I haven't checked on paper. $\endgroup$ Dec 28, 2023 at 17:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.