Not logged in / Log in

articles1/74b.book(保存済みの内容) … 編集へ / ファイル一覧へ

数学的帰納法(クラス版帰納法から)
import /common/word_basis.book

1 準備

word(,s) … \(\mathbb{M}\)  \(0\)
word(s,s) … \(\textit{+1}\)
このBookでは \(\mathbb{M}\) は定義せず、クラスについての帰納法 IND𝕄 を公理として置く。
IND𝕄 … \(0 \in C , \forall m \in \mathbb{M} . ( m \in C \Longrightarrow m \textit{+1} \in C ) \Longrightarrow \mathbb{M} \subset C\)

2 主定理

一項述語 \(p\) を使った帰納法は、IND𝕄 の \(C\) を \(\{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.bookとの関連

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

74a.book では \(\mathbb{M}\) を \({\rm Ind}\) の共通部分として定義し、このBookの公理 IND𝕄 を定理として示している。
\(\mathbb{M}\) は \({\rm Ind}\) の共通部分に含まれる。
\(\mathbb{M} \subset \bigcap \text{Ind}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ,IND𝕄
\(\mathbb{M}\) が帰納的集合なら逆も成り立ち、\(\mathbb{M}\) は \({\rm Ind}\) の共通部分(74a.book の \(\mathbb{M}\) の定義)になる。
\(\mathbb{M} \in \text{Ind} \Longrightarrow \bigcap \text{Ind} \subset \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

イベント 15 件