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 $r$ can be represented by a relation on the integers that is “almost linear”, e.g., the function that takes an integer $n$ to the floor of $r n$. Schanuel named this after Eudoxus?, who developed a theory of magnitude and proportion to account for the relations between the discrete and the continuous^{1}.
A function $f: \mathbb{Z} \to \mathbb{Z}$ is almost linear if the quantity $f(m+n) - f(m) - f(n)$ taken over all $m, n \in \mathbb{Z}$ is bounded. Almost linear functions are closed under the pointwise abelian group operations inherited from $\mathbb{Z}$ (i.e., $f + g$, $-f$), and are also closed under composition of functions.
Define an equivalence relation $\sim$ on the set of almost linear functions $AL(\mathbb{Z})$ by $f \sim g$ if $f - g$ is bounded. This equivalence relation respects the abelian group structure of $AL(\mathbb{Z})$, and if $f \sim f'$, then for any $g \in AL(\mathbb{Z})$ we have $g \circ f \sim g \circ f'$ and $f \circ g \sim f' \circ g$. We write $[f]$ for the equivalence class of $f$.
A Eudoxus real number is an equivalence class of $AL(\mathbb{Z})$ under $\sim$.
The set of Eudoxus reals $\mathbb{E} \coloneqq AL(\mathbb{Z})/\sim$ becomes a commutative ring whose addition and multiplication are descended from $+$ and $\circ$ on $AL(\mathbb{Z})$. Already one distributive law $(f + f') \circ g = f \circ g + f' \circ g$ holds in $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]$ is deemed positive if it is represented by an $f$ such that for any $C$ there are infinitely many $m \in \mathbb{N}$ such that $f(m) \gt C$. It is easy to see this condition would then be satisfied by any representative function. As usual, define $[f] \lt [g]$ to mean $[g-f]$ is positive.
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 $f$, the sequence $f(n)/n$ is a Cauchy sequence of rationals that converges to the corresponding real number.
An endofunction $f:\mathbb{Z}^\mathbb{Z}$ over the integers is bounded if
and $f$ is almost linear if
Let the set of almost linear endofunctions over the integers be defined as
Let us define a Eudoxus algebra as a set $A$ with a function $\iota \in A^{AL(\mathbb{Z})}$ such that
An Eudoxus algebra homomorphism between two Eudoxus algebras $A$ and $B$ is a function $f \in B^A$ such that
The category of Eudoxus algebras is the category $EudoxusAlg$ whose objects $Ob(EudoxusAlg)$ are Eudoxus algebras and whose morphisms $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.
Let the proposition that an endofunction $f:\mathbb{Z} \to \mathbb{Z}$ over the integers is bounded be defined as follows:
and let the proposition that $f$ is almost linear be defined as follows:
Let the type of almost linear endofunctions over the integers be defined as
The type of Eudoxus real numbers, denoted as $\mathbb{R}$, is a higher inductive type generated by:
a function $\iota: AL(\mathbb{Z}) \to \mathbb{R}$
a dependent product of functions from propositions to identities:
In an exchange at the categories 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.
Schanuel’s discovery was unpublished by him, but was first disseminated by Ross Street:
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 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:
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 September 22, 2023 at 20:17:46. See the history of this page for a list of all contributions to it.