1
集合・クラスに関する素朴でない話とか。当システムがZFをカバーするようにします。
集合となるクラス
word(c,p) … \(\dot\exists\)def …【\(\dot\exists {\sf X}\)】≃【\(\exists {\sf x} \, ( {\sf x} = {\sf X} )\)】
Russelのパラドクスが「集合でないクラス(固有クラス)」の最初の例を与えます。
word(,c) … \(\text{Nsc}\)
def …【\(\text{Nsc}\)】≃【\(\{ {\sf x} \mid {\sf x} \notin {\sf x} \}\)】
【\(\neg \dot\exists \text{Nsc}\)】\(\,{\blacktriangleleft}\,\text{O}\)
いくつかの公理
ZFには集合の存在に関する公理があります。当システムでは、例えば空集合公理の代わりに\(\emptyset\)と\({\emptyset.}\)を置きます。
集合とクラスの共通部分は集合になります(分出公理)が、word(sc,s)は使用できません。
無限個の公理が必要なのは頭の痛い所です。
word(c,p)F … \(\text{ax_s}\)
def …【\(\text{ax_s} ( {\sf X} )\)】≃【\(\forall {\sf d} \, \dot\exists ( {\sf d} \cap {\sf X} )\)】
【\(\neg \dot\exists \text{Set}\)】\(\,{\blacktriangleleft}\,\text{Ax_s}\)
正則性公理
\(\text{ax_r}\)【\(\forall X \neq \emptyset . \exists Y \in X . X \cap Y = \emptyset\)】\(\,{\triangleleft}\,\)
\(\text{wfs}0\)【\(X \notin X\)】\(\,{\blacktriangleleft}\,\mathbb{W}.{\bf ,}\,\text{ax_r}\)
\(\text{wfs}1\)【\(\neg ( X \in Y \in X )\)】\(\,{\blacktriangleleft}\,\mathbb{W}.{\bf ,}\,\text{ax_r}\)
関数の像
word関数 … 表記の無い #p : (s,s)→(s,c)def …【\({\mathop{{\sf f}}} \, {\sf A}\)】≃【\(\{ \mathop{{\sf f}} {\sf a} \mid {\sf a} \in {\sf A} \}\)】
【\(\dot\exists \, {\mathop{{\sf f}}} \, {\sf A}\)】というのが置換公理です(？)
word関数 … 表記の無い #l , #r , #P : (ss,s)→(ss,c)
def …【\({\sf A} \, {\mathop{{\sf f}}} \, {\sf b}\)】≃【\(\{ {\sf a} \mathop{{\sf f}} {\sf b} \mid {\sf a} \in {\sf A} \}\)】
def …【\({\sf a} \, {\mathop{{\sf f}}} \, {\sf B}\)】≃【\(\{ {\sf a} \mathop{{\sf f}} {\sf b} \mid {\sf b} \in {\sf B} \}\)】
def …【\({\sf A} \, {\mathop{{\sf f}}} \, {\sf B}\)】≃【\(\{ {\sf a} \mathop{{\sf f}} {\sf b} \mid {\sf a} \in {\sf A} , {\sf b} \in {\sf B} \}\)】
2
自然数の理論の作成ではメタでの自然数が使用されメタ定理も多く作られます。
定理チェックに入れるときに「n に自然数を代入すると」を ; n と書きます。
自然数
0以上の自然数 \({\tt n}\) に対し word(,s) … \({\tt n}\)自然数を集合と思う時にはvon Neumann流の定義を採用します。
\({0.}\)【\(0 = \emptyset\)】\(\,{\triangleleft}\,\)
\({\tt n}.\)【\({\tt n} = \{ 0 , 1 , \cdots , {\tt n\,{\text -}\,1} \}\)】\(\,{\triangleleft}\,\)
0以上の自然数全体を作ってしまいます。
word(,s) … \(\mathbb{M}\)
\(\mathbb{M}0\)【\(0 \in \mathbb{M}\)】
加法および後続関数を準備します。
word(ss,s) … \(+\) \(+\) \(+\) \(+\)
\({+}\text{l}.\)【\(+ \, {\tt ==} \, {+}\)】 \({+}\text{r}.\)【\(+ \, {\tt ==} \, {+}\)】 \({+}\text{_}.\)【\(+ \, {\tt ==} \, {+}\)】
後置される suc ≅ + 1 suc_ ≅ +l 1
\({+1\_}.\)【\(+1 \, {\tt ==} \, {+1}\)】
帰納法
def …【\(\text{Ind}\)】≃【\(\{ M \mid 0 \in M , M +1 \subset M \}\)】帰納法を使うときだけは自然数全体として \Mi ≅ \M を使用します。
\(\mathbb{M}.\)【\(\mathbb{M} = \bigcap \text{Ind}\)】
\(\mathbb{M}1\)【\(\mathbb{M} +1 \subset \mathbb{M}\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
\({+}1.\)【\(n \in \mathbb{M} \Longrightarrow n +1 = n \cup \{ n \}\)】\(\,{\triangleleft}\,\)
次のThmはメタの帰納法で示されます。
\({\tt n}{+}1\)【\({\tt n} +1 = {\tt n+1}\)】\(\,{\blacktriangleleft}\,\mathbb{W}.{\bf ,}\,\mathbb{M}0\)
【\({\tt n} \in \mathbb{M}\)】 \(\,{\blacktriangleleft}\,\mathbb{W}.{\bf ,}\,\mathbb{M}0\)
\({\in}\mathbb{M}\)【\(n \in \mathbb{M} \Longrightarrow n \subset \mathbb{M}\)】\(\,{\blacktriangleleft}\,\mathbb{W}.{\bf ,}\,\mathbb{M}0{\bf ,}\,\text{Ax_s}\)
準備 \(\text{M_i}.\)【\(M_i = \{ n \in \mathbb{M} \mid n \subset \mathbb{M} \}\)】
\(\mathbb{M}\)が推移的であることを示します。機械は細い論理も平気で通します！
\({\in}{\in}\mathbb{M}\)【\(m \in n \in \mathbb{M} \Longrightarrow m \subsetneq n\)】\(\,{\blacktriangleleft}\,\mathbb{W}.{\bf ,}\,\mathbb{M}0{\bf ,}\,\text{Ax_s}\)
準備 \(\text{M_j}.\)【\(M_j = \{ n \in \mathbb{M} \mid \forall m \in n . m \subsetneq n \}\)】
【\(n \in \mathbb{M} \Rightarrow n \notin n\)】\(\,{\blacktriangleleft}\,\mathbb{W}.{\bf ,}\,\mathbb{M}0{\bf ,}\,\text{Ax_s}\)
\(\mathbb{M}\)が連結的であることも示します。【\( m , n \in \mathbb{M} \Rightarrow m \subset n \mathbin{\rm o\!r} n \subset m\)】
補題や新wordの準備をやりやすく
1以上の自然数
word(,s) … \(\mathbb{N}\)\(\mathbb{N}.\)【\(\mathbb{N} = \mathbb{M} \mathop\setminus 1\)】\(\,{\triangleleft}\,\)
\(\mathbb{N}{.}{.}\)【\(\mathbb{N} = \mathbb{M} +1\)】\(\,{\blacktriangleleft}\,\mathbb{W}.{\bf ,}\,\mathbb{M}0{\bf ,}\,\text{Ax_s}\)
準備 \(\text{M_n}.\)【\(M_n = \{ n \in \mathbb{M} \mid n \neq 0 \Rightarrow \exists k \in \mathbb{M} . n = k +1 \}\)】
Le1 / W. ＜ \M0，\Mi1；Le1 := `M_n in_ Ind`，Le2 := `n in \Mi dif 1 => n in \M suc_`
`n in \M => n suc #/=s 0` / W. ＜ O
`n in \Mi dif 1 => n in \M suc_` / W. ＜ Le1，M_n.