### Constructing the Real Numbers as Nearly Multiplicative Sequences

#### Posted by Emily Riehl

I’m in Regensburg this week attending a workshop on Interactions of Proof Assistants and Mathematics. One of the lecture series is being given by John Harrison, a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services, and a lead developer of the HOL Light interactive theorem prover. He just told us about a very cool construction of the non-negative real numbers as sequences of natural numbers satisfying a property he calls “near multiplicativity”. In particular, the integers and the rational numbers aren’t needed at all! This is how the reals are constructed in HOL Light and is described in more detail in a book he wrote entitled *Theorem Proving with the Real Numbers*.

Edit: as the commenters note, these are also known as the Eudoxus reals and were apparently discovered by our very own Stephen Schanuel and disseminated by Ross Street. Thanks for pointing me to the history of this construction!

## The idea

One of the standard constructions of the real numbers is as equivalence classes of Cauchy sequences of rationals. Let us consider a non-negative real number $a$. One way to say that a sequence $q \colon \mathbb{N} \to \mathbb{Q}$ of rational numbers **converges** to $a$ is to ask there to exist a constant $A \in \mathbb{N}$ so that for all $n \in \mathbb{N}$,

$|q_n - a | \le \frac{A}{n}.$

These representations aren’t at all unique: many Cauchy sequences of rationals represent the same real number. And in particular, for any positive real number $a$, it is possible to find a sequence of natural numbers $a \colon \mathbb{N} \to \mathbb{N}$ so that the sequence $n \mapsto \frac{a_n}{n}$ converges to $a$ in the above sense, i.e.:

$|\frac{a_n}{n} - a | \le \frac{A}{n}$

or equivalently

$|a_n - n \cdot a | \le A.$

This sequence $a \colon \mathbb{N} \to \mathbb{N}$ will encode the real number $a$ (which is why I’ve given them the same name).

## The construction

Now that I’ve explained the idea let’s try to characterize the sequences of natural numbers that will correspond to non-negative real numbers without presupposing the existence of non-negative real numbers. The idea is that a sequence $a \colon \mathbb{N} \to \mathbb{N}$ will have the property that the sequence $n \mapsto \frac{a_n}{n}$ encodes some non-negative real number just when this sequence is Cauchy, which we express in the following way: there exists a constant $A \in \mathbb{N}$ so that for all $n,m \in \mathbb{N}$,

$|\frac{a_n}{n} - \frac{a_m}{m} | \le \frac{A}{n} + \frac{A}{m},$

or equivalently by

$|m \cdot {a_n} - n \cdot {a_m} | \le (m + n) \cdot A.$

Such sequences are called *nearly multiplicative*. Supposedly this is equivalent to the property of a sequence being *nearly additive*, meaning there exists a constant $A' \in \mathbb{N}$ so that for all $m,n \in \mathbb{N}$

$|a_{m+n} - (a_m + a_n)| \le A'.$

The non-negative reals are then equivalence classes of nearly multiplicative sequences of natural numbers, where the equivalence relation says that $a, a' \colon \mathbb{N} \to \mathbb{N}$ represent the same real number when there exists $C \in \mathbb{N}$ so that for all $n \in \mathbb{N}$

$|a_n - a'_n | \le C.$

This is more or less the usual equivalence relation of Cauchy sequences, except with a specified rate of convergence.

## Addition and multiplication

Now that we have the non-negative reals, how do we add and how do we multiply?

Given nearly multiplicative sequences $a \colon \mathbb{N} \to \mathbb{N}$ and $b \colon \mathbb{N} \to \mathbb{N}$, their sum $a + b \colon \mathbb{N} \to \mathbb{N}$ is defined by pointwise addition: $(a+b)_n := a_n + b_n$. This is fairly intuitive.

More interestingly, their product $a \cdot b \colon \mathbb{N} \to \mathbb{N}$ is defined by function composition: $(a \cdot b)_n := a_{b_n}$. It’s a fun exercise to work out that this converges to the desired non-negative real number.

## Re: Constructing the real numbers as nearly multiplicative sequences

I think these are the Eudoxus reals.