Posts

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,isuc1, \suc, \isuc, where suc(a)=1+a\suc(a)=1+a and isuc(a)=1suc(a)=11+a\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