1 - a - test2.atp-research.com

一階論理から始め、集合・クラスの基本的な扱いまでを整備します。\(\dagger\)
集合・クラスについては「ZFとそのメタ」（あるいはNGB）に準拠します。
私たちのシステムは、例えば空集合公理の代わりとして\0というwordとその定義\0.を置きます。
集合をクラスとみなす仕組みも作られ、集合の関数をクラスの関数から誘導することもあります。\(\dagger\)

a1

命題記号、等号

word(,p) … \(\top\) \({\perp}\)
word(p,p) … \(\neg\)
word(pp,p) … \(,\) \({\bf ,}\) \(\mathbin{\rm o\!r}\) \(\Rightarrow\) \(\Longrightarrow\) \(\Leftrightarrow\) \(\Longleftrightarrow\)
word(ss,p) … \(=\)

2以上の自然数 \({\tt n}\) に対し
abbr … \(\begin{cases} P_{1} \\ \vdots \\ P_{\tt n} \end{cases}\) ≈ \(( P_{1} ) , \cdots , ( P_{\tt n} )\)
abbr … \( X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}\) ≈ \(X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}\)

abbr* … \( X\) ≈ \(X , X\)
abbr* … \( X\) ≈ \(X {\bf ,} \, X\)

二項記号の処理

word(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
cvt … \(A \stackrel{{\tt /}}{\mathop{{\sf p}}} B\) ≃ \(\neg ( A \mathop{{\sf p}} B )\)
word(\({\tt x}\)\({\tt y}\),\({\tt z}\)→\({\tt y}\)\({\tt x}\),\({\tt z}\)) … \(\leftrightarrow\)
cvt … \(A \stackrel{\leftrightarrow}{\mathop{{\sf p}}} B\) ≃ \(B \mathop{{\sf p}} A\)
word(\({\tt x}\)\({\tt x}\),\({\tt y}\)→\({\tt x}\),\({\tt y}\)) … \(\prime\prime\)
cvt … \(\stackrel{\prime\prime}{\mathop{{\sf p}}} A\) ≃ \(A \mathop{{\sf p}} A\)

二項記号の関数化
abbr … \(\mathop{{\sf f}} \stackrel{\star}{\mathop{{\sf a}}} \mathop{{\sf g}}\) ≈ \(\forall x \, ( \mathop{{\sf f}} x \mathop{{\sf a}} \mathop{{\sf g}} x )\)
abbr … \(\mathop{{\sf f}} \stackrel{\star\!\star}{\mathop{{\sf a}}} \mathop{{\sf g}}\) ≈ \(\forall x , y \, ( x \mathop{{\sf f}} y \mathop{{\sf a}} x \mathop{{\sf g}} y )\)

量化子

二項述語の一項述語

abbr … \(\mathop{{\sf p}} {:}\, \text{I}\) ≈ \(\forall x \, ( x \mathop{{\sf p}} x )\)
abbr … \(\mathop{{\sf p}} {:}\, \text{T}\) ≈ \(\forall x , y , z \, ( x \mathop{{\sf p}} y \mathop{{\sf p}} z \Longrightarrow x \mathop{{\sf p}} z )\)
abbr … \(\mathop{{\sf p}} {:}\, \text{X}\) ≈ \(\forall x , y \, ( x \mathop{{\sf p}} y \Longrightarrow y \mathop{{\sf p}} x )\)
次のようなabbrは自動で準備されます。
abbr … \(\mathop{{\sf p}} {:}\, \text{I} \text{T}\) ≈ \(\mathop{{\sf p}} {:}\, \text{I} , \mathop{{\sf p}} {:}\, \text{T}\)

\(= {:}\, \text{I} \text{T} \text{X}\) \(\blacktriangleleft\)

a2

クラス

word(vp,c) … cls
abbr … \(\{ x \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , ( P ) \}\)
abbr … \(_{ P } x\) ≈ \(\{ x \mid P \}\)

abbr … \(\{ T \mid P \}\) ≈ \(\{ x \mid \exists \mathop{{\sf X}} \, ( ( P ) , x = T ) \}\)
abbr … \(\{ T \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mathop{{\sf A}} \mid \exists \mathop{{\sf X}} \, ( ( P ) , x = T ) \}\)
abbr … \(_{ P } T\) ≈ \(\{ T \mid P \}\)

word(sc,p) … \(\in\)
cvt … \(X \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(X\) を代入したもの

inという関係、クラスの等号

word(ss,p) … \(\in\)
word(cc,p) … \(=\)
=_. … \(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}\}\) に置き換えられます。

=s ≅ =
=s. … \(= \stackrel{\star\!\star}{\Leftrightarrow} =\)

一意の量化子

word(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 ) )\)

アロー関数

word(vss,s) … fn
cvt … \([ x \mapsto X ] \, T\) ≃ \(T\) の \(x\) に \(X\) を代入したもの
\(\mapsto\) の前のv-Formを \(\bullet\) に替えられます。それが使用された時は \(\mapsto\) は略されます。
例　 \([ \bullet + a ]\) ≈ \([ x \mapsto x + a ]\)
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例　 \([ \bullet + [ \bullet + a ] x ]\) ≃ \([ \bullet + ( x + a ) ]\)

a3

a4

合併、共通部分、差

word(cc,c) … \(\cup\) \(\cap\)
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 \}\)
word(c,c) … \(\mathop\setminus\)
xs. … \(\mathop\setminus Y = \{ x \mid x \notin Y \}\)

word(ss,s) … \(\cup\) \(\cap\) \(\mathop\setminus\)
cup. … \(\cup \stackrel{\star\!\star}{=} \cup\)
cap. … \(x \in \bigcap \mathcal{X} \Longleftrightarrow \begin{cases} \exists X \, X \in \mathcal{X} \Rightarrow \forall X \in \mathcal{X} . x \in X \\ \not\exists X \, X \in \mathcal{X} \Rightarrow x \in \bigcap \mathcal{X} \end{cases}\)
dif. … \(X \mathop\setminus Y = X \cap ( \mathop\setminus Y )\)
\(X \subset Y \Longleftrightarrow X \cup Y = Y \Longleftrightarrow X \cap Y = X\) \(\blacktriangleleft\)

総合併、総共通部分

word(c,c) … \(\bigcup\) \(\bigcap\)
Cup_. … \(\bigcup \mathcal{X} = \{ x \mid \exists X \in \mathcal{X} . x \in X \}\)
Cap_. … \(\bigcap \mathcal{X} = \{ x \mid \forall X \in \mathcal{X} . x \in X \}\)
\(\bigcap \emptyset = \mathbb{V}\) \(\blacktriangleleft\)

word(s,s)R … \(\bigcup\) \(\bigcap\)
Cup. … \(\bigcup \stackrel{\star}{=} \bigcup\)
Cap.' … \(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)
\(X = \bigcup \{ X \}\) \(\blacktriangleleft\)
\(X = \bigcap \{ X \}\) \(\blacktriangleleft\)
\(X \cup Y = \bigcup \{ X , Y \}\) \(\blacktriangleleft\)
\(X \cap Y = \bigcap \{ X , Y \}\) \(\blacktriangleleft\)
\(X = \bigcup _{ x \in X } \{ x \}\) \(\blacktriangleleft\)

べき集合

word(s,s) … \(\wp\)
wp. … \(\wp X = \{ A \mid A \subset X \}\)
wp0 … \(\wp \emptyset = \{ \emptyset \}\) \(\blacktriangleleft\)
wp1 … \(\wp \{ x \} = \{ \emptyset , \{ x \} \}\) \(\blacktriangleleft\)

集合となるクラス、正則性公理

word(c,p) … \(\dot\exists\)
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)

word(,c) … \(\mathbb{V}_0\)
\V0. … \(\mathbb{V}_0 = \{ x \mid x \notin x \}\)
\(\neg \dot\exists \mathbb{V}_0\) \(\blacktriangleleft\)

ax_r' … \(\forall X \neq \emptyset . \exists Y \in X . X \cap Y = \emptyset\)
\(\mathbb{V}_0 = \mathbb{V}\) \(\blacktriangleleft\)

1 - a

a1