数学の始まりとして、論理と集合・クラスの基礎を整備します。
bではRussellのパラドクスも一つの定理として紹介されます。
a
一階論理の記号、2項述語
\(\mathbb{W}_0\)(,p) … \(\top\) \({\perp}\)\(\mathbb{W}_0\)(p,p) … \(\neg\)
\(\mathbb{W}_0\)(pp,p) … \(,\) \(\mathbin{\rm o\!r}\) \(\Rightarrow\) \(\Leftrightarrow\) \(\Longrightarrow\) \(\Longleftrightarrow\)
\(\mathbb{W}_0\)(vp,p)R … \(\forall\) \(\exists\)
\(\mathbb{W}_0\)(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}_2\)(\({\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}_1\)(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}_1\)(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}_1\)(cc,p) … \(\subset\) \(=\)sub_. … \(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\)の定義から誘導されます。
sub. … \(X \subset Y \Longleftrightarrow X \subset Y\)
次の\(\Longleftarrow\)は外延性公理と呼ばれます。
=. … \(X = Y \Longleftrightarrow X = Y\)
=.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
一意の量化子
\(\mathbb{W}_1\)(vp,p)R … \(!\) \(\exists!\)am1. … \(! x P \Longleftrightarrow \forall y , z \in \{ x \mid P \} . y = z\)
exi!. … \(\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}_1\)(,c) … \(\mathbb{V}\)\V. … \(\mathbb{V} = \{ x \mid \top \}\)
\(x \in \mathbb{V}\) \(\blacktriangleleft\) O
\(X \subset \mathbb{V}\) \(\blacktriangleleft\) O
\(\mathbb{W}_0\)(,s) … \(\emptyset\)
\0. … \(\emptyset = \{ x \mid {\perp} \}\)
\(x \notin \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\emptyset \subset X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\0.. … \(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
集合となるクラス
クラスが集合となるか、が議論されます。\(\mathbb{W}_1\)(c,p) … \(\dot\exists\)
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)
集合の部分クラスは集合である、ことが要請されます。
\(\mathbb{W}_1\)(c,p) … \(\text{ax_s}\)
ax_s. … \(\text{ax_s} ( C ) \Longleftrightarrow \exists X \, C \subset X \Rightarrow \dot\exists C\)
\(\text{ax_s}({\tt C})\) (\({\tt C}\)はc-Form) という形の全てのPropの列を Ax_s とします。
(大きすぎて)集合になれないクラスは固有クラスと呼ばれます。最初の例はRusselクラスです。
\(\mathbb{W}_1\)(,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_s
外延記法
指定した元だけを持つ集合を作ります。1以上の自然数 \({\tt n}\) に対して\(\mathbb{W}_0\)(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}_0\)(ss,s) … \(\cup\) \(\cap\) \(\mathop\setminus\)cup. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
cap. … \(X \cap Y = \{ x \mid x \in X , x \in Y \}\)
dif. … \(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}_0.\)
総合併、総共通部分
\(\mathbb{W}_0\)(s,s)R … \(\bigcup\) \(\bigcap\)Cup. … \(\bigcup \mathcal{X} = \{ x \mid \exists X \in \mathcal{X} . x \in X \}\)
Cap. … \(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \{ x \mid \forall X \in \mathcal{X} . x \in X \}\)
\(X = \bigcup \{ X \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X = \bigcap \{ X \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \cup Y = \bigcup \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \cap Y = \bigcap \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
冪集合
\(\mathbb{W}_0\)(s,s) … \(\wp\)wp. … \(\wp X = \{ A \mid A \subset X \}\)
wp0 … \(\wp \emptyset = \{ \emptyset \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
wp1 … \(\wp \{ x \} = \{ \emptyset , \{ x \} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)