Generating the Rationals

$ \gdef\gcd{\mathrm{gcd}} \gdef\N{\mathbb{N}} \gdef\Q{\mathbb{Q}} \gdef\suc{\mathrm{suc}} \gdef\isuc{\mathrm{isuc}}$

Arnon Avron, who supervised my master's degree, once told me about a surprising little result that he had discovered. Paraphrasing:

Theorem. The positive rationals are freely generated by $1, \suc, \isuc$, where $\suc(a)=1+a$ and $\isuc(a)=\frac{1}{\suc(a)}=\frac{1}{1+a}$.

If someone asked me why we need quotients to do math, rational numbers would probably be the first example I give. So it is interesting that the positive rationals can be given as an inductive type.

I don't know how Arnon proved it, but here is my take on it. The theorem is a consequence of the following two lemmas.

Lemma (Canonicity). For every $q \in \Q_+$ one and only one of the following holds:

1. $q=1$.
2. There exists a unique $a \in \Q_+$ such that $q = \suc(a)$.
3. There exists a unique $a \in \Q_+$ such that $q = \isuc(a)$.

Proof. Let $q \in \Q_+$. If (1) holds, then $q=1$. If (2) holds, then $q>1$. If (3) holds, then $q<1$. Therefore, at most one of the clauses may hold.

To show that there is a clause that holds, we do case analysis on the ordering of $q$ relative to $1$:

1. If $q=1$ then (1) holds.
2. If $q>1$ then (2) holds by taking $a = q-1$. Uniqueness follows from the injectivity of $\suc$.
3. If $q<1$ then (3) holds by taking $a = \frac{1}{q}-q$. Uniqueness follows from the injectivity of $\isuc$. $\Box$

Lemma (Generation). For every $m,n \in \N_+$, if $n \in \N_+$ is coprime to $m$, then $\frac{n}{m}$ is generated by $1, \suc, \isuc$.

Proof. By (strong) induction on $m$. Let $n \in \N_+$. There exist $k \in \N$ and $r \in \N_{<m}$ such that $n = km + r$. If $r=0$ then $\frac{n}{m} = k = \suc^{k-1}(1)$. Otherwise, $\frac{n}{m} = k + \frac{r}{m} = \suc^k(\frac{r}{m}) = \suc^k(\isuc(\frac{m-r}{r}))$. So it suffices to show that $\frac{m-r}{r}$ is generated by $1, \suc, \isuc$. Denote $g := \gcd(m-r,m)$; $n' := \frac{m-r}{g}$; $m' := \frac{r}{g}$. Then $\frac{m-r}{r} = \frac{n'}{m'}$. Since $m' \leq r < m$, by the induction hypothesis $\frac{n'}{m'}$ is generated by $1, \suc, \isuc$, as required. $\Box$