Generating the Rationals
An inductive definition of the positive rational numbers
3 min,
490 words
$ \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.