一階論理から始め、集合・クラスの基本的な扱いまでを整備します。\(\dagger\)
集合・クラスについては「ZFとそのメタ」（あるいはNGB）に準拠します。
当システムは、例えば空集合公理の代わりとして\0というwordとその定義\0.を置きます。
集合をクラスとみなす仕組みも作られ、集合の関数をクラスの関数から誘導することもあります。\(\dagger\)
word(p,p) … \(\neg\)
word(pp,p) … \(,\) \({\bf ,}\) \(\mathbin{\rm o\!r}\) \(\Rightarrow\) \(\Longrightarrow\) \(\Leftrightarrow\) \(\Longleftrightarrow\)
word(ss,p) … \(=\)
word(cc,p) … \(=\)
\(\mathbin{{\sf p}}\) がword(\({\tt xx}\),\({\tt x}\))のとき \( \mathbin{{\sf p}} \mathbin{{\sf p}} \cdots \mathbin{{\sf p}} \) は \(( \cdots ( \mathbin{{\sf p}} ) \mathbin{{\sf p}} \cdots ) \mathbin{{\sf p}} \) に展開されます。
\(\mathbin{{\sf p}}\) に対する結合則があるときのみ使用されるべきです。
いくつかの \(\mathbin{{\sf p}}\) に対してはこれとは別の展開にするためのabbrが与えられます。
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_{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}\)
abbr … \(X \mathbin{{\sf p}} Y \mathbin{{\sf q}} Z\) ≈ \(X \mathbin{{\sf p}} Y , Y \mathbin{{\sf q}} Z\)
word(p\(^{\tt n}\),p)F … \(\mathsf{equiv}_{\tt n}\)
abbr … \(P_{1} \Longleftrightarrow P_{2} \Longleftrightarrow \cdots \Longleftrightarrow P_{\tt n}\) ≈ \(\mathsf{equiv}_{\tt n} ( P_{1} , P_{2} , \cdots , P_{\tt n} )\)
equiv\({\tt n}\). … \(( P_{1} \Longleftrightarrow P_{2} \Longleftrightarrow \cdots \Longleftrightarrow P_{\tt n} ) \Longleftrightarrow ( P_{1} \Longrightarrow P_{2} \Longrightarrow \cdots \Longrightarrow P_{\tt n} \Longrightarrow P_{1} )\)
lower … \(A \stackrel{{\tt /}}{\mathbin{{\sf p}}} B\) ≃ \(\neg ( A \mathbin{{\sf p}} B )\)
word(\({\tt x}\)\({\tt y}\),\({\tt z}\)→\({\tt y}\)\({\tt x}\),\({\tt z}\)) … \(\leftrightarrow\)
lower … \(A \stackrel{\leftrightarrow}{\mathbin{{\sf p}}} B\) ≃ \(B \mathbin{{\sf p}} A\)
word(\({\tt x}\)\({\tt x}\),\({\tt y}\)→\({\tt x}\),\({\tt y}\)) … \(\prime\prime\)
lower … \(\stackrel{\prime\prime}{\mathbin{{\sf p}}} A\) ≃ \(A \mathbin{{\sf p}} A\)
1以上の自然数 \({\tt n}\) に対し
abbr … \(\forall x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( P )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( P )\)
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 ) )\)
2以上の自然数 \({\tt n}\) に対し
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\exists x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)
lower … \({\mathbin{{\sf p}}} :\mathsf{I}\) ≃ \(\forall x ( x \mathbin{{\sf p}} x )\)
lower … \({\mathbin{{\sf p}}} :\mathsf{T}\) ≃ \(\forall x , y , z ( x \mathbin{{\sf p}} y \mathbin{{\sf p}} z \Longrightarrow x \mathbin{{\sf p}} z )\)
lower … \({\mathbin{{\sf p}}} :\mathsf{X}\) ≃ \(\forall x , y ( x \mathbin{{\sf p}} y \Longrightarrow y \mathbin{{\sf p}} x )\)
次のようなlowerは自動で追加されます。
lower … \({\mathbin{{\sf p}}} :\mathsf{I}\&\mathsf{T}\) ≃ \({\mathbin{{\sf p}}} :\mathsf{I} , {\mathbin{{\sf p}}} :\mathsf{T}\)
\({=} :\mathsf{I}\&\mathsf{T}\&\mathsf{X}\) \(\blacktriangleleft\) O
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)
abbr … \(\{ x \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , ( P ) \}\)
以下の3つの左辺では \(\mathop{{\sf X}}\) が表記上無視されます。
abbr … \(\{ T \mid P \}\) ≈ \(\{ x \mid \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
abbr … \(\{ T \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
abbr … \(_{ P } T\) ≈ \(\{ T \mid P \}\)
word(ss,p) … \(\in\)
word(sc,p) … \(\in\)
cvt … \(X \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(X\) を代入したもの
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 ) )\)
lower … \(\stackrel{\text{^}}{\mathbin{{\sf f}}} A\) ≃ \(\{ \mathbin{{\sf f}} a \mid a \in A \}\)
\(\dot\exists \stackrel{\text{^}}{\mathop{{\sf f}}} A\) というのが置換公理です(？)
word(ss,s→ss,c) … \(\text{^*}\) \(\text{*^}\) \(\text{^^}\)
lower … \(A \stackrel{\text{^*}}{\mathbin{{\sf f}}} b\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A \}\)
lower … \(a \stackrel{\text{*^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid b \in B \}\)
lower … \(A \stackrel{\text{^^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A , b \in B \}\)
abbr … \(\{ x \mapsto X \}\) ≈ \(\mathsf{fn} x ( X )\)
cvt … \(\{ x \mapsto X \} ( T )\) ≃ \(T\) の \(x\) に \(X\) を代入したもの
\(\mapsto\) の前のv-Formを \(\bullet\) に替えられます。その際 \(\bullet \mapsto\) は略されます。
例 \(\{ \bullet + a \}\) ≈ \(\{ x \mapsto x + a \}\)
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例 \(\{ \bullet + \{ \bullet + a \} ( x ) \}\) ≃ \(\{ \bullet + ( x + a ) \}\)
lower … \({\mathbin{{\sf f}}} \stackrel{\star}{\mathbin{{\sf a}}} {\mathbin{{\sf g}}}\) ≃ \(\forall x ( ( \mathbin{{\sf f}} x ) \mathbin{{\sf a}} ( \mathbin{{\sf g}} x ) )\)
word(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[ff,\({\tt x}\)][ff,\({\tt x}\)],\({\tt y}\)) … \(\star\!\star\)
lower … \({\mathbin{{\sf f}}} \stackrel{\star\!\star}{\mathbin{{\sf a}}} {\mathbin{{\sf g}}}\) ≃ \(\forall x \forall y ( ( x \mathbin{{\sf f}} y ) \mathbin{{\sf a}} ( x \mathbin{{\sf g}} y ) )\)
Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます。
=s ≅ =
=s. … \({=} \stackrel{\star\!\star}{\Leftrightarrow} {=}\)
sub_. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
subn_. … \(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\)
word(ss,p) … \(\subset\) \(\subsetneq\)
sub. … \({\subset} \stackrel{\star\!\star}{\Leftrightarrow} {\subset}\)
subn. … \({\subsetneq} \stackrel{\star\!\star}{\Leftrightarrow} {\subsetneq}\)
subn.. … \(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\) \(\blacktriangleleft\) W.
\({\subset} :\mathsf{I}\&\mathsf{T}\) \(\blacktriangleleft\) W.
=s.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) W.
\(X \subsetneq Y \subset Z \mathbin{\rm o\!r} X \subset Y \subsetneq Z \Longrightarrow X \subsetneq Z\) \(\blacktriangleleft\) W.
\V. … \(\mathbb{V} = \{ x \mid \top \}\)
\(x \in \mathbb{V}\) \(\blacktriangleleft\) O
\(X \subset \mathbb{V}\) \(\blacktriangleleft\) O
word(,s) … \(\emptyset\)
\0. … \(\emptyset = \{ x \mid {\perp} \}\)
\(x \notin \emptyset\) \(\blacktriangleleft\) W.
\(\emptyset \subset X\) \(\blacktriangleleft\) W.
\0.. … \(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\) \(\blacktriangleleft\) W.
word(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} \}\)
sets ≅ set
sets\({\tt n}\). … \(x \in \{ X_{1} , \cdots , X_{\tt n} \} \Longleftrightarrow x = X_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} x = X_{\tt n}\)
cup_. … \(A \cup B = \{ x \mid x \in A \mathbin{\rm o\!r} x \in B \}\)
cap_. … \(A \cap B = \{ x \mid x \in A , x \in B \}\)
dif_. … \(A \setminus B = \{ x \mid x \in A , x \notin B \}\)
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. … \({\cap} \stackrel{\star\!\star}{=} {\cap}\)
dif. … \({\mathop\setminus} \stackrel{\star\!\star}{=} {\setminus}\)
\(X \mathop\setminus Y = X \cap ( \mathop\setminus Y )\) \(\blacktriangleleft\) W.
\(X \subset Y \Longleftrightarrow X \cup Y = Y \Longleftrightarrow X \cap Y = X\) \(\blacktriangleleft\) W.
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\) W.
word(s,s)R … \(\bigcup\) \(\bigcap\)
Cup. … \({\bigcup} \stackrel{\star}{=} {\bigcup}\)
Cap. … \(\exists X \, X \in \mathcal{X} \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)
Cap.' … \(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\) \(\blacktriangleleft\) W.
\(X = \bigcup \{ X \}\) \(\blacktriangleleft\) W.
\(X = \bigcap \{ X \}\) \(\blacktriangleleft\) W.
\(X \cup Y = \bigcup \{ X , Y \}\) \(\blacktriangleleft\) W.
\(X \cap Y = \bigcap \{ X , Y \}\) \(\blacktriangleleft\) W.
\(X = \bigcup _{ x \in X } \{ x \}\) \(\blacktriangleleft\) W.
lower … \(( X , {\mathbin{{\sf f}}} ) :\underline{1}\) ≃ \(\forall x \in X . \mathbin{{\sf f}} x \in X\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{j}\) ≃ \(\forall x \in X . \mathbin{{\sf f}} ( \mathbin{{\sf f}} x ) = x\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\underline{2}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y \in X\)
$X {^^}$..f $X sub_ $X としたいが…？
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{C}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y = y \mathbin{{\sf f}} x\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{A}\) ≃ \(\forall x , y , z \in X . x \mathbin{{\sf f}} \, ( y \mathbin{{\sf f}} z ) = ( x \mathbin{{\sf f}} y ) \mathbin{{\sf f}} z\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{J}\) ≃ \(\forall x \in X . x \mathbin{{\sf f}} x = x\)
word(s[ss,s],c) … \(\text{unit}\)
lower … \(\text{unit} ( X , {\mathbin{{\sf f}}} )\) ≃ \(\{ e \mid \forall x ( x \in X \Rightarrow ( e \mathbin{{\sf f}} x = x , x = x \mathbin{{\sf f}} e ) ) \}\)
wp. … \(\wp X = \{ A \mid A \subset X \}\)
wp0 … \(\wp \emptyset = \{ \emptyset \}\) \(\blacktriangleleft\) W.
wp1 … \(\wp \{ x \} = \{ \emptyset , \{ x \} \}\) \(\blacktriangleleft\) W.
代数の最初の例にべき集合があります。証明においては = → =s が必要になります。
\(( \wp X , {\cup} ) :\underline{2}\&\mathsf{C}\&\mathsf{A}\&\mathsf{J}\) \(\blacktriangleleft\)
\(( \wp X , {\cap} ) :\underline{2}\&\mathsf{C}\&\mathsf{A}\&\mathsf{J}\) \(\blacktriangleleft\)
\(\emptyset \in \text{unit} ( \wp X , {\cup} )\) \(\blacktriangleleft\)
\(X \in \text{unit} ( \wp X , {\cap} )\) \(\blacktriangleleft\)
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\) O
ax0 … \(\forall X \neq \emptyset . \exists Y \in X . X \cap Y = \emptyset\)
\(\mathbb{V}_0 = \mathbb{V}\) \(\blacktriangleleft\) W. ，ax0
集合・クラスについては「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) … \(=\)
word(cc,p) … \(=\)
\(\mathbin{{\sf p}}\) がword(\({\tt xx}\),\({\tt x}\))のとき \( \mathbin{{\sf p}} \mathbin{{\sf p}} \cdots \mathbin{{\sf p}} \) は \(( \cdots ( \mathbin{{\sf p}} ) \mathbin{{\sf p}} \cdots ) \mathbin{{\sf p}} \) に展開されます。
\(\mathbin{{\sf p}}\) に対する結合則があるときのみ使用されるべきです。
いくつかの \(\mathbin{{\sf p}}\) に対してはこれとは別の展開にするためのabbrが与えられます。
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_{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}\)
abbr … \(X \mathbin{{\sf p}} Y \mathbin{{\sf q}} Z\) ≈ \(X \mathbin{{\sf p}} Y , Y \mathbin{{\sf q}} Z\)
word(p\(^{\tt n}\),p)F … \(\mathsf{equiv}_{\tt n}\)
abbr … \(P_{1} \Longleftrightarrow P_{2} \Longleftrightarrow \cdots \Longleftrightarrow P_{\tt n}\) ≈ \(\mathsf{equiv}_{\tt n} ( P_{1} , P_{2} , \cdots , P_{\tt n} )\)
equiv\({\tt n}\). … \(( P_{1} \Longleftrightarrow P_{2} \Longleftrightarrow \cdots \Longleftrightarrow P_{\tt n} ) \Longleftrightarrow ( P_{1} \Longrightarrow P_{2} \Longrightarrow \cdots \Longrightarrow P_{\tt n} \Longrightarrow P_{1} )\)
2項記号の処理
word(\({\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 )\)
word(\({\tt x}\)\({\tt y}\),\({\tt z}\)→\({\tt y}\)\({\tt x}\),\({\tt z}\)) … \(\leftrightarrow\)
lower … \(A \stackrel{\leftrightarrow}{\mathbin{{\sf p}}} B\) ≃ \(B \mathbin{{\sf p}} A\)
word(\({\tt x}\)\({\tt x}\),\({\tt y}\)→\({\tt x}\),\({\tt y}\)) … \(\prime\prime\)
lower … \(\stackrel{\prime\prime}{\mathbin{{\sf p}}} A\) ≃ \(A \mathbin{{\sf p}} A\)
量化子
word(vp,p)R … \(\forall\) \(\exists\)1以上の自然数 \({\tt n}\) に対し
abbr … \(\forall x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( P )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( P )\)
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 ) )\)
2以上の自然数 \({\tt n}\) に対し
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\exists x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)
2項述語の1項述語
word([ss,p],p)R … \(:\mathsf{I}\) \(:\mathsf{T}\) \(:\mathsf{X}\)lower … \({\mathbin{{\sf p}}} :\mathsf{I}\) ≃ \(\forall x ( x \mathbin{{\sf p}} x )\)
lower … \({\mathbin{{\sf p}}} :\mathsf{T}\) ≃ \(\forall x , y , z ( x \mathbin{{\sf p}} y \mathbin{{\sf p}} z \Longrightarrow x \mathbin{{\sf p}} z )\)
lower … \({\mathbin{{\sf p}}} :\mathsf{X}\) ≃ \(\forall x , y ( x \mathbin{{\sf p}} y \Longrightarrow y \mathbin{{\sf p}} x )\)
次のようなlowerは自動で追加されます。
lower … \({\mathbin{{\sf p}}} :\mathsf{I}\&\mathsf{T}\) ≃ \({\mathbin{{\sf p}}} :\mathsf{I} , {\mathbin{{\sf p}}} :\mathsf{T}\)
\({=} :\mathsf{I}\&\mathsf{T}\&\mathsf{X}\) \(\blacktriangleleft\) O
a2
クラス
word(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 ) \}\)
以下の3つの左辺では \(\mathop{{\sf X}}\) が表記上無視されます。
abbr … \(\{ T \mid P \}\) ≈ \(\{ x \mid \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
abbr … \(\{ T \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
abbr … \(_{ P } T\) ≈ \(\{ T \mid P \}\)
word(ss,p) … \(\in\)
word(sc,p) … \(\in\)
cvt … \(X \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(X\) を代入したもの
一意の量化子
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(s,s→s,c) … \(\text{^}\)lower … \(\stackrel{\text{^}}{\mathbin{{\sf f}}} A\) ≃ \(\{ \mathbin{{\sf f}} a \mid a \in A \}\)
\(\dot\exists \stackrel{\text{^}}{\mathop{{\sf f}}} A\) というのが置換公理です(？)
word(ss,s→ss,c) … \(\text{^*}\) \(\text{*^}\) \(\text{^^}\)
lower … \(A \stackrel{\text{^*}}{\mathbin{{\sf f}}} b\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A \}\)
lower … \(a \stackrel{\text{*^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid b \in B \}\)
lower … \(A \stackrel{\text{^^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A , b \in B \}\)
アロー関数
word(vs,(s,s)) … \(\mathsf{fn}\)abbr … \(\{ x \mapsto X \}\) ≈ \(\mathsf{fn} x ( X )\)
cvt … \(\{ x \mapsto X \} ( T )\) ≃ \(T\) の \(x\) に \(X\) を代入したもの
\(\mapsto\) の前のv-Formを \(\bullet\) に替えられます。その際 \(\bullet \mapsto\) は略されます。
例 \(\{ \bullet + a \}\) ≈ \(\{ x \mapsto x + a \}\)
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例 \(\{ \bullet + \{ \bullet + a \} ( x ) \}\) ≃ \(\{ \bullet + ( x + a ) \}\)
a3
2項記号の関数化
word(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[f,\({\tt x}\)][f,\({\tt x}\)],\({\tt y}\)) … \(\star\)lower … \({\mathbin{{\sf f}}} \stackrel{\star}{\mathbin{{\sf a}}} {\mathbin{{\sf g}}}\) ≃ \(\forall x ( ( \mathbin{{\sf f}} x ) \mathbin{{\sf a}} ( \mathbin{{\sf g}} x ) )\)
word(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[ff,\({\tt x}\)][ff,\({\tt x}\)],\({\tt y}\)) … \(\star\!\star\)
lower … \({\mathbin{{\sf f}}} \stackrel{\star\!\star}{\mathbin{{\sf a}}} {\mathbin{{\sf g}}}\) ≃ \(\forall x \forall y ( ( x \mathbin{{\sf f}} y ) \mathbin{{\sf a}} ( x \mathbin{{\sf g}} 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}\}\) に置き換えられます。
=s ≅ =
=s. … \({=} \stackrel{\star\!\star}{\Leftrightarrow} {=}\)
包含関係
word(cc,p) … \(\subset\) \(\subsetneq\)sub_. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
subn_. … \(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\)
word(ss,p) … \(\subset\) \(\subsetneq\)
sub. … \({\subset} \stackrel{\star\!\star}{\Leftrightarrow} {\subset}\)
subn. … \({\subsetneq} \stackrel{\star\!\star}{\Leftrightarrow} {\subsetneq}\)
subn.. … \(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\) \(\blacktriangleleft\) W.
\({\subset} :\mathsf{I}\&\mathsf{T}\) \(\blacktriangleleft\) W.
=s.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) W.
\(X \subsetneq Y \subset Z \mathbin{\rm o\!r} X \subset Y \subsetneq Z \Longrightarrow X \subsetneq Z\) \(\blacktriangleleft\) W.
宇宙、空集合
word(,c) … \(\mathbb{V}\)\V. … \(\mathbb{V} = \{ x \mid \top \}\)
\(x \in \mathbb{V}\) \(\blacktriangleleft\) O
\(X \subset \mathbb{V}\) \(\blacktriangleleft\) O
word(,s) … \(\emptyset\)
\0. … \(\emptyset = \{ x \mid {\perp} \}\)
\(x \notin \emptyset\) \(\blacktriangleleft\) W.
\(\emptyset \subset X\) \(\blacktriangleleft\) W.
\0.. … \(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\) \(\blacktriangleleft\) W.
有限集合
1以上の自然数 \({\tt n}\) に対してword(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} \}\)
sets ≅ set
sets\({\tt n}\). … \(x \in \{ X_{1} , \cdots , X_{\tt n} \} \Longleftrightarrow x = X_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} x = X_{\tt n}\)
合併、共通部分、差
word(cc,c) … \(\cup\) \(\cap\) \(\setminus\)cup_. … \(A \cup B = \{ x \mid x \in A \mathbin{\rm o\!r} x \in B \}\)
cap_. … \(A \cap B = \{ x \mid x \in A , x \in B \}\)
dif_. … \(A \setminus B = \{ x \mid x \in A , x \notin B \}\)
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. … \({\cap} \stackrel{\star\!\star}{=} {\cap}\)
dif. … \({\mathop\setminus} \stackrel{\star\!\star}{=} {\setminus}\)
\(X \mathop\setminus Y = X \cap ( \mathop\setminus Y )\) \(\blacktriangleleft\) W.
\(X \subset Y \Longleftrightarrow X \cup Y = Y \Longleftrightarrow X \cap Y = X\) \(\blacktriangleleft\) W.
総合併、総共通部分
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\) W.
word(s,s)R … \(\bigcup\) \(\bigcap\)
Cup. … \({\bigcup} \stackrel{\star}{=} {\bigcup}\)
Cap. … \(\exists X \, X \in \mathcal{X} \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)
Cap.' … \(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\) \(\blacktriangleleft\) W.
\(X = \bigcup \{ X \}\) \(\blacktriangleleft\) W.
\(X = \bigcap \{ X \}\) \(\blacktriangleleft\) W.
\(X \cup Y = \bigcup \{ X , Y \}\) \(\blacktriangleleft\) W.
\(X \cap Y = \bigcap \{ X , Y \}\) \(\blacktriangleleft\) W.
\(X = \bigcup _{ x \in X } \{ x \}\) \(\blacktriangleleft\) W.
a4
1項関数の1項述語
word(s[s,s],p)R … \(:\underline{1}\) \(:\mathsf{j}\)lower … \(( X , {\mathbin{{\sf f}}} ) :\underline{1}\) ≃ \(\forall x \in X . \mathbin{{\sf f}} x \in X\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{j}\) ≃ \(\forall x \in X . \mathbin{{\sf f}} ( \mathbin{{\sf f}} x ) = x\)
2項関数の1項述語
word(s[ss,s],p)R … \(:\underline{2}\) \(:\mathsf{C}\) \(:\mathsf{A}\) \(:\mathsf{J}\)lower … \(( X , {\mathbin{{\sf f}}} ) :\underline{2}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y \in X\)
$X {^^}$..f $X sub_ $X としたいが…？
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{C}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y = y \mathbin{{\sf f}} x\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{A}\) ≃ \(\forall x , y , z \in X . x \mathbin{{\sf f}} \, ( y \mathbin{{\sf f}} z ) = ( x \mathbin{{\sf f}} y ) \mathbin{{\sf f}} z\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{J}\) ≃ \(\forall x \in X . x \mathbin{{\sf f}} x = x\)
word(s[ss,s],c) … \(\text{unit}\)
lower … \(\text{unit} ( X , {\mathbin{{\sf f}}} )\) ≃ \(\{ e \mid \forall x ( x \in X \Rightarrow ( e \mathbin{{\sf f}} x = x , x = x \mathbin{{\sf f}} e ) ) \}\)
べき集合
word(s,s) … \(\wp\)wp. … \(\wp X = \{ A \mid A \subset X \}\)
wp0 … \(\wp \emptyset = \{ \emptyset \}\) \(\blacktriangleleft\) W.
wp1 … \(\wp \{ x \} = \{ \emptyset , \{ x \} \}\) \(\blacktriangleleft\) W.
代数の最初の例にべき集合があります。証明においては = → =s が必要になります。
\(( \wp X , {\cup} ) :\underline{2}\&\mathsf{C}\&\mathsf{A}\&\mathsf{J}\) \(\blacktriangleleft\)
\(( \wp X , {\cap} ) :\underline{2}\&\mathsf{C}\&\mathsf{A}\&\mathsf{J}\) \(\blacktriangleleft\)
\(\emptyset \in \text{unit} ( \wp X , {\cup} )\) \(\blacktriangleleft\)
\(X \in \text{unit} ( \wp X , {\cap} )\) \(\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\) O
ax0 … \(\forall X \neq \emptyset . \exists Y \in X . X \cap Y = \emptyset\)
\(\mathbb{V}_0 = \mathbb{V}\) \(\blacktriangleleft\) W. ，ax0