2
ZFCで遊ぼう！（１）
146
1
この著者は初心者として投稿しています。間違いや考慮が足りていない点が含まれている可能性が高いです。見つけたらコメント欄で優しく指摘してあげましょう。
$$$$
はじめに
こんにちは、ここではAAGと名乗ってます。
ZFCを厳密に扱っていろんなものを作ってみたいと思いました。
第一回である今回は自然数を作ります。
無限公理で十分？
大体の場合、無限公理は「自然数全体の集合が存在する」と理解されることがあります（要出典）
ただし注意すべき点として、外延性の公理を用いても無限公理は一つの集合を定めません。
というのも無限公理で言及される集合は各要素の条件について定めておらず、$\varnothing$があることと、各要素に後者が存在するというだけです。
そのため、条件を満たす、好きなだけ大きな集合を考えられます。
しかし、自然数全体の集合はその条件を満たす最小の集合ですよね。
今回はそういう意味で「自然数全体の集合の存在」を示したいと思います。
（ノイマン型）自然数の存在
2024/02/05 追記
英語版Wikipedia
にほぼ同じ内容があったので参考文献に載せました
以下
$\phi(N) = (\exists e\in N \ \forall z\ z\notin e) \land \forall x\in N\ \exists s\in N\ \forall z(z\in s \Leftrightarrow(z \in x \lor z=x))$
とおく
自然数の存在
$$\exists N(\phi(N)\land\forall X(\phi(X)\Rightarrow \forall x\in N\ x\in X))$$
(行間ひっどい概要)
無限公理を満たす$N_1$が存在する。（2）
$N=\lbrace x\in N_1 \ |\ \forall A(\phi(A) \Rightarrow x\in A)\rbrace$とおくと（5）、
$\phi(N)$であり（103）、
$\phi(X)$を満たす$X$について、$N\subset X$（115）
| 番号 | 内容 | 式 |
|---|---|---|
| 1 | 無限公理 | $\exists N\ \phi(N)$ |
| 2 | 仮定 | $\phi(N_1)$ |
| 3 | 分出公理 | $\forall x\exists y\forall z(z\in y\Leftrightarrow z\in x\land \forall w(\phi(w)\Rightarrow z\in w))$ |
| 4 | ∀E(3) | $\exists y\forall z(z\in y\Leftrightarrow z\in N_1\land \forall w (\phi(w)\Rightarrow z\in w))$ |
| 5 | 仮定 | $\forall z(z\in N\Leftrightarrow z\in N_1\land \forall w (\phi(w)\Rightarrow z\in w))$ |
| 6 | ∧E(2) | $\exists e\in N_1 \ \forall z\ z\notin e$ |
| 7 | 仮定 | $e_1\in N_1\land\forall z\ z\notin e_1$ |
| 8 | ∧E(7) | $\forall z\ z\notin e_1$ |
| 9 | ∀E(8) | $z_1\notin e_1$ |
| 10 | 仮定 | $\phi(w_1)$ |
| 11 | ∧E(10) | $\exists e\in w_1 \ \forall z\ z\notin e$ |
| 12 | 仮定 | $e_2\in w_1\land\forall z\ z\notin e_2$ |
| 13 | ∧E(12) | $\forall z\ z\notin e_2$ |
| 14 | ∀E(13) | $z_1\notin e_2$ |
| 15 | 仮定 | $z_1\in e_1$ |
| 16 | ￢E(15,9) | $\bot$ |
| 17 | ⊥(16) | $z_1 \in e_2$ |
| 18 | ⇒I(15-17) | $z_1\in e_1\Rightarrow z_1\in e_2$ |
| 19 | 仮定 | $z_1\in e_2$ |
| 20 | ￢E(19,14) | $\bot$ |
| 21 | ⊥(20) | $z_1 \in e_1$ |
| 22 | ⇒I(19-21) | $z_1\in e_2\Rightarrow z_1\in e_1$ |
| 23 | ∧I(22,18) | $z_1\in e_2\Leftrightarrow z_1\in e_1$ |
| 24 | ∀I(23) | $\forall z (z\in e_2\Leftrightarrow z\in e_1)$ |
| 25 | 外延性の公理 | $\forall x\forall y((\forall z (z\in x\Leftrightarrow z\in y))\Rightarrow x=y)$ |
| 26 | ∀E(25) | $\forall y((\forall z (z\in e_2\Leftrightarrow z\in y))\Rightarrow e_2=y)$ |
| 27 | ∀E(26) | $(\forall z (z\in e_2\Leftrightarrow z\in e_1))\Rightarrow e_2=e_1$ |
| 28 | ⇒E(24,27) | $e_2=e_1$ |
| 29 | 等号の代入 | $\forall x\forall y(x=y\Rightarrow(x\in w_1\Rightarrow y\in w_1))$ |
| 30 | ∀E(29) | $\forall y(e_2=y\Rightarrow(e_2\in w_1\Rightarrow y\in w_1))$ |
| 31 | ∀E(30) | $e_2=e_1\Rightarrow(e_2\in w_1\Rightarrow e_1\in w_1)$ |
| 32 | ⇒E(28,31) | $e_2\in w_1\Rightarrow e_1\in w_1$ |
| 33 | ∧E(12) | $e_2\in w_1$ |
| 34 | ⇒E(33,32) | $e_1\in w_1$ |
| 35 | ∃E(11,12-34) | $e_1\in w_1$ |
| 36 | ⇒I(10-35) | $\phi(w_1)\Rightarrow e_1\in w_1$ |
| 37 | ∀I(36) | $\forall w(\phi(w)\Rightarrow e_1\in w)$ |
| 38 | ∧E(7) | $e_1\in N_1$ |
| 39 | ∧I(37,38) | $e_1\in N_1\land \forall w (\phi(w)\Rightarrow e_1\in w)$ |
| 40 | ∀I(5) | $e_1\in N\Leftrightarrow e_1\in N_1\land \forall w (\phi(w)\Rightarrow e_1\in w)$ |
| 41 | ∧E(40) | $e_1\in N_1\land \forall w(\phi(w)\Rightarrow e_1\in w)\Rightarrow e_1\in N$ |
| 42 | ⇒E(39,41) | $e_1\in N$ |
| 43 | ∧I(42,8) | $e_1\in N\land \forall z\ z\notin e_1$ |
| 44 | ∃I(43) | $\exists e\in N\ \forall z\ z\notin e$ |
| 45 | ∃E(6,7-44) | $\exists e\in N\ \forall z\ z\notin e$ |
| 46 | 仮定 | $x_1\in N$ |
| 47 | 仮定 | $\phi(w_2)$ |
| 48 | ∀E(5) | $x_1\in N\Leftrightarrow x_1\in N_1\land \forall w (\phi(w)\Rightarrow x_1\in w)$ |
| 49 | ∧E(48) | $x_1\in N\Rightarrow x_1\in N_1\land \forall w (\phi(w)\Rightarrow x_1\in w)$ |
| 50 | ⇒E(46,49) | $x_1\in N_1\land \forall w (\phi(w)\Rightarrow x_1\in w)$ |
| 51 | ∧E(50) | $x_1\in N_1$ |
| 52 | ∧E(2) | $\forall x\in N_1\ \exists s\in N_1\ \forall z(z\in s \Leftrightarrow(z \in x \lor z=x))$ |
| 53 | ∀E(52) | $x_1\in N_1\Rightarrow \exists s\in N_1\ \forall z(z\in s \Leftrightarrow(z \in x_1 \lor z=x_1))$ |
| 54 | ⇒E(51,53) | $\exists s\in N_1\ \forall z(z\in s \Leftrightarrow(z \in x_1 \lor z=x_1))$ |
| 55 | 仮定 | $s_1\in N_1\land \forall z(z\in s _1\Leftrightarrow(z \in x_1 \lor z=x_1))$ |
| 56 | ∧E(50) | $\forall w (\phi(w)\Rightarrow x_1\in w)$ |
| 57 | ∀E(56) | $\phi(w_2)\Rightarrow x_1\in w_2$ |
| 58 | ⇒E(47,57) | $x_1\in w_2$ |
| 59 | ∧E(47) | $\forall x\in w_2\ \exists s\in w_2\ \forall z(z\in s \Leftrightarrow(z \in x \lor z=x))$ |
| 60 | ∀E(59) | $ x_1\in w_2\Rightarrow \exists s\in w_2\ \forall z(z\in s \Leftrightarrow(z \in x \lor z=x))$ |
| 61 | ⇒E(58,60) | $\exists s\in w_2\ \forall z(z\in s \Leftrightarrow(z \in x \lor z=x))$ |
| 62 | 仮定 | $s_2\in w_2\land \forall z(z\in s _2\Leftrightarrow(z \in x \lor z=x))$ |
| 63 | 仮定 | $z_2\in s_1$ |
| 64 | ∧E(55) | $\forall z(z\in s _1\Leftrightarrow(z \in x_1 \lor z=x_1))$ |
| 65 | ∀E(64) | $z_2\in s _1\Leftrightarrow(z_2 \in x_1 \lor z_2=x_1)$ |
| 66 | ∧E(65) | $z_2\in s _1\Rightarrow(z_2 \in x_1 \lor z_2=x_1)$ |
| 67 | ⇒E(63,66) | $z_2 \in x_1 \lor z_2=x_1$ |
| 68 | ∧E(62) | $\forall z(z\in s_2\Leftrightarrow(z \in x_1 \lor z=x_1))$ |
| 69 | ∀E(68) | $z_2\in s_2\Leftrightarrow(z_2 \in x_1 \lor z_2=x_1)$ |
| 70 | ∧E(69) | $(z_2 \in x_1 \lor z_2=x_1)\Rightarrow z_2\in s_2$ |
| 71 | ⇒E(67,70) | $z_2\in s_2$ |
| 72 | ⇒I(63-71) | $z_2\in s_1\Rightarrow z_2\in s_2$ |
| 73 | 仮定 | $z_2\in s_2$ |
| 74 | ∧E(69) | $z_2\in s_2\Rightarrow (z_2 \in x_1 \lor z_2=x_1)$ |
| 75 | ⇒E(73,74) | $z_2 \in x_1 \lor z_2=x_1$ |
| 76 | ∧E(65) | $(z_2 \in x_1 \lor z_2=x_1)\Rightarrow z_2\in s_1$ |
| 77 | ⇒E(75,76) | $z_2\in s_1$ |
| 78 | ⇒I(73-77) | $z_2\in s_2\Rightarrow z_2\in s_1$ |
| 79 | ∧I(78,72) | $z_2\in s_2\Leftrightarrow z_2\in s_1$ |
| 80 | ∀I(79) | $\forall z (z\in s_2\Leftrightarrow z\in s_1)$ |
| 81 | ∀E(25) | $\forall y((\forall z (z\in s_2\Leftrightarrow z\in y))\Rightarrow s_2=y)$ |
| 82 | ∀E(81) | $(\forall z (z\in s_2\Leftrightarrow z\in s_1))\Rightarrow s_2=s_1$ |
| 83 | ⇒E(80,82) | $s_1=s_2$ |
| 84 | 等号の代入 | $\forall x\forall y(x=y\Rightarrow(x\in w_2\Rightarrow y\in w_2))$ |
| 85 | ∀E(84) | $\forall y(s_2=y\Rightarrow(s_2\in w_2\Rightarrow y\in w_2))$ |
| 86 | ∀E(85) | $s_2=s_1\Rightarrow(s_2\in w_2\Rightarrow s_1\in w_2)$ |
| 87 | ⇒E(83,86) | $s_2\in w_2\Rightarrow s_1\in w_2$ |
| 88 | ∧E(62) | $s_2\in w_2$ |
| 89 | ⇒E(88,87) | $s_1\in w_2$ |
| 90 | ∃E(61,62-89) | $s_1\in w_2$ |
| 91 | ⇒I(47-90) | $\phi(w_2)\Rightarrow s_1\in w_2$ |
| 92 | ∀I(91) | $\forall w(\phi(w)\Rightarrow s_1\in w)$ |
| 93 | ∧E(55) | $s_1\in N_1$ |
| 94 | ∧I(93,92) | $s_1\in N_1\land \forall w(\phi(w)\Rightarrow s_1\in w)$ |
| 95 | ∀E(5) | $s_1\in N\Leftrightarrow s_1\in N_1\land \forall w (\phi(w)\Rightarrow s_1\in w)$ |
| 96 | ∧E(95) | $s_1\in N_1\land \forall w (\phi(w)\Rightarrow s_1\in w)\Rightarrow s_1\in N$ |
| 97 | ⇒E(94,96) | $s_1\in N$ |
| 98 | ∧I(97,64) | $s_1\in N\land\forall z(z\in s_1\Leftrightarrow(z \in x_1 \lor z=x_1))$ |
| 99 | ∃I(98) | $\exists s\in N\ \forall z(z\in s\Leftrightarrow(z \in x_1 \lor z=x_1))$ |
| 100 | ∃E(54,55-99) | $\exists s\in N\ \forall z(z\in s\Leftrightarrow(z \in x_1 \lor z=x_1))$ |
| 101 | ⇒I(46-100) | $x_1\in N\Rightarrow\exists s\in N\ \forall z(z\in s\Leftrightarrow(z \in x_1 \lor z=x_1))$ |
| 102 | ∀I(101) | $\forall x\in N\ \exists s\in N\ \forall z(z\in s\Leftrightarrow(z \in x \lor z=x))$ |
| 103 | ∧I(45,102) | $\phi(N)$ |
| 104 | 仮定 | $\phi(X)$ |
| 105 | 仮定 | $z_3\in N$ |
| 106 | ∀E(5) | $z_3\in N\Leftrightarrow z_3\in N_1\land \forall w (\phi(w)\Rightarrow z_3\in w)$ |
| 107 | ∧E(106) | $z_3\in N\Rightarrow z_3\in N_1\land \forall w (\phi(w)\Rightarrow z_3\in w)$ |
| 108 | ⇒E(105,107) | $z_3\in N_1\land \forall w (\phi(w)\Rightarrow z_3\in w)$ |
| 109 | ∧E(108) | $\forall w (\phi(w)\Rightarrow z_3\in w)$ |
| 110 | ∀E(109) | $\phi(X)\Rightarrow z_3\in X$ |
| 111 | ⇒E(104,110) | $z_3\in X$ |
| 112 | ⇒I(105-111) | $z_3\in N\Rightarrow z_3\in X$ |
| 113 | ∀I(112) | $\forall x\in N\ x\in X$ |
| 114 | ⇒I(104-113) | $\phi(X)\Rightarrow \forall x\in N\ x\in X$ |
| 115 | ∀I(114) | $\forall X(\phi(X)\Rightarrow \forall x\in N\ x\in X))$ |
| 116 | ∧I(103,115) | $\phi(N)\land\forall X(\phi(X)\Rightarrow \forall x\in N\ x\in X))$ |
| 117 | ∃I(116) | $\exists N(\phi(N)\land\forall X(\phi(X)\Rightarrow \forall x\in N\ x\in X))$ |
| 118 | ∃E(4,5-117) | $\exists N(\phi(N)\land\forall X(\phi(X)\Rightarrow \forall x\in N\ x\in X))$ |
| 119 | ∃E(1,2-118) | $\exists N(\phi(N)\land\forall X(\phi(X)\Rightarrow \forall x\in N\ x\in X))$ |
仮定のつながり
参考までに仮定の関係をまとめときます。
開いた仮定
公理のみから導いているものは省略した
| 番号 | 2 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 |
| 仮定 | 2 | 5 | 2 | 7 | 7 | 7 | 10 | 10 | 12 | 12 | 12 | 15 | 7,15 | 7,15 | 7 | 19 | 12,19 |
| 番号 | 21 | 22 | 23 | 24 | 28 | 32 | 33 | 34 | 35 | 36 | 37 | 38 | 39 | 40 |
| 仮定 | 12,19 | 12 | 7,12 | 7,12 | 7,12 | 7,12 | 12 | 7,12 | 7,10 | 7 | 7 | 7 | 7 | 5 |
| 番号 | 41 | 42 | 43 | 44 | 45 | 46 | 47 | 48 | 49 | 50 | 51 | 52 | 53 | 54 | 55 | 56 | 57 | 58 | 59 | 60 |
| 仮定 | 5 | 5,7 | 5,7 | 5,7 | 2,5 | 46 | 47 | 5 | 5 | 5,46 | 5,46 | 2 | 2 | 2,5,46 | 55 | 5,46 | 5,46 | 5,46,47 | 47 | 47 |
| 番号 | 61 | 62 | 63 | 64 | 65 | 66 | 67 | 68 | 69 | 70 | 71 | 72 | 73 | 74 | 75 | 76 | 77 | 78 | 79 | 80 |
| 仮定 | 5,46,47 | 62 | 63 | 55 | 55 | 55 | 55,63 | 62 | 62 | 62 | 55,62,63 | 55,62 | 73 | 62 | 62,73 | 55 | 55,62,73 | 55,62 | 55,62 | 55,62 |
| 番号 | 83 | 87 | 88 | 89 | 90 | 91 | 92 | 93 | 94 | 96 | 97 | 98 | 99 | 100 |
| 仮定 | 55,62 | 55,62 | 62 | 55,62 | 5,46,47,55 | 5,46,55 | 5,46,55 | 55 | 5,46,55 | 5 | 5,46,55 | 5,46,55 | 5,46,55 | 2,5,46 |
| 番号 | 101 | 102 | 103 | 104 | 105 | 106 | 107 | 108 | 109 | 110 | 111 | 112 | 113 | 114 | 115 | 116 | 117 | 118 |
| 仮定 | 2,5 | 2,5 | 2,5 | 104 | 105 | 5 | 5 | 5,105 | 5,105 | 5,105 | 5,104,105 | 5,104 | 5,104 | 5 | 5 | 2,5 | 2,5 | 2 |
閉じる場所
| 仮定 | 2 | 5 | 7 | 10 | 12 | 15 | 19 | 46 | 47 | 55 | 62 | 63 | 73 | 104 | 105 |
| 結論 | 119 | 118 | 45 | 36 | 35 | 18 | 23 | 101 | 91 | 100 | 90 | 72 | 78 | 114 | 112 |
おわりに
結構めんどくさかったけど、やりきることができてよかったです。
これからは、ZFCでノイマン型自然数を扱うとき119行を省略していることを認識して数学をしましょう。
ただ、今回は純粋な自然演繹を使って議論していたので冗長な部分も多くわかりにくかったと思います。
そのため、次回は環境を整えたりして、もっとわかりやすい方法でできたらと思います。
参考文献
投稿日：1月27日
更新日：2月4日
この記事を高評価した人
この記事を高評価した人
高評価したユーザはいません
この記事に送られたバッジ
この記事に送られたバッジ
バッジはありません。
投稿者
投稿者
AAG
28
6923
抽象代数学(群とか圏とか)が好きな高校3年生。気分屋です。
(元の名前:AGA)
Twitterではキャベツとして呟いてます
厳密にテキトーにやってます。
基本検算しません。
間違いがあったら容赦なく指摘してください。
コメント
コメント
他の人のコメント
コメントはありません。
読み込み中...
読み込み中