1 準備

word(c,c) … \(\bigcap\)
⋂_. … \(\bigcap \mathcal{X} = \{ x \mid \forall X \in \mathcal{X} . x \in X \}\)

word(,s) … \(0\)
word(s,s) … \(\textit{+1}\)  \(\hat{\textit{+1}}\)
^suc. … \(X \hat{\textit{+1}} = \{ n \textit{+1} \mid n \in X \}\)

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}\)

\(\mathbb{M}\) は、\(0\) を含み後続で閉じた集合（帰納的集合）すべての共通部分。
なお、\(0\) と後続の中身を決めないので \(\mathbb{M}\) が無限集合とは限らない（\(0 = \emptyset\)、\({\rm suc}(n) = n \cup \{n\}\) とすれば、この仮定は無限公理に当たる）。

2 主定理

一項述語\(p\)を使って、帰納法は以下の形で書かれる。
\(A = \{m \in \mathbb{M} \mid p(m)\}\) とすると、\(A\)が帰納的集合であることからすぐにわかる。
\({p} ( 0 ) , \forall n \in \mathbb{M} . {p} ( n ) \Rightarrow {p} ( n \textit{+1} ) \Longrightarrow \forall n \in \mathbb{M} . {p} ( n )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s