数学的帰納法(クラス版帰納法から)
import /common/word_basis.book(section 2 まで)
このBookでは \(\mathbb{M}\) は定義せず、クラスについての帰納法 IND𝕄 を公理として置く(74a と別の構成)。
1 準備
word(,s) …
\(\mathbb{M}\) \(0\)word(s,s) …
\(\textit{+1}\)IND𝕄 …
\(0 \in D , \forall m \in \mathbb{M} . ( m \in D \Longrightarrow m \textit{+1} \in D ) \Longrightarrow \mathbb{M} \subset D\) 2 主定理
一項述語 \(p\) を使った帰納法は、IND𝕄 の \(D\) を \(\{m \mid p(m)\}\) とすればすぐにわかる。
\({p} ( 0 ) , \forall n \in \mathbb{M} . \, ( {p} ( n ) \Rightarrow {p} ( n \textit{+1} ) ) \Longrightarrow \forall n \in \mathbb{M} . \, {p} ( n )\) \(\blacktriangleleft\) IND𝕄3 74a との関連
word(s,s) …
\(\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(c,c) …
\(\bigcap\)⋂_. …
\(\bigcap \mathcal{X} = \{ x \mid \forall X \in \mathcal{X} . x \in X \}\) \(\mathbb{M}\) が帰納的集合なら逆も成り立ち、74a.book の定義が定理となる。
\(\mathbb{M} \subset \bigcap \text{Ind}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ,IND𝕄 \(\mathbb{M} \in \text{Ind} \Longrightarrow \bigcap \text{Ind} \subset \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\)