数学の始まりとして、論理と集合・クラスの基礎を整備します。
bではRussellのパラドクスも一つの定理として紹介されます。
a
一階論理の記号、2項述語
\(\mathbb{W}\)(,p) … \(\top\) \({\perp}\)\(\mathbb{W}\)(p,p) … \(\neg\)
\(\mathbb{W}\)(pp,p) … \(,\) \(\mathbin{\rm o\!r}\) \(\Rightarrow\) \(\Leftrightarrow\)
\(\mathbb{W}_{++}\)(pp,p) … \(\Longrightarrow\) \(\Longleftrightarrow\)
\(\mathbb{W}\)(vp,p)R … \(\forall\) \(\exists\)
\(\mathbb{W}\)(ss,p) … \(\in\) \(\subset\) \(=\)
abbr … \(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \mathop{{\sf A}} , \cdots , x_{\tt n} \mathop{{\sf A}} \Longrightarrow ( P ) )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} \mathop{{\sf A}} , \cdots , x_{\tt n} \mathop{{\sf A}} , ( P ) )\)
abbr … \(X_{1} \mathbin{{\sf p}} X_{2} \cdots \mathbin{{\sf p}} X_{\tt n}\) ≈ \(( X_{1} \mathbin{{\sf p}} X_{2} ) , \cdots , ( X_{\tt n\,{\text -}\,1} \mathbin{{\sf p}} X_{\tt n} )\)
\(\mathbb{W}_{++}\)(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
lower … \(A \stackrel{{\tt /}}{\mathbin{{\sf p}}} B\) ≃ \(\neg ( A \mathbin{{\sf p}} B )\)
内包記法
\(\mathbb{W}_+\)(vp,c)F … \(\mathsf{cls}\)abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)
abbr … \(\{ x \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , ( P ) \}\)
以下の左辺では \(\mathop{{\sf X}}\) が表記上無視されます。
abbr … \(\{ T \mid P \}\) ≈ \(\{ x \mid \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
「(クラスの)元である」という関係が重要です。Mathelでは「p-Formへの代入」も記述できます。
\(\mathbb{W}_+\)(sc,p) … \(\in\)
cvt … \(X \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(X\) を代入したもの
例 \(Y \in \{ X \mid x \in X \}\) ≃ \(x \in Y\)
2項述語の定義
\(\mathbb{W}_+\)(cc,p) … \(\subset\) \(=\)⊂_. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
集合は自然にクラスと見なされます。
Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます。
例 \(x \in X\) ≃ \(x \in \{ x \mid x \in X \}\)
通常の教科書と逆で、この教科書では\(\subset\)の定義が\(\subset\)の定義から誘導されます。
⊂. … \(X \subset Y \Longleftrightarrow X \subset Y\)
次の\(\Longleftarrow\)は外延性公理と呼ばれます。
=. … \(X = Y \Longleftrightarrow X = Y\)
=.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
一意の量化子
\(\mathbb{W}_+\)(vp,p)R … \(!\) \(\exists!\)！. … \(! x P \Longleftrightarrow \forall y , z \in \{ x \mid P \} . y = z\)
∃！. … \(\exists! x P \Longleftrightarrow \exists x P , ! x P\)
abbr … \(! x \mathop{{\sf A}} . P\) ≈ \(! x ( x \mathop{{\sf A}} , ( P ) )\)
abbr … \(\exists! x \mathop{{\sf A}} . P\) ≈ \(\exists! x ( x \mathop{{\sf A}} , ( P ) )\)
b
宇宙、空集合
\(\mathbb{W}_+\)(,c) … \(\mathbb{V}\)\V. … \(\mathbb{V} = \{ x \mid \top \}\)
\(x \in \mathbb{V}\) \(\blacktriangleleft\) O
\(X \subset \mathbb{V}\) \(\blacktriangleleft\) O
\(\mathbb{W}\)(,s) … \(\emptyset\)
∅. … \(\emptyset = \{ x \mid {\perp} \}\)
\(x \notin \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(\emptyset \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
∅.. … \(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\) \(\blacktriangleleft\) \(\mathbb{W}.\)
集合となるクラス
クラスが集合となるか、が議論されます。\(\mathbb{W}_+\)(c,p) … \(\dot\exists\)
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)
集合の部分クラスは集合である、ことが要請されます。これが公理 ax_s0 です。
ax_s0 … \(\exists X \, C \subset X \Longrightarrow \dot\exists C\)
(大きすぎて)集合になれないクラスは固有クラスと呼ばれます。最初の例はRusselクラスです。
\(\mathbb{W}_+\)(,c) … \(\mathbb{V}_0\)
\V0. … \(\mathbb{V}_0 = \{ x \mid x \notin x \}\)
\(\neg \dot\exists \mathbb{V}_0\) \(\blacktriangleleft\) O
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\) ax_s0
外延記法
指定した元だけを持つ集合を作ります。1以上の自然数 \({\tt n}\) に対して\(\mathbb{W}\)(s\(^{\tt n}\),s)F … \(\mathsf{set}_{\tt n}\)
abbr … \(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈ \(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\)
set\({\tt n}\). … \(\{ x_{1} , \cdots , x_{\tt n} \} = \{ v \mid v = x_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} v = x_{\tt n} \}\)
c
合併、共通部分、差
\(\mathbb{W}\)(ss,s) … \(\cup\) \(\cap\) \(\mathop\setminus\)∪. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
∩. … \(X \cap Y = \{ x \mid x \in X , x \in Y \}\)
∖. … \(X \mathop\setminus Y = \{ x \mid x \in X , x \notin Y \}\)
\(X \subset Y \Longleftrightarrow X \cup Y = Y \Longleftrightarrow X \cap Y = X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
総合併、総共通部分
\(\mathbb{W}\)(s,s)R … \(\bigcup\) \(\bigcap\)\(\mathbb{W}_+\)(c,c) … \(\bigcap\)
⋃. … \(\bigcup \mathcal{X} = \{ x \mid \exists X \in \mathcal{X} . x \in X \}\)
⋂. … \(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \{ x \mid \forall X \in \mathcal{X} . x \in X \}\)
\(X = \bigcup \{ X \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(X = \bigcap \{ X \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(X \cup Y = \bigcup \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(X \cap Y = \bigcap \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
冪集合
\(\mathbb{W}\)(s,s) … \(\wp\)℘. … \(\wp X = \{ A \mid A \subset X \}\)
wp0 … \(\wp \emptyset = \{ \emptyset \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
wp1 … \(\wp \{ x \} = \{ \emptyset , \{ x \} \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
hidden Prop として wp.' を作る。
査読でPrfを表示したときには見せる。
b2-2 いくつか◀Oに
一番下の定理 ax_s0◀に