1
一般の一階言語で使用されうる記号を作ります。特別な二項述語として \(=\) も作られます。量化子、省略記号には多様なものが用意されます。
論理
word(,p) … \(\top\) \({\perp}\)word(p,p) … \(\neg\)
word(pp,p) … \(,\) \({\bf ,}\) \(\mathbin{\rm o\!r}\) \(\Rightarrow\) \(\Longrightarrow\) \(\Leftrightarrow\) \(\Longleftrightarrow\)
word(vp,p)R … \(\forall\) \(\exists\)
precedの差により\((\;)\)が略せることがあります。例 【\(\forall x \neg P\)】≈【\(\forall x ( \neg P )\)】
abbr …【\(\begin{cases} {\sf P} \\ {\sf Q} \end{cases}\)】≈【\(( {\sf P} ) , ( {\sf Q} )\)】
論理の略記
abbr …【\( {\sf X}\)】≈【\({\sf X} , {\sf X}\)】abbr …【\( {\sf X}\)】≈【\({\sf X} {\bf ,} \, {\sf X}\)】
例 【\(P \Longleftrightarrow Q \Longleftrightarrow R\)】≈【\(P \Longleftrightarrow Q {\bf ,} \, Q \Longleftrightarrow R\)】
abbr … 【\( {\sf T}_{1} , \cdots , {\sf T}_{\tt n} {\sf A}\)】≈【\({\sf T}_{1} {\sf A} , \cdots , {\sf T}_{\tt n} {\sf A}\)】
例 【\( x , y \in X\)】≈【\(x \in X , y \in X\)】
abbr … 【\(\forall {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf P}\)】≈【\(\forall {\sf x}_{1} \cdots \forall {\sf x}_{\tt n} ( {\sf P} )\)】
abbr … 【\(\exists {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf P}\)】≈【\(\exists {\sf x}_{1} \cdots \exists {\sf x}_{\tt n} ( {\sf P} )\)】
abbr … 【\(\forall {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf A} . {\sf P}\)】≈【\(\forall {\sf x}_{1} \cdots \forall {\sf x}_{\tt n} ( {\sf x}_{1} {\sf A} , \cdots , {\sf x}_{\tt n} {\sf A} \Longrightarrow ( {\sf P} ) )\)】
abbr … 【\(\exists {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf A} . {\sf P}\)】≈【\(\exists {\sf x}_{1} \cdots \exists {\sf x}_{\tt n} ( {\sf x}_{1} {\sf A} , \cdots , {\sf x}_{\tt n} {\sf A} , ( {\sf P} ) )\)】
token all,exiを変更すべし。supのやり方も。
2項記号の処理
word関数 … 斜線をつける #/ : (\({\tt x}\)\({\tt y}\),p)→(\({\tt x}\)\({\tt y}\),p)def … #/$..p $A $B ≃ not ($..p $A $B)
word関数 … 左右反転させる #- : (\({\tt x}\)\({\tt y}\),\({\tt z}\))→(\({\tt y}\)\({\tt x}\),\({\tt z}\))
def …【\({\sf A} \class{reflect}{\mathop{{\sf p}}} {\sf B}\)】≃【\({\sf B} \mathop{{\sf p}} {\sf A}\)】
表記は【\(X \class{reflect}{\notin} x\)】より【\(X \not\ni x\)】の方が良いでしょう。
word関数 … \(\widehat{\;\;}\) を付ける #2 : (\({\tt x}\)\({\tt x}\),\({\tt y}\))→(\({\tt x}\),\({\tt y}\))
def …【\(\widehat{\mathop{{\sf p}}} \, {\sf A}\)】≃【\({\sf A} \mathop{{\sf p}} {\sf A}\)】
等号を含む論理
word(ss,p) … \(=\)abbr … 【\(\overline\forall {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf P}\)】≈【\( \forall {\sf x}_{1} \cdots {\sf x}_{\tt n} \, ( {\sf x}_{1} \neq {\sf x}_{2} , \cdots \Longrightarrow {\sf P} )\)】
abbr … 【\(\overline\exists {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf P}\)】≈【\(\exists {\sf x}_{1} \cdots \exists {\sf x}_{\tt n} \, ( {\sf x}_{1} \neq {\sf x}_{2} , \cdots , {\sf P} )\)】
abbr … 【\(\overline\forall {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf A} . {\sf P}\)】≈【\(\forall {\sf x}_{1} {\sf A} \cdots \forall {\sf x}_{\tt n} {\sf A} \, ( {\sf x}_{1} \neq {\sf x}_{2} , \cdots \Longrightarrow {\sf P} )\)】
abbr … 【\(\overline\exists {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf A} . {\sf P}\)】≈【\(\exists {\sf x}_{1} {\sf A} \cdots \exists {\sf x}_{\tt n} {\sf A} \, ( {\sf x}_{1} \neq {\sf x}_{2} , \cdots , {\sf P} )\)】
n=2のときだけ多分完成
一意性量化子
word(vx,p)R … \(!\) \(\exists!\)
def …【\(! {\sf x} {\sf P}\)】≃【\(\forall {\sf y} , {\sf z} \in \{ {\sf x} \mid {\sf P} \} . {\sf y} = {\sf z}\)】
def …【\(\exists! {\sf x} {\sf P}\)】≃【\(\exists {\sf x} \, {\sf P} , ! {\sf x} {\sf P}\)】
abbr …【\(! {\sf x} {\sf A} . {\sf P}\)】≈【\(! {\sf x} \, ( {\sf x} {\sf A} , ( {\sf P} ) )\)】
abbr …【\(\exists! {\sf x} {\sf A} . {\sf P}\)】≈【\(\exists! {\sf x} \, ( {\sf x} {\sf A} , ( {\sf P} ) )\)】
2項述語に対する1項述語
次の3条件を満たす \({\tt p}\) は同値関係と呼ばれます。abbr …【\(\mathop{{\sf p}} {:}\, \mathfrak{I}\)】≈【\(\forall {\sf x} \, ( {\sf x} \mathop{{\sf p}} {\sf x} )\)】
abbr …【\(\mathop{{\sf p}} {:}\, \mathfrak{T}\)】≈【\(\forall {\sf x} , {\sf y} , {\sf z} ( {\sf x} \mathop{{\sf p}} {\sf y} \mathop{{\sf p}} {\sf z} \Longrightarrow {\sf x} \mathop{{\sf p}} {\sf z} )\)】
abbr …【\(\mathop{{\sf p}} {:}\, \mathfrak{X}\)】≈【\(\forall {\sf x} , {\sf y} ( {\sf x} \mathop{{\sf p}} {\sf y} \Longrightarrow {\sf y} \mathop{{\sf p}} {\sf x} )\)】
次のようなabbrは自動で準備されます。
abbr …【\(\mathop{{\sf p}} {:}\, \mathfrak{I} \mathfrak{T}\)】≈【\(\mathop{{\sf p}} {:}\, \mathfrak{I} , \mathop{{\sf p}} {:}\, \mathfrak{T}\)】
【\(= {:}\, \mathfrak{I} \mathfrak{T} \mathfrak{X}\)】\(\,{\blacktriangleleft}\,\text{O}\)
2
集合・クラスの最も基本的な記号を作ります。\(\{\;|\;\}\) と２項述語 \(\in,\subset\) などです。
クラスの生成（内包記法）
word(vp,c)! … cls abbr … 【\(\{ {\sf X} \mid {\sf P} \}\)】≈ cls ($X , $P)abbr …【\(\{ {\sf x} {\sf A} \mid {\sf P} \}\)】≈【\(\{ {\sf x} \mid {\sf x} {\sf A} , {\sf P} \}\)】
\(\sum_{i\in\{1,2\}}i=3\) の左辺を \(\sum\{i \mid i\in\{1,2\}\}\) と解釈するために次の準備をします。
abbr …【\(_{ {\sf P} } {\sf x}\)】≈【\(\{ {\sf x} \mid {\sf P} \}\)】
拡張された内包記法は$Xが表記では消えるので注意しましょう。
abbr …【\(\{ {\sf T} \mid {\sf P} \}\)】≈【\(\{ {\sf x} \mid \exists {\sf X} ( ( {\sf P} ) , {\sf x} = {\sf T} ) \}\)】
abbr …【\(\{ {\sf T} {\sf A} \mid {\sf P} \}\)】≈【\(\{ {\sf x} {\sf A} \mid \exists {\sf X} ( ( {\sf P} ) , {\sf x} = {\sf T} ) \}\)】
\(\sum_{i\in\{0,1\}}(i+1)=3\) という記述もできるようにします。
abbr …【\(_{ {\sf P} } {\sf T}\)】≈【\(\{ {\sf T} \mid {\sf P} \}\)】
「属する」という関係
word(sc,p) … \(\in\)def … 【\({\sf T} \in \{ {\sf x} \mid {\sf P} \}\)】≃\(【{\sf P}】\!^{{\sf x}\,\mapsto\,{\sf T}}\)
word(ss,p) … \(\in\)
集合はクラスとみなされます。
word(s,c)! … sc
def …【\( {\sf X}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf X} \}\)】
scは省略可能です。例 【\(x \in X\)】≃【\(x \in X\)】
超decentの必要なし？
等号
word(cc,p) … \(=\)def …【\({\sf X} = {\sf Y}\)】≃【\(\forall {\sf x} \, ( {\sf x} \in {\sf X} \Leftrightarrow {\sf x} \in {\sf Y} )\)】
定義の誘導を行うときに次の略記が使用されます。
abbr …【\(\mathop{{\sf p}} {\tt <=>} \mathop{{\sf q}}\)】≈【\(X \mathop{{\sf p}} Y \Longleftrightarrow X \mathop{{\sf q}} Y\)】
abbr …【\(\mathop{{\sf f}} {\tt ==} \mathop{{\sf g}}\)】≈【\(\mathop{{\sf f}} X = \mathop{{\sf g}} X\)】
abbr …【\(\mathop{{\sf f}} {\tt ==} \mathop{{\sf g}}\)】≈【\(X \mathop{{\sf f}} Y = X \mathop{{\sf g}} Y\)】
集合の等号として =s ≅ = を用意し、外延性公理を与えます。
\({=.}\)【\(= {\tt <=>} =\)】
包含関係
word(cc,p) … \(\subset\) \(\subsetneq\)def …【\({\sf X} \subset {\sf Y}\)】≃【\(\forall {\sf x} \in {\sf X} . {\sf x} \in {\sf Y}\)】
def …【\({\sf X} \subsetneq {\sf Y}\)】≃【\({\sf X} \subset {\sf Y} , {\sf X} \neq {\sf Y}\)】
word(ss,p) … \(\subset\) \(\subsetneq\)
\({\subset.}\)【\(\subset {\tt <=>} \subset\)】
\({\subsetneq}.\)【\(\subsetneq {\tt <=>} \subsetneq\)】
【\(\subset {:}\, \mathfrak{I} \mathfrak{T}\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
\({=}{.}{.}\)【\(X = Y \Longleftrightarrow X \subset Y \subset X\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
【\(( X \subsetneq Y \subset Z ) \mathbin{\rm o\!r} ( X \subset Y \subsetneq Z ) \Longrightarrow X \subsetneq Z\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
3
具体的な集合・クラスの作成に取りかかります。基本的な関数を作ります。
宇宙、空集合
word(,c) … \(\text{Set}\)def …【\(\text{Set}\)】≃【\(\{ x \mid \top \}\)】
【\(x \in \text{Set}\)】\(\,{\blacktriangleleft}\,\text{O}\)
【\(X \subset \text{Set}\)】\(\,{\blacktriangleleft}\,\text{O}\)
word(,s) … \(\emptyset\)
\({\emptyset.}\)【\(\emptyset = \{ x \mid {\perp} \}\)】
【\(x \notin \emptyset\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
【\(\emptyset \subset X\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
\(\emptyset{.}{.}\)【\(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
有限集合の生成(外延記法)
word(s\(^{\tt n}\),s)! … set abbr … 【\(\{ {\sf X}_{1} , \cdots , {\sf X}_{\tt n} \}\)】≈ set ($X1 , … , $Xn)例えば【\(\{ x , \{ x , y \} \}\)】はs-Formで、現れる2つのsetはword(ss,s)です。
\(\text{set}_{\tt n}.\)【\(\{ X_{1} , \cdots , X_{\tt n} \} = \{ x \mid x = X_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} x = X_{\tt n} \}\)】
集合の有限集合を作るときには sets ≅ set を使用します。
\(\text{sets}_{\tt n}.\)【\(\{ X_{1} , \cdots , X_{\tt n} \} = \{ x \mid x = X_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} x = X_{\tt n} \}\)】
合併、共通部分、差
word(cc,c) … \(\cup\) \(\cap\)def …【\({\sf X} \cup {\sf Y}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf X} \mathbin{\rm o\!r} {\sf x} \in {\sf Y} \}\)】
def …【\({\sf X} \cap {\sf Y}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf X} , {\sf x} \in {\sf Y} \}\)】
word(c,c) … \(\mathop\setminus\)
def …【\(\mathop\setminus {\sf Y}\)】≃【\(\{ {\sf x} \mid {\sf x} \notin {\sf Y} \}\)】
word(ss,s) … \(\cup\) \(\cap\) \(\mathop\setminus\)
\(\cup.\)【\(\cup \, {\tt ==} \, \cup\)】
\(\cap.\)【\(\cap \, {\tt ==} \, \cap\)】
\(\setminus.\)【\(X \mathop\setminus Y = X \cap ( \mathop\setminus Y )\)】
【\(X \subset Y \Longleftrightarrow X \cup Y = Y \Longleftrightarrow X \cap Y = X\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
総合併、総共通部分
word(c,c) … \(\bigcup\) \(\bigcap\)def …【\(\bigcup {\sf X}\)】≃【\(\{ {\sf t} \mid \exists {\sf x} \in {\sf X} . {\sf t} \in {\sf x} \}\)】
def …【\(\bigcap {\sf X}\)】≃【\(\{ {\sf t} \mid \forall {\sf x} \in {\sf X} . {\sf t} \in {\sf x} \}\)】
【\(\bigcap \emptyset = \text{Set}\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
word(s,s) … \(\bigcup\) \(\bigcap\)
\(\bigcup.\)【\(\bigcup {\tt ==} \bigcup\)】
\(\bigcap.\)【\(X \neq \emptyset \Longrightarrow \bigcap X = \bigcap X\)】\(\,{\triangleleft}\,\)
【\(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}.\)
集合は１点集合により分割されます。
【\(X = \bigcup _{ x \in X } \{ x \}\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
べき集合
word(s,s) … \(\wp\)\(\wp.\)【\(\wp X = \{ A \mid A \subset X \}\)】
【\(\wp \emptyset = \{ \emptyset \}\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
【\(\wp ( \{ x \} ) = \{ \emptyset , \{ x \} \}\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)