induction

$ \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.

Read More