The Nonlinear Library LW - Constructive Cauchy sequences vs. Dedekind cuts by jessicata
Mar 15, 2024
07:46
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 x It represents the real number supA. As with Cauchy sequences, we can approximate this number to within some arbitrary ϵ; we do this by doing a binary search to find rationals x Translating a Dedekind cut to a CSR is straightforward. We set the terms of the sequence to be successive binary search approximations of supA, 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 ϵ>0 and some natural N, such that for every n > N, y+ϵ 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:NQ
t:(ϵ:Q,ϵ>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 a specifies the sets A and B; b and c show that A...
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 x It represents the real number supA. As with Cauchy sequences, we can approximate this number to within some arbitrary ϵ; we do this by doing a binary search to find rationals x Translating a Dedekind cut to a CSR is straightforward. We set the terms of the sequence to be successive binary search approximations of supA, 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 ϵ>0 and some natural N, such that for every n > N, y+ϵ 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:NQ
t:(ϵ:Q,ϵ>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 a specifies the sets A and B; b and c show that A...