Constructive Cauchy sequences vs. Dedekind cuts

~ Jessica Taylor

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 x_1, x_2, \ldots, such that for any \epsilon > 0, there is a natural N such that for any m, n > N, |x_m - x_n| < \epsilon. 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 x_i 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 \epsilon, we find N corresponding to this \epsilon and use x_{N+1} as the approximation. We are assured that this approximation must be within \epsilon of any future x_i in the sequence; therefore, the approximation error (that is, |x_{N+1} - \lim_{i \rightarrow \infty} x_i|) will not exceed \epsilon.

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

  • A and B are non-empty.
  • For rationals x < y, if y \in A, then x \in A (A is downward closed).
  • For x \in A, there is also y \in A with x < y (A has no greatest element).

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

Translating a Dedekind cut to a CSR is straightforward. We set the terms of the sequence to be successive binary search approximations of \sup A, 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 A 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 y for which there exists some rational \epsilon > 0 and some natural N, such that for every n > N, y + \epsilon < x_n. (In particular, we set some \epsilon < \frac{1}{2}((\lim_{i \rightarrow \infty} x_i) - y), and N can be set so that successive terms are within \epsilon 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:

  • s : \mathbb{N} \rightarrow \mathbb{Q}
  • t : (\epsilon : \mathbb{Q}, \epsilon > 0) \rightarrow \mathbb{N}

Satisfying:

\forall (\epsilon : \mathbb{Q}, \epsilon > 0), (m: \mathbb{N}, m > t(\epsilon)), (n : \mathbb{N}, n > t(\epsilon)): |s(m) - s(n)| < \epsilon

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

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

  • a : \mathbb{Q} \rightarrow \mathbb{B}
  • b : \mathbb{Q}
  • c : \mathbb{Q}
  • d : (x : \mathbb{Q}, a(x) = \mathrm{True}) \rightarrow \mathbb{Q}

Where \mathbb{B} is the Boolean type. A corresponds to the set of rationals for which a is true. The triple must satisfy:

  • a(b) = \mathrm{True}
  • a(c) = \mathrm{False}
  • \forall (x : \mathbb{Q}, a(x) = \mathrm{True}): d(x) > x \wedge a(d(x)) = \mathrm{True}
  • \forall (x,y : \mathbb{Q}, x < y, a(y) = \mathrm{True}): a(x) = \mathrm{True}

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

Let’s first consider translating Dedekind cuts to CSRs. We can use b and c 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 t.

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 M be a Turing machine that does not necessarily halt, but returns a Boolean if it does halt. Let f(M) be equal to 0 if M doesn’t halt; if M halts in exactly n steps returning a boolean b, then, if b is true, f(M) = 1/n, and if b is false, then f(M) = -1/n.

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

This sequence is (constructively) Cauchy since all terms past i are within 2/i of each other. This makes a valid t for the Cauchy sequence computable (we simply need t(\epsilon) > 2/\epsilon).

On the other hand, f cannot be represented as a function returning a Dedekind cut. Suppose a(M) represents the A set for the Dedekind cut of f(M). We will specify g : M \rightarrow \mathbb{B} to be an arbitration oracle, by setting g(M) = a(M)(0). This is an arbitration oracle by cases:

  • If M doesn’t halt, then the arbitration oracle can return anything.
  • If M halts and returns true, then the arbitration oracle must return true. Since f(M) > 0 in this case, we must have a(M)(0) = \mathrm{True}, so g(M) is correct in this case.
  • If M halts and returns false, then the arbitration oracle must return false. Since f(M) < 0 in this case, we must have a(M)(0) = \mathrm{False}, so g(M) is correct in this case.

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

Conclusion

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.

Published by Jessica Taylor

Leave a comment