a3
集合の有限集合を作るときには sets ≅ set を使用します。sets\({\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} \}\)】
証明のために次を準備しておきます。
set\({\tt n}\).x【\(v \in \{ x_{1} , \cdots , x_{\tt n} \} \Rightarrow P \Longleftrightarrow ( v = x_{1} \Rightarrow P ) , \cdots , ( v = x_{\tt n} \Rightarrow P )\)】
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}\)】\(\blacktriangleleft\)
b1
cvt …【\(\mathbb{V}_1\)】≃【\(\{ x \mid \not\exists y \, ( x \in y \in x ) \}\)】【\(\mathbb{V}_1 = \mathbb{V}_1\)】\(\blacktriangleleft\)
b2
0.【\(x \in 0 \Longleftrightarrow {\perp}\)】\(\blacktriangleleft\)suc.【\(x \in n \textit{+1} \Longleftrightarrow x \in n \mathbin{\rm o\!r} x = n\)】\(\blacktriangleleft\)
cvt …【\(\text{Ind}\)】≃【\(\{ M \mid 0 \in M , \forall m \in M . m \textit{+1} \in M \}\)】
【\(\text{Ind} = \text{Ind}\)】\(\blacktriangleleft\)
\Mi1【\(\forall n \in \mathbb{M} . n \textit{+1} \in \mathbb{M}\)】\(\blacktriangleleft\)
Cup\M【\(n \in \mathbb{M} \Longrightarrow n \subset \mathbb{M}\)】\(\blacktriangleleft\)
準備 M_a.【\(M_a = \{ n \in \mathbb{M} \mid n \subset \mathbb{M} \}\)】
\(\mathbb{M}\)が推移的であることを示します。機械は細い論理も平気で通します！
<\Ml【\(m \in n \in \mathbb{M} \Longrightarrow m \subsetneq n\)】\(\blacktriangleleft\)
準備 M_b.【\(M_b = \{ n \in \mathbb{M} \mid \forall m \in n . m \subsetneq n \}\)】
<\Mr【\( m , n \in \mathbb{M} , m \subsetneq n \Longrightarrow m \in n\)】\(\blacktriangleleft\)
準備 M_c.【\(M_c = \{ n \in \mathbb{M} \mid \forall m \in \mathbb{M} . ( m \subsetneq n \Rightarrow m \in n ) \}\)】
\({\tt n}\).【\(x \in {\tt n} \Longleftrightarrow x = 0 \mathbin{\rm o\!r} x = 1 \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} x = {\tt n\,{\text -}\,1}\)】\(\blacktriangleleft\)
b3
+\M0【\(m \in \mathbb{M} , n \in \mathbb{M} \Longrightarrow m + n \in \mathbb{M}\)】\(\blacktriangleleft\)準備 M_p.【\(M_p = \{ n \in \mathbb{M} \mid \forall m \in \mathbb{M} . ( m + n \in \mathbb{M} ) \}\)】
*\M0【\(m \in \mathbb{M} , n \in \mathbb{M} \Longrightarrow m \cdot n \in \mathbb{M}\)】\(\blacktriangleleft\)
準備 M_m.【\(M_m = \{ n \in \mathbb{M} \mid \forall m \in \mathbb{M} . ( m \cdot n \in \mathbb{M} ) \}\)】
c2
->..【\(X \to Y = \{ f \in \text{Map} ( X ) \mid \forall x \in X . f ( x ) \in Y \}\)】\(\blacktriangleleft\)c3
->I.【\(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \forall y \, ! x \, \langle x , y \rangle \in f \}\)】\(\blacktriangleleft\)->S.【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists x \, \langle x , y \rangle \in f \}\)】\(\blacktriangleleft\)
->I..【\(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \forall^* x_{0} , x_{1} \in X . f ( x_{0} ) \neq f ( x_{1} ) \}\)】\(\blacktriangleleft\)
->S..【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists x \in X . y = f ( x ) \}\)】\(\blacktriangleleft\)
choice.【\(\text{choice} ( \mathcal{X} ) = \{ f \in \mathcal{X} \to \bigcup \mathcal{X} \mid \forall X , x \, ( \langle X , x \rangle \in f \Rightarrow x \in X ) \}\)】\(\blacktriangleleft\)
d1
=#.【\(X \stackrel{\#}= Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm IS}\to Y\)】\(\blacktriangleleft\)le#.【\(X \stackrel{\#}\le Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm I}\to Y\)】\(\blacktriangleleft\)