強い数学的帰納法のひみつ

イベント内容

定理証明支援系 Isabelle/HOL や Coq で、帰納的に集合や述語を定義すると、数学的帰納法の規則が生成されます。

たとえば Isabelle/HOL で偶数の集合を帰納的に定義すると、こんな感じです：

inductive_set E where
  base: "0 ∈ E"
| step: "n ∈ E ⟹ Suc (Suc n) ∈ E"

thm E.induct
  ⟦?x ∈ E; ?P 0; ⋀n. ⟦n ∈ E; ?P n⟧ ⟹ ?P (Suc (Suc n))⟧ ⟹ ?P ?x

帰納法の仮定をみると、ふつうの P n に加えて n ∈ E というものがあります。これははなんでしょう？

帰納法の仮定に条件が追加されているわけですから、仮定が強くなっているということです。つまり、証明しやすくなっているわけです。どうしてこのようなことができるのでしょうか。

このような強い数学的帰納法がなりたつことの証明を追ってみたいと思います。証明を追っていくのでなかなかたいへんですが、興味があればどうぞ。

Isabelle/HOL の知識を前提とします。

注意事項