book集

section 準備
word ⋂_
prop ⋂_.
br
word 0
word suc ^suc
prop ^suc. <- `X ^suc =_ \{ n suc Cls n | n ∈ X \}`
br
word Ind
prop Ind.
word 𝕄
prop 𝕄.
br
txt \(\mathbb{M}\) は、\(0\) を含み後続で閉じた集合（帰納的集合）すべての共通部分。
txt なお、\(0\) と後続の中身を決めないので \(\mathbb{M}\) が無限集合とは限らない（\(0 = \emptyset\)、\({\rm suc}(n) = n \cup \{n\}\) とすれば、この仮定は無限公理に当たる）。

section 主定理
txt 一項述語\(p\)を使って、帰納法は以下の形で書かれる。
txt \(A = \{m \in \mathbb{M} \mid p(m)\}\) とすると、\(A\)が帰納的集合であることからすぐにわかる。
thm `?p^ (0) and [ ∀ n ∈ 𝕄 . ?p^ (n) ⇒ ?p^ (n suc) ] ⟹ [ ∀ n ∈ 𝕄 . ?p^ (n) ]` ◀ W. , ax_s
prf L𝕄1 <- `[ ∀ n ∈ 𝕄 . n suc ∈ 𝕄 ]` /// W.'!=. -| O p;
    A_ := `\{ cls m ∈ 𝕄 | ?p^ (m) \}` ;
    LAs <- `A_ ⊂_ 𝕄` /// W. -| O p;
    LEA <- `Exi A_` -| LAs , ax_s[C_:=`A_`] p;
    LE <- `[ ∃ A \, [ ∀ m (m ∈ A ⟺ m ∈ 𝕄 and ?p^ (m)) ] ]` -| LEA p;
    LI <- `?p^ (0) and [ ∀ n ∈ 𝕄 . ?p^ (n) ⟹ ?p^ (n suc) ] and [ ∀ m (m ∈ A ⟺ m ∈ 𝕄 and ?p^ (m)) ] ⟹ A ∈_ Ind` // W.!𝕄. -| L𝕄1 , 𝕄. p;
    LM <- `?p^ (0) and [ ∀ n ∈ 𝕄 . ?p^ (n) ⟹ ?p^ (n suc) ] and [ ∀ m (m ∈ A ⟺ m ∈ 𝕄 and ?p^ (m)) ] ⟹ 𝕄 ⊂ A` / W. -| LI , 𝕄. v;
    goal -| LE , LM / W.!𝕄. p;
    goal -| W. , ax_s h;

articles1/74.book

`articles1/74.book`