nLab Cauchy real number

Contents

Context

Analysis

Constructivism, Realizability, Computability

Contents

Idea

A Cauchy real number is a real number that is given as the limit of a Cauchy sequence of rational numbers. One may use this idea as a definition of the general concept of real number. This is due to Georg Cantor in 1872, the same year that Richard Dedekind developed Dedekind cuts as a definition of the same concept.

Definitions

If we simply want a construction of the real line \mathbb{R} for the purposes of classical mathematics, then we can use Cantor's original version. If we wish to use weak foundations or internalise the Cauchy real line, then there are subtler alternatives.

Classical version

Putting Cantor's definition in modern terminology, \mathbb{R} is the quotient set of the set of Cauchy sequences of rational numbers, with two sequences considered equivalent if their difference converges to zero. Although the notion of Cauchy sequence (and convergence, for that matter) is best known in the context of metric spaces (which cannot be defined in general without having, at least implicitly, constructed \mathbb{R} already), it is easy to state the definitions in elementary terms. (We can also view these as Cauchy sequences in a Booij premetric space.) If there is any tricky point, it is that the requirements made for all ϵ>0\epsilon \gt 0 need be made only for rational ϵ\epsilon. (We could also treat \mathbb{Q} as a uniform space or even a Cauchy space, although again to write down the definitions of those structures still requires one to handle the ϵ\epsilons.)

To be explicit: A Cauchy real number xx is an infinite sequence (x 0,x 1,x 2,)(x_0,x_1,x_2,\ldots) of rational numbers such that, for every positive rational number ϵ\epsilon, there exists a natural number α\alpha such that

|x ix j|ϵ {|x_i - x_j|} \leq \epsilon

holds whenever i,jαi,j \geq \alpha. Two Cauchy real numbers x,yx,y are considered equal if, for every positive rational number ϵ\epsilon, there exists a natural number α\alpha such that

|x iy i|ϵ {|x_i - y_i|} \leq \epsilon

holds whenever iαi \geq \alpha. It is easy to prove that this is an equivalence relation on the set of Cauchy sequences, so the set \mathbb{R} of real numbers is a quotient set.

This definition comes in two steps: one to identify the Cauchy sequences from among the infinite sequences, another to identify equivalent sequences. Actually, we can do this in one step by placing a partial equivalence relation on the set of all infinite sequences of rational numbers. Two sequences x,yx,y are considered equivalent if, for every positive rational number ϵ\epsilon, there exists a natural number α\alpha such that

|x iy j|ϵ {|x_i - y_j|} \leq \epsilon

holds whenever i,jαi,j \geq \alpha. It is immediate that a sequence xx is Cauchy if and only if it equivalent to itself, and it is easy to prove that two Cauchy sequences x,yx,y are equivalent if and only if they are equal as real numbers using the definition above. Thus, we can construct \mathbb{R} immediately as a subquotient of the function set \mathbb{Q}^{\mathbb{N}}.

Moduli of convergence

In weak foundations, we sometimes want to be a little more strict about how a sequence is Cauchy and how the difference of two such sequences converges to zero. We do this by requiring explicit moduli of convergence. These moduli can always be constructed using (for example) either countable choice or the principle of excluded middle, but the requirement makes a difference in (for example) a localic topos over any non-discrete space.

(Since the term ‘Cauchy real number’ is used ambiguously in the constructive literature, we can identify Cantor's classical definition above as a Cantor real number or a classical Cauchy real number.)

In general, a modulus of convergence may be any function α\alpha from the positive rational numbers to the natural numbers such that, for every natural number nn, there is a positive rational number ϵ\epsilon such that α(ϵ)n\alpha(\epsilon) \geq n.

A modulated Cauchy real number xx is an infinite sequence (x 0,x 1,x 2,)(x_0,x_1,x_2,\ldots) of rational numbers such that there exists a modulus α\alpha such that

|x ix j|ϵ {|x_i - x_j|} \leq \epsilon

holds whenever i,jα(ϵ)i,j \geq \alpha(\epsilon). Two modulated Cauchy real numbers x,yx,y are considered equal if there exists a modulus α\alpha such that

|x iy i|ϵ {|x_i - y_i|} \leq \epsilon

holds whenever iα(ϵ)i \geq \alpha(\epsilon). Again we can combine these conditions into a single partial equivalence relation: that there exists a modulus α\alpha such that

|x iy j|ϵ {|x_i - y_j|} \leq \epsilon

holds whenever i,jα(ϵ)i,j \geq \alpha(\epsilon).

Some variations are often met. A modulus α\alpha may be extended to all rational numbers, although the conditions above can only be required for positive ϵ\epsilon. Alternatively, it is enough to define α\alpha (and require the conditions) for ϵ\epsilon of specific form; common choices are 1/n1/n and 1/2 n1/2^n for nn a natural number, which work well with α(ϵ)=1/ϵ\alpha(\epsilon) = 1/\epsilon and α(ϵ)=log 2ϵ\alpha(\epsilon) = -\log_2\epsilon, respectively. (The important criterion is to use a detachable set of positive rational numbers of which zero is a limit point; then α\alpha can be extended from this set to all positive rational numbers by rounding down.)

It is also possible to fix a specific modulus α\alpha ahead of time. Then we need to treat each index separately, in this way: An α\alpha-regular Cauchy real number xx is an infinite sequence (x 0,x 1,x 2,)(x_0,x_1,x_2,\ldots) of rational numbers such that

|x ix j|δ+ϵ {|x_i - x_j|} \leq \delta + \epsilon

holds whenever iα(δ)i \geq \alpha(\delta) and jα(ϵ)j \geq \alpha(\epsilon). Two α\alpha-regular Cauchy real numbers are considered equal if

|x iy i|2ϵ {|x_i - y_i|} \leq 2\epsilon

holds whenever iα(ϵ)i \geq \alpha(\epsilon). Once more, we can combine these conditions into a single partial equivalence relation: that

|x iy j|δ+ϵ {|x_i - y_j|} \leq \delta + \epsilon

holds whenever iα(δ)i \geq \alpha(\delta) and jα(ϵ)j \geq \alpha(\epsilon).

Cauchy approximations

The modulated Cauchy real numbers could also be constructed through Cauchy approximations rather than sequences of rational numbers with a modulus of convergence. Let \mathbb{Q} be the rational numbers \mathbb{Q} and let

+{x|0<x}\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}

be the positive rational numbers.

As an initial algebra

Let us define a modulated Cauchy algebra to be a set AA with a function ιA C()\iota \in A^{C(\mathbb{Q})}, where C()C(\mathbb{Q}) is the set of Cauchy approximations in \mathbb{Q} and A C()A^{C(\mathbb{Q})} is the set of functions with domain C()C(\mathbb{Q}) and codomain AA, such that

aC().bC().(ϵ +.|a ϵb ϵ|<4ϵ)(ι(a)=ι(b))\forall a \in C(\mathbb{Q}). \forall b \in C(\mathbb{Q}). \left( \forall \epsilon \in \mathbb{Q}_{+}. \vert a_\epsilon - b_\epsilon \vert \lt 4 \epsilon \right) \implies (\iota(a) = \iota(b))

A modulated Cauchy algebra homomorphism is a function f:B Af:B^A between modulated Cauchy algebras AA and BB such that

aC().f(ι A(a))=ι B(a)\forall a \in C(\mathbb{Q}). f(\iota_A(a)) = \iota_B(a)

The category of modulated Cauchy algebras is the category MCAlgMCAlg whose objects Ob(MCAlg)Ob(MCAlg) are modulated Cauchy algebras and whose morphisms Mor(MCAlg)Mor(MCAlg) are modulated Cauchy algebra homomorphisms. The set of modulated Cauchy real numbers, denoted C\mathbb{R}_C, is defined as the initial object in the category of modulated Cauchy algebras.

As a quotient inductive type

The modulated Cauchy real numbers C\mathbb{R}_C are a quotient inductive type inductively generated by the following:

  • a function ι:C() C\iota: C(\mathbb{Q}) \to \mathbb{R}_C, where C()C(\mathbb{Q}) is the type of Cauchy approximations in \mathbb{Q}.

  • a dependent family of terms

    a:C(),b:C()eq C(a,b):( ϵ: +|a ϵb ϵ|<4ϵ)(ι(a)= Cι(b))a:C(\mathbb{Q}), b:C(\mathbb{Q}) \vdash eq_{\mathbb{R}_C}(a, b): \left( \prod_{\epsilon:\mathbb{Q}_{+}} \vert a_\epsilon - b_\epsilon \vert \lt 4 \epsilon \right) \to (\iota(a) =_{\mathbb{R}_C} \iota(b))
  • a family of dependent terms

    a: C,b: Cτ(a,b):isProp(a= Cb)a:\mathbb{R}_C, b:\mathbb{R}_C \vdash \tau(a, b): isProp(a =_{\mathbb{R}_C} b)

This is the approach of Booij20

Generalisations

While requiring a modulus of convergence, even fixing the modulus of convergence, may be more restrictive, it is also possible to use a potentially more lax definition.

One way is to use multivalued functions from the natural numbers. A multivalued Cauchy real number xx is an entire relation between natural numbers and rational numbers such that, for every positive rational number ϵ\epsilon, there exists a natural number α\alpha such that, whenever i,jαi, j \geq \alpha,

|ab|ϵ {|a - b|} \leq \epsilon

holds for some a,ba,b such that x i,ax_{i,a} and x j,bx_{j,b} hold. Two multivalued Cauchy real numbers are considered equal if, for every positive rational number ϵ\epsilon, there exists a natural number α\alpha such that, whenever iαi \geq \alpha,

|ab|ϵ {|a - b|} \leq \epsilon

holds for some a,ba,b such that x i,ax_{i,a} and y i,by_{i,b} hold. The partial equivalence relation subsuming both conditions is that, for every positive rational number ϵ\epsilon, there exists a natural number α\alpha such that, whenever i,jαi,j \geq \alpha,

|ab|ϵ {|a - b|} \leq \epsilon

holds for some a,ba,b such that x i,ax_{i,a} and y j,by_{j,b}.

Another way is to use nets (also called ‘generalised sequences’). A generalised Cauchy real number xx is a net (x ν) ν:D(x_\nu)_{\nu\colon D} (where DD is any directed set of indices) of rational numbers such that, for every positive rational number ϵ\epsilon, there exists an index α\alpha in DD such that

|x ix j|ϵ {|x_i - x_j|} \leq \epsilon

holds whenever i,jαi,j \geq \alpha in DD. Two generalised Cauchy real numbers x,yx,y are considered equal if, for every positive rational number ϵ\epsilon, there exists an index α\alpha for xx and an index β\beta for yy such that

|x iy j|ϵ {|x_i - y_j|} \leq \epsilon

holds whenever iαi \geq \alpha and jβj \geq \beta. Actually, this is already a partial equivalence relation on all nets which subsumes both conditions.

Requiring a modulus of convergence would make no difference for either of these, since we would expect such a modulus to also to be either multivalued or given by a net, and these are easy to construct explicitly (even in constructive mathematics).

(Since the term ‘Cauchy real number’ logically applies just as well to these generalisations, we may speak of sequential real numbers for the classical or modulated version.)

Relations between these definitions

Classically, all of these definitions are equivalent. In fact, to prove their equivalence, we need only the following equivalent principles (cf. Booij 2020):

If we don't accept any of the above, then we still have these results:

Theorems

(constructive).

Given any modulus of convergence α\alpha, every α\alpha-regular Cauchy real number is a modulated Cauchy real number. Furthermore, any two α\alpha-regular real numbers are equal as α\alpha-regular real numbers if and only if they are equal as modulated Cauchy real numbers. Conversely, every modulated Cauchy real number is equal (as a modulated Cauchy real number) to some α\alpha-regular Cauchy real number.

Every modulated Cauchy real number is a classical Cauchy real number, and any two equal modulated Cauchy real numbers are equal as classical Cauchy real numbers.

Every classical Cauchy real number is a multivalued Cauchy real number, and any two equal classical Cauchy real numbers are equal as multivalued Cauchy real numbers.

Every multivalued Cauchy real number becomes a generalised Cauchy real number whose index set DD comes equipped with a surjection to the natural numbers. Furthermore, any two multivalued Cauchy real numbers are equal as multivalued Cauchy real numbers if and only if they are equal as generalised Cauchy real numbers. Conversely, any generalised Cauchy real number is equal (as a generalised Cauchy real number) to some multivalued Cauchy real number.

Every generalised Cauchy real number becomes a Dedekind real number in the usual way, defining lower and upper sets in terms of the order relation on generalised Cauchy real numbers. Furthermore, any two generalised Cauchy real numbers are equal as generalised Cauchy real numbers if and only if they are equal as Dedekind cuts. Conversely, any Dedekind cut is equal (as a Dedekind cut) to some generalised Cauchy real number.

Hence even in constructive mathematics, there are only three notions that we need consider: modulated Cauchy real numbers, classical Cauchy real numbers, and Dedekind real numbers; and there is a function from each of these to the next.

Just to be explicit, here are the missing converses:

Axioms

Every classical Cauchy real number is modulated, and any two equal Cauchy real numbers are equal as modulated Cauchy real numbers.

Every multivalued Cauchy real number is equal (as a multivalued Cauchy real number) to some classical Cauchy real number, and two classical Cauchy real numbers are equal if they are equal as multivalued Cauchy real numbers.

Most practitioners of both constructive mathematics and topos theory want to use the Dedekind real numbers. Without excluded middle or countable choice, the classical Cauchy real numbers are not very well behaved. The modulated Cauchy real numbers, however, do have their good points; for example, the fundamental theorem of algebra is simplest for them. They also make sense in predicative mathematics with function sets, whereas multivalued Cauchy reals require fullness and the Dedekind reals require powersets for their definitions.

On the other hand, even the (modulated) Cauchy real numbers are not necessarily Cauchy complete, i.e. a Cauchy sequence (even a modulated one) of Cauchy real numbers need not converge to another Cauchy real number (though it always does converge to a Dedekind real number, since the Dedekind real numbers are always Cauchy complete). The problem is that without enough countable choice, we cannot lift a (modulated) Cauchy sequence of (modulated Cauchy) real numbers to a Cauchy sequence of Cauchy sequences in order to “diagonalize” it; a countermodel is constructed by Lubarsky.

For non-modulated Cauchy sequences and reals, there are additional problems even if we assume representatives are already chosen. A modulated Cauchy sequence of modulated Cauchy sequences does converge to a modulated Cauchy sequence. Moreover, a modulated Cauchy sequence of classical Cauchy sequences, and a classical Cauchy sequence of modulated Cauchy sequences, both necessarily converge to a classical Cauchy sequence. But the results need not be modulated, and a classical Cauchy sequence of classical Cauchy sequences need not converge to a classical Cauchy sequence. In fact, Lubarsky shows that:

  • The generic classical Cauchy sequence, in the classifying topos of classical Cauchy sequences, is not modulated. Thus, we cannot prove that every classical Cauchy sequence is modulated. Hence, we cannot prove that a classical Cauchy sequence of modulated Cauchy sequences has a modulated limit (since a classical Cauchy sequence of rationals can be regarded as a classical Cauchy sequence of (constant) modulated Cauchy sequences).

  • The generic classical Cauchy sequence of classical Cauchy sequences, in the classifying topos of such, does not converge to a classical Cauchy sequence.

  • The generic modulated Cauchy sequence of classical Cauchy sequences, in the classifying topos of such, does not converge to a modulated Cauchy sequence.

(Actually, Lubarsky writes using Heyting-valued sets? on topological spaces rather than classifying toposes of propositional geometric theories, but it seems almost certain to me that his results can be rephrased as the above.)

Using locators

Let FF be an Archimedean ordered field. Every element of FF satisfies the axioms of a Dedekind cut with respect to the strict order relation of FF, and is thus a real number.

The Dedekind real numbers D\mathbb{R}_D are the terminal Archimedean ordered field, i.e. for any other Archimedean ordered field FF, there exists a unique strictly monotonic field homomorphism u F:F Cu_F:F \to \mathbb{R}_C. Since every ring homomorphism between fields is an injection, the Dedekind real numbers being the terminal Archimedean ordered field FF implies that every other Archimedean ordered field is a subfield of D\mathbb{R}_D via the unique ring homomorphism u F:F Du_F:F \to \mathbb{R}_D:

F.isAOField(F)(F D)\forall F.\mathrm{isAOField}(F) \Rightarrow (F \subseteq \mathbb{R}_D)

In this sense, the Dedekind real numbers is the collection of all real numbers.

An element xFx \in F is a Cauchy real number if there exists a locator of xx. The Cauchy real numbers are the set of Dedekind real numbers x Dx \in \mathbb{R}_D where there exist a locator

C={x D|plocator(x)}\mathbb{R}_C = \{x \in \mathbb{R}_D \vert \exists p \in \mathrm{locator}(x)\}

Alternatively, if one doesn’t have the Dedekind real numbers, then one can still characterize the Cauchy real numbers by its universal property. The Cauchy real numbers C\mathbb{R}_C is the terminal Archimedean ordered field where for every element x Cx \in \mathbb{R}_C there exists a locator of xx: i.e. for any other Archimedean ordered field FF where for every element xFx \in F there exists a locator of xx, there exists a unique strictly monotonic field homomorphism u F:F Cu_F:F \to \mathbb{R}_C.

Since every ring homomorphism between fields is an injection, the Cauchy real numbers being the terminal Archimedean ordered field FF where for every element xFx \in F there exists a locator of xx implies that every other such Archimedean ordered field is a subfield of C\mathbb{R}_C via the unique ring homomorphism u F:F Cu_F:F \to \mathbb{R}_C:

F.(isAOField(F)xF.plocator(x))(F C)\forall F.\left(\mathrm{isAOField}(F) \wedge \forall x \in F.\exists p \in \mathrm{locator}(x)\right) \Rightarrow (F \subseteq \mathbb{R}_C)

In this sense, the Cauchy real numbers is the collection of all real numbers for which there exist a locator.

Either way, this definition makes sense in any Heyting category with exponential objects and a natural numbers object, even when the Heyting category is not a pretopos and the Cauchy real numbers cannot be constructed as a quotient set. In classical mathematics, one can prove that the Dedekind real numbers is a discrete field, which implies that the Cauchy real numbers and the Dedekind real numbers coincide.

In dependent type theory, the property that there exists a locator of xx is rendered as the bracket type of the type of locators of xx.

In addition, in constructive mathematics, the Cauchy real numbers C\mathbb{R}_C is not to be confused with the set of real numbers

= x Dlocator(x)\mathbb{R}^\mathcal{L} = \bigcup_{x \in \mathbb{R}_D} \mathrm{locator}(x)

which have as structure a locator. That the two notions coincide is equivalent to the WLPO, and is not provable in general.

Algebraic closure

The algebraic closure of the modulated Cauchy real numbers is the modulated Cauchy complex numbers; i.e. the fundamental theorem of algebra is true for the modulated Cauchy real numbers.

Generalisations

Although the notion of metric space doesn't make sense until we know what real numbers are, once we have these, we can recognise that the rational numbers form a metric space \mathbb{Q} and the real numbers were constructed from them in a way that makes reference only to the metric-space structure of \mathbb{Q}. Thus, this procedure may be generalised to any metric space to produce its completion.

We can also interpret \mathbb{Q} as a uniform space or even as a Cauchy space and define analogous notions of completion for these. However, these require us (in general) to use generalised Cauchy sequences, that is Cauchy nets, even in classical mathematics. (Of course, without excluded middle or countable choice, we should use nets even for metric spaces.)

Motivation

Suppose that we wish to approximate a real number xx by common fractions with arbitrarily large denominators. That is, given any natural number ii, we wish to find integers a ia_i such that x ia i/ix_i \coloneqq a_i/i is within 1/i1/i of xx. Then the sequence of values (0,x 1,x 2,x 3,)(0,x_1,x_2,x_3,\ldots) is an α\alpha-regular Cauchy real with α(1/i)i\alpha(1/i) \coloneqq i as modulus of convergence. (You can extend α\alpha to every positive rational number by α(ϵ)1/ϵ\alpha(\epsilon) \coloneqq \lfloor{1/\epsilon}\rfloor, but that is not important.) Conversely, given an α\alpha-regular Cauchy real (x 0,x 1,x 2,)(x_0,x_1,x_2,\ldots) for this modulus α\alpha, we can round each x ix_i (for i>0i \gt 0) to the nearest rational number with denominator ii (which can be done using only rational arithmetic) to produce an equal α\alpha-regular Cauchy real.

We might instead want to approximate xx by arbitrarily long decimal fractions. That is, given any natural number ii, we wish to find integers a ia_i such that x ia i/10 ix_i \coloneqq a_i/10^i is within 1/10 i1/10^i of xx. Now the sequence of values (x 0,x 1,x 2,)(x_0,x_1,x_2,\ldots) is an α\alpha-regular Cauchy real with α(1/10 i)i\alpha(1/10^i) \coloneqq i as modulus of convergence. Conversely, we can round off the values of any α\alpha-regular Cauchy real as before. Of course, there is nothing special about the base 1010 here; for theoretical purposes, base 22 is popular.

Thus, to define a real number to be an α\alpha-regular Cauchy real (for any of these choices of α\alpha) is to make into a definition our intuition that we can round real numbers in this way.

Note we may be rounding up or down, regardless of which is nearer. For example, in approximating e=exp1e = \exp\,1 by decimal fractions, we might get (2,2.7,2.71,)2,2.7,2.71,\ldots) or (3,2.7,2.72,)(3,2.7,2.72,\ldots), but we might also get (2,2.8,2.71,)(2,2.8,2.71,\ldots). To choose to always round down, towards zero, or towards the nearer approximant (with a rule for 0.50.5) requires an application of excluded middle (or at least the lesser limited principle of omniscience).

Even for Dedekind reals in neutral constructive mathematics, we can always approximate a real number in this way up to any given ii. Choice is needed only to make infinitely many approximations at once. Trying to avoid this can motivate multivalued Cauchy real numbers.

See also

References

See also the references at real number and constructive analysis.

Original articles:

Dicussion in constructive analysis:

The proof that Cauchy sequences (with a modulus of convergence) as such (i.e. not passing to their equivalence classes) are sequentially Cauchy complete:

See also

On why the (modulated) Cauchy real numbers, hence after passage to equivalence classes of Cauchy sequences, are not sequentially Cauchy complete (without the axiom of countable choice):

See also

A constructive algebraic proof of the fundamental theorem of algebra for the modulated Cauchy real numbers without countable choice:

  • Wim Ruitenberg, Constructing Roots of Polynomials over the Complex Numbers, Computational Aspects of Lie Group Representations and Related Topics, CWI Tract, Vol. 84, Centre for Mathematics and Computer Science, Amsterdam, 1991, pp. 107–128. (pdf)

Implementation of Bishop-style Cauchy real numbers in Agda:

review:

A novel construction principle of the type of real numbers, as a higher inductive-inductive type in univalent homotopy type theory, not reliant on representatives by sequences of rational numbers, and with provable Cauchy completeness even without extra axiom of countable choice is laid out (cf. HoTT book real numbers) in

but has not yet been implemented in any proof assistant,

Exposition and review:

Last revised on February 13, 2024 at 02:28:00. See the history of this page for a list of all contributions to it.