# 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 \autorefsec:set-quotients as a quotient of $\mathbb{N}\times \mathbb{N}$, and observed that this quotient is generated by an idempotent. In \autorefsec:free-algebras we saw that $\mathbb{Z}$ is the free group on $\mathrm{\U0001d7cf}$; we could similarly show that it is the free commutative ring on $\mathrm{\U0001d7ce}$. 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 \autoreflem: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}}_{+}=\text{setof}q:\mathbb{Q}|q>0$ be the type of positive rational numbers.

Title | 11.1 The field of rational numbers |
---|---|

\metatable |