2
エンタメ議論
文献あり

ZFCで遊ぼう!(1)

146
1
$$$$

はじめに

こんにちは、ここではAAGと名乗ってます。
ZFCを厳密に扱っていろんなものを作ってみたいと思いました。

公理はZFC( こちらの記事 参照)
および、等号の公理( こちらの記事 参照)
推論は自然演繹( こちらのPDF を参照)を使います。
(∀E(3)は3に∀Eを適用させることを表すことにします。)
(∧I(1,2)は1,2に∧Iを適用させることを表すことにします。)
(⇒I(1-2)は1から2の証明に⇒Iを適用させることを表すことにします。)
(便宜上、¬の定義を¬I、¬に⇒Eを使うことを¬Eとします。)

ちなみに、だいぶ長いです。

第一回である今回は自然数を作ります。

無限公理で十分?

大体の場合、無限公理は「自然数全体の集合が存在する」と理解されることがあります(要出典)
ただし注意すべき点として、外延性の公理を用いても無限公理は一つの集合を定めません
というのも無限公理で言及される集合は各要素の条件について定めておらず、$\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))$

仮定のつながり

参考までに仮定の関係をまとめときます。

開いた仮定

公理のみから導いているものは省略した

番号2567891011121314151617181920
仮定2527771010121212157,157,1571912,19
番号2122232428323334353637383940
仮定12,19127,127,127,127,12127,127,1077775
番号4142434445464748495051525354555657585960
仮定55,75,75,72,54647555,465,46222,5,46555,465,465,46,474747
番号6162636465666768697071727374757677787980
仮定5,46,47626355555555,6362626255,62,6355,62736262,735555,62,7355,6255,6255,62
番号83878889909192939496979899100
仮定55,6255,626255,625,46,47,555,46,555,46,55555,46,5555,46,555,46,555,46,552,5,46
番号101102103104105106107108109110111112113114115116117118
仮定2,52,52,5104105555,1055,1055,1055,104,1055,1045,104552,52,52
閉じる場所
仮定25710121519464755626373104105
結論119118453635182310191100907278114112

おわりに

結構めんどくさかったけど、やりきることができてよかったです。
これからは、ZFCでノイマン型自然数を扱うとき119行を省略していることを認識して数学をしましょう。
ただ、今回は純粋な自然演繹を使って議論していたので冗長な部分も多くわかりにくかったと思います。
そのため、次回は環境を整えたりして、もっとわかりやすい方法でできたらと思います。

参考文献

投稿日:127
更新日:24
OptHub AI Competition

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。

投稿者

AAG
AAG
28
6826
抽象代数学(群とか圏とか)が好きな高校3年生。気分屋です。 (元の名前:AGA) Twitterではキャベツとして呟いてます 厳密にテキトーにやってます。 基本検算しません。 間違いがあったら容赦なく指摘してください。

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中