11.1 The field of rational numbers

We first construct the rational numbers $\mathbb{Q}$, as the reals can then be seen as a completionof $\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 inversesexist. An example is thering 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 thosewho 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. Insec:free-algebras we saw that $\mathbb{Z}$ is the free group on $\mathrm{𝟏}$; we could similarlyshow that it is the free commutative ring on $\mathrm{𝟎}$. The field of rationals $\mathbb{Q}$ isconstructed 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 beno division by zero because we cunningly added one to the denominator $a$. Here too wehave a canonical choice of representatives, namely fractions in lowest terms. Thus we mayapply lem:quotient-when-canonical-representatives to obtain a set $\mathbb{Q}$, whichagain has a decidable equality.

We do not bother to write down the arithmetical operations on $\mathbb{Q}$ as we trust our readersknow 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 ofthe 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.