11.1 The field of rational numbers

We first construct the rational numbers $\mathbb{Q}$, as the reals can then be seen as a completion of $\mathbb{Q}$. An expert will point out that $\mathbb{Q}$ could be replaced by any approximate field, i.e., a subring of $\mathbb{Q}$ in which arbitrarily precise approximate inverses exist. An example is the ring of dyadic rationals, which are those of the form $n/2^k$. If we were implementing constructive mathematics on a computer, an approximate field would be more suitable, but we leave such finesse for those who care about the digits of $\pi$.

We constructed the integers $\mathbb{Z}$ in sec:set-quotients as a quotient of $\mathbb{N}\times \mathbb{N}$, and observed that this quotient is generated by an idempotent. In sec:free-algebras we saw that $\mathbb{Z}$ is the free group on $\mathrm{𝟏}$; we could similarly show that it is the free commutative ring on $\mathrm{𝟎}$. The field of rationals $\mathbb{Q}$ is constructed along the same lines as well, namely as the quotient

$$\mathbb{Q}:\equiv (\mathbb{Z}\times \mathbb{N})/\approx$$

where

$$(u,a)\approx (v,b):\equiv (u(b+1)=v(a+1)).$$

In other words, a pair $(u,a)$ represents the rational number $u/(1+a)$. There can be no division by zero because we cunningly added one to the denominator $a$. Here too we have a canonical choice of representatives, namely fractions in lowest terms. Thus we may apply lem:quotient-when-canonical-representatives to obtain a set $\mathbb{Q}$, which again has a decidable equality.

We do not bother to write down the arithmetical operations on $\mathbb{Q}$ as we trust our readers know how to compute with fractions even in the case when one is added to the denominator. Let us just record the conclusion that there is an entirely unproblematic construction of the ordered field of rational numbers $\mathbb{Q}$, with a decidable equality and decidable order. It can also be characterized as the initial ordered field.

Let ${\mathbb{Q}}_{+}=q:\mathbb{Q}|q>0$ be the type of positive rational numbers.

Title	11.1 The field of rational numbers