整礎帰納法？

ホワット・ア・ワンダフル・ワールド - FC2 BLOG パスワード認証
コメントしようと思ったのですが、なんか長くなりそうなのでトラバで。もちろんネタは整礎帰納法と超限帰納法の違いについて。

整礎帰納法もwell-founded inductionも聞いたことありませんでした(爆)。もちろん手法としては知っていますが。論理式の複雑さに関する帰納法が典型例ですね。
超限帰納法というのはすなわちωより大きい順序数に拡張された帰納法です。一番普通な形としてはこんな感じ。「φを述語とする。全ての順序数αに対して、もし全ての順序数β<αについてφ(β)が成り立っているならば、φ(α)が成り立つことを仮定する。このとき全ての順序数に対してφ(α)が成り立つ」。なんでφ(0)を明示しなくてもいいの？とかは頭の体操ってことで。
数学的帰納法(のちょっと強い形)は、超限帰納法をωステージでちょん切ったものになります。

整礎帰納法の定義は多分、「φを述語とし、(S, <)を整礎な集合とする。全てのSの元xに対して、もし全てのy<xについてφ(y)が成り立っているならば、φ(x)が成り立つことを仮定する。このとき全てのSの元xに対してφ(x)が成り立つ」というものでしょう。これだとすれば、超限帰納法は整礎帰納法の特別な形ということになります。*1なぜかといえば、順序数は(同型を除いた)整礎な全順序構造と一対一に対応しているからです。ですので、整礎全順序集合に制限した整礎帰納法が超限帰納法ということになります。

もっとも、プログラミングに関する帰納法で、ωより大きい高さを持つ整礎集合やωより大きい順序数が出てくることって多分少ないので、ここに書いたことはあんまり意味がないです。…最初に書けよ、それ。

*1:あー、ここで書いたそのままの定義を使うとちょっとごまかしてますが、ごまかさせてください。