1 自然数

1.1 0と後続関数

word(,s) … \(0\)
0. … \(0 = \emptyset\)

word(s,s) … \(\textit{+1}\)  \(\hat{\textit{+1}}\)
suc. … \(n \textit{+1} = n \cup \{ n \}\)
^suc. … \([\hat{\textit{+1}}] \, \stackrel{\star}{=} [\stackrel{\text{^}}{\textit{+1}}]\)

1.2 帰納法

word(,c) … \(\text{Ind}\)
Ind. … \(\text{Ind} = \{ M \mid 0 \in M , M \hat{\textit{+1}} \subset M \}\)

word(,s) … \(\mathbb{M}\)
𝕄. … \(\mathbb{M} = \bigcap \text{Ind}\)
\(0 \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(\mathbb{M} \in \text{Ind}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
<𝕄:i … \(n \in \mathbb{M} \Longrightarrow n \subset \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
\(\bigcup \mathbb{M} = \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s

<𝕄:0 … \(m , n \in \mathbb{M} \Longrightarrow m \in n \Leftrightarrow m \subsetneq n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
<𝕄:1 … \(m , n \in \mathbb{M} \Longrightarrow m \subsetneq n \textit{+1} \Leftrightarrow m \subset n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
\(\mathbb{M} \subset \mathbb{V}_0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
Cup𝕄 … \(m \in \mathbb{M} \Longrightarrow \bigcup ( m \textit{+1} ) = m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
<𝕄:T … \(m , n \in \mathbb{M} \Longrightarrow m \subset n \mathbin{\rm o\!r} n \subset m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s

1.3 自然数の記号

1以上の自然数 \({\tt n}\) に対し
word(,s) … \({\tt n}\)
\({\tt n}\). … \({\tt n} = \{ 0 , \cdots , {\tt n\,{\text -}\,1} \}\)
\({\tt n}\).. … \({\tt n} = ( {\tt n\,{\text -}\,1} ) \textit{+1}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
次の Thm は \({\tt n}\) についてのメタの帰納法で示されます。
\({\tt n} \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2以上の自然数 \({\tt n}\) に対し
∈\({\tt n}\) … \(0 \in 1 \in \cdots \in {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
≠\({\tt n}\) … \(0 \neq 1 , \cdots\!\cdots , {\tt n\,{\text -}\,2} \neq {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
⊊\({\tt n}\) … \(0 \subsetneq 1 \subsetneq \cdots \subsetneq {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
<\(\mathbb{M}\):0）を使用すると証明が速くなります。
⊊\({\tt n}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s