Constructive Cauchy sequences vs. Dedekind cuts

Link post

In classical ZF and ZFC, there are two standard ways of defining reals: as Cauchy sequences and as Dedekind cuts. Classically, these are equivalent, but are inequivalent constructively. This makes a difference as to which real numbers are definable in type theory.

Cauchy sequences and Dedekind cuts in classical ZF

Classically, a Cauchy sequence is a sequence of reals , such that for any , there is a natural such that for any , . Such a sequence must have a real limit, and the sequence represents this real number. Representing reals using a construction that depends on reals is unsatisfactory, so we define a Cauchy sequence of rationals (CSR) to be a Cauchy sequence in which each is rational.

A Cauchy sequence lets us approximate the represented real to any positive degree of precision. If we want to approximate the real by a rational within , we find N corresponding to this and use as the approximation. We are assured that this approximation must be within of any future in the sequence; therefore, the approximation error (that is, ) will not exceed .

A Dedekind cut, on the other hand, is a partition of the rationals into two sets such that:

  • and are non-empty.

  • For rationals x < y, if , then ( is downward closed).

  • For , there is also with ( has no greatest element).

It represents the real number . As with Cauchy sequences, we can approximate this number to within some arbitrary ; we do this by doing a binary search to find rationals with , at which point approximates to within . (Note that we need to find rational bounds on before commencing a straightforward binary search, but this is possible by listing the integers sorted by absolute value until finding at least one in and one in .)

Translating a Dedekind cut to a CSR is straightforward. We set the terms of the sequence to be successive binary search approximations of , each of which are rational. Since the binary search converges, the sequence is Cauchy.

To translate a CSR to a Dedekind cut, we will want to set to be the set of rational numbers strictly less than the sequence’s limit; this is correct regardless if the limit is rational (check both cases). These constitute the set of rationals for which there exists some rational and some natural N, such that for every n > N, . (In particular, we set some , and N can be set so that successive terms are within of the limit).

We’re not worried about this translation being computable, since we’re finding a classical logic definition. Since CSRs can be translated to Dedekind cuts representing the same real number and vice versa, these formulations are equivalent.

Cauchy sequences and Dedekind cuts in constructive mathematics

How do we translate these definitions to constructive mathematics? I’ll use an informal type theory based on the calculus of constructions for these definitions; I believe they can be translated to popular theorem provers such as Coq, Agda, and Lean.

Defining naturals, integers, and rationals constructively is straightforward. Let’s first consider CSRs. These can be defined as a pair of values:


Generally, type theories are computable, so and will be computable functions.

What about Dedekind cuts? This consists of a quadruple of values

Where is the Boolean type. corresponds to the set of rationals for which is true. The triple must satisfy:

specifies the sets and ; and show that and are non-empty; maps an element of to a greater element of . The conditions straightforwardly translate the classical definition to a constructive one.

Let’s first consider translating Dedekind cuts to CSRs. We can use and as bounds for a binary search and generate successive terms in the binary search to get our Cauchy sequence. It is easy to bound the error of the binary search and thereby specify .

The other way around is not possible in general.

Showing that not every constructive Cauchy sequence corresponds to a constructive Dedekind cut

I will show that there is a constructive CSR that cannot be translated to a constructive Dedekind cut, assuming a computable type theory.

This will use the framework of arbitration oracles, or consistent guessing in Scott Aaronson’s terms.

Let be a Turing machine that does not necessarily halt, but returns a Boolean if it does halt. Let be equal to 0 if doesn’t halt; if halts in exactly steps returning a boolean , then, if is true, , and if is false, then .

We will first try representing as a function from Turing machines to CSRs. We will define to be a CSR for . This is a simple approximation; to find , we run for steps. If has halted by then, we know and can set . Otherwise, we set the approximation

This sequence is (constructively) Cauchy since all terms past are within of each other. This makes a valid for the Cauchy sequence computable (we simply need ).

On the other hand, cannot be represented as a function returning a Dedekind cut. Suppose represents the set for the Dedekind cut of . We will specify to be an arbitration oracle, by setting . This is an arbitration oracle by cases:

  • If doesn’t halt, then the arbitration oracle can return anything.

  • If halts and returns true, then the arbitration oracle must return true. Since in this case, we must have , so is correct in this case.

  • If halts and returns false, then the arbitration oracle must return false. Since in this case, we must have , so is correct in this case.

Since arbitration oracles are uncomputable, this shows that it isn’t possible to represent as a computable function returning a Dedekind cut.


While CSRs are equivalent to Dedekind cuts in classical logic, they are not equivalent in type theory. In type theory, every Dedekind cut can be translated to an equivalent CSR, but not vice versa. While a constructive CSR allows approximation to an arbitrary positive approximation error, a constructive Dedekind cut additionally allows exact queries to determine whether some rational is strictly greater than the represented real number.

This has implications for representing real numbers in type theory. I’m interested in this because I’m interested in constructive definitions of maximal lottery-lotteries in social choice theory, and I expect this to be relevant in other areas of math where constructive and computable definitions are desirable.