Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: Constructive Cauchy sequences vs. Dedekind cuts, published by jessicata on March 15, 2024 on LessWrong.

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 constructive logic.

Cauchy sequences and Dedekind cuts in classical ZF

Classically, a Cauchy sequence is a sequence of reals x1,x2,…, such that for any ϵ>0, there is a natural N such that for any m,n>N, |xmxn|<ϵ. 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 xi 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 xN+1 as the approximation. We are assured that this approximation must be within ϵ of any future xi in the sequence; therefore, the approximation error (that is, |xN+1limixi|) will not exceed ϵ.

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 yA, then xA (A is downward closed).

For xA, there is also yA with x0 and some natural N, such that for every n > N, y+ϵ0)N

Satisfying:

(ϵ:Q,ϵ>0),(m:N,m>t(ϵ)),(n:N,n>t(ϵ)):|s(m)s(n)|<ϵ

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:QB

b:Q

c:Q

d:(x:Q,a(x)=True)Q

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

a(b)=True

a(c)=False

(x:Q,a(x)=True):d(x)>xa(d(x))=True

(x,y:Q,x