カントールの対関数が全単射であること

新井敏康『数学基礎論(増補版)』 東京大学出版会 2021　

a,b,c,......：1つの束縛変数

A,B,C,......：1つの集合

とする．このとき

(n,m)\mapsto J(n,m)が全単射であること

を示す．

(証明の方針)

J:\mathbb{N}^2→\mathbb{N}

J(n,m):=\displaystyle\sum_{i≤n+m}i+m　　関数のかたち

A⊆\mathbb{N}^2

B⊆\mathbb{N}

\mathrm{Im}J:=\{y|∀y∃n∃m［y∈\mathrm{Im}J→［J(n,m)=y∈B］］\}⊆\mathbb{N}

とする．

①　 Jが全射であること

②　 Jが単射であること

①について

　 \mathrm{Im}J=\mathbb{N}を示したい．そのために

\mathbb{N}⊆\mathrm{Im}J

を示せば十分である．また，関数のかたちに注視すると

\displaystyle\sum_{i≤n+m}i∈\mathbb{N}

m∈\mathbb{N}

であり \mathbb{N}は加法で閉じているから

J(n,m)∈\mathbb{N}

と書けるので B:=\mathbb{N}と置くことができる．☆

これより

∀y［y∈\mathbb{N}］\vdash ∀y［y∈\mathbb{N}→y∈\mathrm{Im}J］

をいう．

1　(1)　 ∀y［y∈\mathbb{N}］　　前提

1　(2)　 y_1∈\mathbb{N}　　1. ∀-除去

3　(3)　 y_1∈\mathrm{Im}J　　仮定

☆によりこの仮定は妥当である．

1　(4)　 y_1∈\mathbb{N}→y_1∈\mathrm{Im}J　　2-3. →-導入

1　(5)　 ∀y［y∈\mathbb{N}→y∈\mathrm{Im}J］

②について

(n,m)≠(s,t)→J(n,m)≠J(s,t)　　( ∀n,m,s,t∈\mathbb{N})

を示す． (n,m)≠(s,t)を仮定する．関数 Jについて J(n,m)=yの値を

∃y=［u_1,u_2］_{\mathbb{N}}　s.t.　 u_1≠u_2

と選び

J(n,m)=u_1

J(s,t)=u_2

と表示すれば，写像の一意性と仮定から J(n,m)≠J(s,t)を得る．

　以上より Jは全単射である．