a3
集合の等号としては =s ≅ = を使用します。集合の有限集合を作るときには 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} \}\)】
b1
\(\bigcap.\)【\(x \in \bigcap X \Longleftrightarrow \begin{cases} \exists x \, x \in X \Rightarrow \forall y \in X . x \in y \\ \not\exists x \, x \in X \Rightarrow x \in \bigcap X \end{cases}\)】\(\,{\triangleleft}\,\)def …【\(\mathbb{U}_1\)】≃【\(\{ x \mid \not\exists y \, ( x \in y \in x ) \}\)】
【\(\mathbb{U}_1 = \mathbb{U}_1\)】\(\,{\blacktriangleleft}\,\)
b2
\({0.}\)【\(x \in 0 \Longleftrightarrow {\perp}\)】\(\,{\triangleleft}\,\)\({\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}\)】\(\,{\triangleleft}\,\)
def …【\(\text{Ind}\)】≃【\(\{ M \mid 0 \in M , \forall m \in M . m \textit{+1} \in M \}\)】
【\(\text{Ind} = \text{Ind}\)】\(\,{\blacktriangleleft}\,\)
\(\mathbb{M}1\)【\(\forall n \in \mathbb{M} . n \textit{+1} \in \mathbb{M}\)】\(\,{\blacktriangleleft}\,\)
\(\textit{+1}.\)【\(x \in n \textit{+1} \Longleftrightarrow x \in n \mathbin{\rm o\!r} x = n\)】\(\,{\triangleleft}\,\)
\(\bigcup\mathbb{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}\)が推移的であることを示します。機械は細い論理も平気で通します！
\({<_\mathbb{M}}0\text{l}\)【\(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 \}\)】
\({<_\mathbb{M}}0\text{r}\)【\( 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 ) \}\)】
\(\mathbb{N}.\)【\(n \in \mathbb{N} \Longleftrightarrow 0 \neq n \in \mathbb{M}\)】\(\,{\triangleleft}\,\)
b3
\(+_\mathbb{M}0\)【\(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} ) \}\)】
\(*_\mathbb{M}0\)【\(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
\({\stackrel{\rm I}\to}.\)【\(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \forall y \, ! x \, \langle x , y \rangle \in f \}\)】\({\stackrel{\rm S}\to}.\)【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists x \in X . \langle x , y \rangle \in f \}\)】
c3
\(\stackrel{\#}=.\)【\(X \stackrel{\#}= Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm IS}\to Y\)】\(\stackrel{\#}\le.\)【\(X \stackrel{\#}\le Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm I}\to Y\)】