nLab Eudoxus real number

Contents

Contents

Idea

Eudoxus real number refers to a construction of the ordered field of real numbers discovered by Stephen Schanuel. The idea is that every real number rr can be represented by a relation on the integers that is “almost linear”, e.g., the function that takes an integer nn to the floor of rnr n. Schanuel named this after Eudoxus, who developed a theory of magnitude and proportion to account for the relations between the discrete and the continuous1.

Definition

A function f:f: \mathbb{Z} \to \mathbb{Z} is almost linear if the quantity f(m+n)f(m)f(n)f(m+n) - f(m) - f(n) taken over all m,nm, n \in \mathbb{Z} is bounded. Almost linear functions are closed under the pointwise abelian group operations inherited from \mathbb{Z} (i.e., f+gf + g, f-f), and are also closed under composition of functions.

Define an equivalence relation \sim on the set of almost linear functions AL()AL(\mathbb{Z}) by fgf \sim g if fgf - g is bounded. This equivalence relation respects the abelian group structure of AL()AL(\mathbb{Z}), and if fff \sim f', then for any gAL()g \in AL(\mathbb{Z}) we have gfgfg \circ f \sim g \circ f' and fgfgf \circ g \sim f' \circ g. We write [f][f] for the equivalence class of ff.

Definition

A Eudoxus real number is an equivalence class of AL()AL(\mathbb{Z}) under \sim.

The set of Eudoxus reals 𝔼AL()/\mathbb{E} \coloneqq AL(\mathbb{Z})/{\sim} becomes a commutative ring whose addition and multiplication are descended from ++ and \circ on AL()AL(\mathbb{Z}). Already one distributive law (f+f)g=fg+fg(f + f') \circ g = f \circ g + f' \circ g holds in AL()AL(\mathbb{Z}), so as soon as one proves multiplication on 𝔼\mathbb{E} is commutative, one gets distributivity on the other side.

A Eudoxus real [f][f] is deemed positive if it is represented by an ff such that for any CC there are infinitely many mm \in \mathbb{N} such that f(m)>Cf(m) \gt C. It is easy to see this condition would then be satisfied by any representative function. As usual, define [f]<[g][f] \lt [g] to mean [gf][g-f] is positive.

Theorem

The commutative ring 𝔼\mathbb{E} equipped with <\lt is a complete ordered field.

A careful proof and exposition has been given by Arthan. The resulting construction is equivalent to the Cauchy reals; indeed for any almost linear function ff, the sequence f(n)/nf(n)/n is a Cauchy sequence of rationals that converges to the corresponding real number.

As an initial algebra

An endofunction f: f:\mathbb{Z}^\mathbb{Z} over the integers is bounded if

C.m.|f(m)|<C\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \vert f(m) \vert \lt C

and ff is almost linear if

C.m.n.|f(m+n)f(m)f(n)|<C\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \forall n \in \mathbb{Z}. \vert f(m + n) - f(m) - f(n) \vert \lt C

Let the set of almost linear endofunctions over the integers be defined as

AL(){f |C.m.n.|f(m+n)f(m)f(n)|<C}AL(\mathbb{Z}) \coloneqq \{f\in \mathbb{Z}^\mathbb{Z} \vert \exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \forall n \in \mathbb{Z}. \vert f(m + n) - f(m) - f(n) \vert \lt C \}

Let us define a Eudoxus algebra as a set AA with a function ιA AL()\iota \in A^{AL(\mathbb{Z})} such that

fAL().gAL().(C.m.|f(m)g(m)|<C)(ι(f)=ι(g))\forall f \in AL(\mathbb{Z}). \forall g \in AL(\mathbb{Z}). (\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \vert f(m) - g(m) \vert \lt C) \implies (\iota(f) = \iota(g))

An Eudoxus algebra homomorphism between two Eudoxus algebras AA and BB is a function fB Af \in B^A such that

aAL().f(ι A(a))=ι B(a)\forall a \in AL(\mathbb{Z}). f(\iota_A(a)) = \iota_B(a)

The category of Eudoxus algebras is the category EudoxusAlgEudoxusAlg whose objects Ob(EudoxusAlg)Ob(EudoxusAlg) are Eudoxus algebras and whose morphisms Mor(EudoxusAlg)Mor(EudoxusAlg) are Eudoxus algebra homomorphisms. The set of Eudoxus real numbers, denoted \mathbb{R}, is defined as the initial object in the category of Eudoxus algebras.

As a quotient inductive type

Let the proposition that an endofunction f:f:\mathbb{Z} \to \mathbb{Z} over the integers is bounded be defined as follows:

isBounded(f) C: m:|f(m)|<CisBounded(f) \coloneqq \left\Vert \sum_{C:\mathbb{Z}} \prod_{m:\mathbb{Z}} \vert f(m) \vert \lt C \ \right\Vert

and let the proposition that ff is almost linear be defined as follows:

isAlmostLinear(f) C: m: n:|f(m+n)f(m)f(n)|<CisAlmostLinear(f) \coloneqq \left\Vert \sum_{C:\mathbb{Z}} \prod_{m:\mathbb{Z}} \prod_{n:\mathbb{Z}} \vert f(m + n) - f(m) - f(n) \vert \lt C \ \right\Vert

Let the type of almost linear endofunctions over the integers be defined as

AL() f:isAlmostLinear(f)AL(\mathbb{Z}) \coloneqq \sum_{f:\mathbb{Z} \to \mathbb{Z}} isAlmostLinear(f)

The type of Eudoxus real numbers, denoted as \mathbb{R}, is a higher inductive type generated by:

  • a function ι:AL()\iota: AL(\mathbb{Z}) \to \mathbb{R}

  • a dependent product of functions from propositions to identities:

η: f:AL() g:AL()isBounded(fg)(ι(f)=ι(g)) \eta : \prod_{f:AL(\mathbb{Z})} \prod_{g:AL(\mathbb{Z})} isBounded(f - g) \to (\iota(f) = \iota(g))
  • A set-truncator
    τ 0: a: b:isProp(a=b)\tau_0: \prod_{a:\mathbb{R}} \prod_{b:\mathbb{R}} isProp(a=b)

Remarks

In an exchange at the categories mailing list, Steve Schanuel says he got the idea from an old observation by John Tate on bilinear maps on \mathbb{Z}. The “attribution” to Eudoxus is best understood in the context of the footnote below. Particularly, it should not be thought that Eudoxus was ‘constructing’ the reals (whether of Dedekind type or Cauchy type) or constructing anything at all necessarily (rationals included), despite modern glosses on the spirit of Eudoxus’s theory of magnitude that suggest more of a kinship to Dedekind cuts, and despite the fact that ‘Eudoxus reals’ as described here are equivalent to Cauchy reals, not Dedekind reals. Mainly, Schanuel is observing that by following a path suggested by Eudoxus, one can get to the reals directly, bypassing the need for the rationals as an intermediate construction.

There was a discussion on this at the categories list.

See also

References

Schanuel‘s discovery was unpublished by him, but was first disseminated by:

  • Ross Street, An efficient construction of the real numbers, Gazette Australian Math. Soc. 12 (1985) 57-58 [pdf]

It was subsequently noted several times in the literature that Street’s sketch in that note on how to establish completeness isn’t quite right. Street of course acknowledged this and gave an updated account here, mentioning for example corrected versions (e.g., by Arthan; see below):

  • Ross Street, Update on the efficient reals, September 2003. (web)

  • James Douglas, Rony Kirollos, Ben Odgers, Ross Street and Nguyen Hanh Vo, The Efficient Real Numbers, February 2004 (web)

Scattered remarks by Street, Michael Barr, and Stephen Schanuel may be found at the categories list,

The quote attributed to Schanuel (see the footnote) was drawn from that thread.

A correct and fairly comprehensive account of the construction is by Arthan, who includes some useful historical material:

A blog post on the Eudoxus real numbers:


  1. Quoting Schanuel: “Eudoxus noted that to measure the ratio of a line segment to another with any desired accuracy, it isn’t necessary to cut either of them up – instead multiply the ‘numerator’ segment by a large integer – thus pointing the way to a direct construction of the reals as ring from the integers as mere additive group.”

Last revised on July 5, 2024 at 21:51:00. See the history of this page for a list of all contributions to it.