第一冊 第一部
1 a
\(\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\) \(\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 ) )\) 2 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} \}\) 3 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}.\)
Thm査読