有理数は可算：自然数から有理数への全射を、\(k = 2^m(2n+1)\) の表し方を使って直接作る。
Isabelle の rat_denum と同じく、自然数から有理数への全射を直接作る。
\(k\) を \(2^m(2n+1)\) と表す方法が1通りであること（Linj）は使うが、どの \(k \neq 0\) もそう表せることは示さない。

1 準備

2の冪と奇数
\(2^a(2b+1)\) の形の表し方は1通り（Linj）。
Linj … \(a , b , c , d \in \mathbb{M} , 2 ^ a \cdot ( 2 \cdot b + 1 ) = 2 ^ c \cdot ( 2 \cdot d + 1 ) \Longrightarrow a = c , b = d\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄

2 自然数から有理数への全射の作成

2.1 整数と有理数

整数は自然数 \(n\) と \(-n\)、有理数は分数 \(a \div b\)（\(a\) は整数、\(b\) は 0 でない自然数）。
可算性には \(-\) と \(\div\) の性質（\(-0 = 0\) や約分など）は要らないので、何も仮定しません。
word(s,s) … \(-\)
word(ss,s) … \(/\)
word(,s) … \(\mathbb{Z}\)  \(\mathbb{Q}\)
ℤ. … \(\mathbb{Z} = \{ a \mid a \in \mathbb{M} \mathbin{\rm o\!r} \exists n \in \mathbb{M} . a = - n \}\)
ℚ. … \(\mathbb{Q} = \{ a / b \mid a \in \mathbb{Z} , b \in \mathbb{M} , b \neq 0 \}\)

2.2 主定理

word(ss,s) … \(\stackrel{\rm S}\to\)
→S. … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists x \, \langle x , y \rangle \in f \}\)
自然数 \(k\) を \(2^m(2n+1)\) と表し（表し方は1通り＝Linj）、\(m\) の偶奇で整数の符号を決めて、\(k\) に有理数 \(\pm i \div (n+1)\)（\(m = 2i\) なら \(+\)、\(m = 2i+1\) なら \(-\)）を対応させる。\(k = 0\) は \(0 \div 1\) に送る。
どの有理数 \(a \div b\) も、\(b = n+1\)、\(a = i\) なら \(m = 2i\)、\(a = -i\) なら \(m = 2i+1\) として値に現れるので、この対応は全射。
\(\exists f \, f \in \mathbb{M} \stackrel{\rm S}\to \mathbb{Q}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄