文献あり

ZFCで遊ぼう！（１）

181

この著者は初心者として投稿しています。間違いや考慮が足りていない点が含まれている可能性が高いです。見つけたらコメント欄で優しく指摘してあげましょう。

はじめに

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

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

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

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

無限公理で十分？

大体の場合、無限公理は「自然数全体の集合が存在する」と理解されることがあります（要出典）
ただし注意すべき点として、外延性の公理を用いても無限公理は一つの集合を定めません。
というのも無限公理で言及される集合は各要素の条件について定めておらず、 $\emptyset$ があることと、各要素に後者が存在するというだけです。
そのため、条件を満たす、好きなだけ大きな集合を考えられます。
しかし、自然数全体の集合はその条件を満たす最小の集合ですよね。
今回はそういう意味で「自然数全体の集合の存在」を示したいと思います。

（ノイマン型）自然数の存在

2024/02/05 追記　英語版Wikipedia にほぼ同じ内容があったので参考文献に載せました
以下
$ϕ (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 (ϕ (N) \land \forall X (ϕ (X) \Rightarrow \forall x \in N x \in X))$

(行間ひっどい概要)

無限公理を満たす $N_{1}$ が存在する。（2）
$N = {x \in N_{1} | \forall A (ϕ (A) \Rightarrow x \in A)}$ とおくと（5）、
$ϕ (N)$ であり（103）、
$ϕ (X)$ を満たす $X$ について、 $N \subset X$ （115）

番号	内容	式
1	無限公理	$\exists N ϕ (N)$
2	仮定	$ϕ (N_{1})$
3	分出公理	$\forall x \exists y \forall z (z \in y \Leftrightarrow z \in x \land \forall w (ϕ (w) \Rightarrow z \in w))$
4	∀E(3)	$\exists y \forall z (z \in y \Leftrightarrow z \in N_{1} \land \forall w (ϕ (w) \Rightarrow z \in w))$
5	仮定	$\forall z (z \in N \Leftrightarrow z \in N_{1} \land \forall w (ϕ (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	仮定	$ϕ (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)	$⊥$
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)	$⊥$
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)	$ϕ (w_{1}) \Rightarrow e_{1} \in w_{1}$
37	∀I(36)	$\forall w (ϕ (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 (ϕ (w) \Rightarrow e_{1} \in w)$
40	∀I(5)	$e_{1} \in N \Leftrightarrow e_{1} \in N_{1} \land \forall w (ϕ (w) \Rightarrow e_{1} \in w)$
41	∧E(40)	$e_{1} \in N_{1} \land \forall w (ϕ (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	仮定	$ϕ (w_{2})$
48	∀E(5)	$x_{1} \in N \Leftrightarrow x_{1} \in N_{1} \land \forall w (ϕ (w) \Rightarrow x_{1} \in w)$
49	∧E(48)	$x_{1} \in N \Rightarrow x_{1} \in N_{1} \land \forall w (ϕ (w) \Rightarrow x_{1} \in w)$
50	⇒E(46,49)	$x_{1} \in N_{1} \land \forall w (ϕ (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 (ϕ (w) \Rightarrow x_{1} \in w)$
57	∀E(56)	$ϕ (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)	$ϕ (w_{2}) \Rightarrow s_{1} \in w_{2}$
92	∀I(91)	$\forall w (ϕ (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 (ϕ (w) \Rightarrow s_{1} \in w)$
95	∀E(5)	$s_{1} \in N \Leftrightarrow s_{1} \in N_{1} \land \forall w (ϕ (w) \Rightarrow s_{1} \in w)$
96	∧E(95)	$s_{1} \in N_{1} \land \forall w (ϕ (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)	$ϕ (N)$
104	仮定	$ϕ (X)$
105	仮定	$z_{3} \in N$
106	∀E(5)	$z_{3} \in N \Leftrightarrow z_{3} \in N_{1} \land \forall w (ϕ (w) \Rightarrow z_{3} \in w)$
107	∧E(106)	$z_{3} \in N \Rightarrow z_{3} \in N_{1} \land \forall w (ϕ (w) \Rightarrow z_{3} \in w)$
108	⇒E(105,107)	$z_{3} \in N_{1} \land \forall w (ϕ (w) \Rightarrow z_{3} \in w)$
109	∧E(108)	$\forall w (ϕ (w) \Rightarrow z_{3} \in w)$
110	∀E(109)	$ϕ (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)	$ϕ (X) \Rightarrow \forall x \in N x \in X$
115	∀I(114)	$\forall X (ϕ (X) \Rightarrow \forall x \in N x \in X))$
116	∧I(103,115)	$ϕ (N) \land \forall X (ϕ (X) \Rightarrow \forall x \in N x \in X))$
117	∃I(116)	$\exists N (ϕ (N) \land \forall X (ϕ (X) \Rightarrow \forall x \in N x \in X))$
118	∃E(4,5-117)	$\exists N (ϕ (N) \land \forall X (ϕ (X) \Rightarrow \forall x \in N x \in X))$
119	∃E(1,2-118)	$\exists N (ϕ (N) \land \forall X (ϕ (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行を省略していることを認識して数学をしましょう。
ただ、今回は純粋な自然演繹を使って議論していたので冗長な部分も多くわかりにくかったと思います。
そのため、次回は環境を整えたりして、もっとわかりやすい方法でできたらと思います。