日記

補題 1.1.1　6項

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

補題 1.1.1

可算集合 $X$ の有限列全体 $X^{∪ω}$ も可算である．

(証明の方針)

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

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

$a_1,a_2,...,b_1,b_2,......：1つの自由変項$

$\mathbb{N}=\{1,2,...,n,n+1,......\}$

$∀k=［1,2,......,n］_{\mathbb{N}}$

$〈x_1,...,x_n〉：1つのn重対(有限列)$

$X^{∪ω}:=\displaystyle\bigcup_{k=1}^nX^k$

　まず，可算集合 $X$ として $\mathbb{N}$ を考える．このとき次のような関数が

①　 $f: \mathbb{N}→\displaystyle\bigcup_{k=1}^nX^k$ 　全射

あるいは

②　 $f: \displaystyle\bigcup_{k=1}^nX^k→\mathbb{N}$ 　単射

であることを示す．但し

$\displaystyle\bigcup_{k=1}^nX^k=\{x|∀k∀x［k∈\mathbb{N}→［x=〈x_1,...,x_n〉∈X^n］］\}$

関数 $f:I→X$ について

$f:I→X$ 　 $I$ から $X$ への関数

$i\mapsto f(i)$

$\{a_i\}_{i∈I}$ ：1つの集合族( $i∈I$ で添字付けられた列)

$f(i)=a_i=x$

に対して

$X^{i∈I}:=\{x|∀i∀x［i∈I→［f(i)=a_i=x∈X］］\}$ 　

$I$ から $X$ への関数全体の集合

と定める．

①について

$f:\mathbb{N}→\displaystyle\bigcup_{k=1}^nX^k$

$x\mapsto f(x)$

$f(x)=y$

とする．このとき

$\mathrm{Im} f=\displaystyle\bigcup_{k=1}^nX^k$ を示したい．

$\mathrm{Im}f:=\{y|∀y∃x［y∈\mathrm{Im} f→［f(x)=y∈X^{∪ω}］］\}⊂\displaystyle\bigcup_{k=1}^nX^k$

であるから

$\displaystyle\bigcup_{k=1}^nX^k ⊂\mathrm{Im}f$

を示せば十分である．すなわち

$∀y［y∈X^{∪ω}］\vdash ∀y［y∈X^{∪ω}→y∈\mathrm{Im}f］$

をいう．

1　(1)　 $∀y［y∈X^{∪ω}］$ 　　前提

1　(2)　 $y_1∈X^{∪ω}$ 　　1. ∀-除去

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

ここで， $\mathrm{Im} f$ の定義及び関数 $f(x)=y$ よりこの仮定は妥当である．

1　(4)　 $y_1∈X^{∪ω}→y_1∈\mathrm{Im}f$ 　　2-3. →-導入

1　(5)　 $∀y［y∈X^{∪ω}→y∈\mathrm{Im}f］$

　以上より， $f$ は全射であるから， $X^{∪ω}$ は可算集合である．

②について

$f: \displaystyle\bigcup_{k=1}^nX^k→\mathbb{N}$

$x\mapsto f(x)$

$f(x)=y$ 　　i.e.　 $∀x∃y［x∈X^{∪ω}→［f(x)=y∈\mathbb{N}］］$

とする．このとき

$∀s∀t［s≠t→f(s)≠f(t)］$

を示す．

　前提として $∀s∀t［s≠t］$ を表示し，そして∀-除去より $s_1≠t_1$ を仮定する．いま

$∃y=［u,v］_{\mathbb{N}}$ 　 $u_1≠v_1$

を選び

$f(s_1)=u_1$

$f(t_1)=v_1$

を考えれば，写像の一意性と仮定より

$f(s_1)≠f(t_1)$ 　☆

を得る．☆は∀-導入可能なので

$∀s∀t［s≠t→f(s)≠f(t)］$

が成立する．

補足

　たとえば記号 $A=B=C$ のとき，表示は

①　 $A$ のみ， $B$ のみ， $C$ のみ

②　 $A=B$ ， $A=C$ ， $B=C$

③　 $A=B=C$

という方法がある．物事の便宜に応じて使い分ける．