数学的帰納法にまつわる話

ソクラテス・モロボシ @sokrates_chaos

帰納法、整列集合についての性質が大事だからどっちが強いとかないと思うのだけれど…… 上に有界な集合が有限である場合は同値になってくれるだけで……

スマートコン @mr_konn

Course of value induction も 普通のも互いに互いの特別な場合だからなあ

ソクラテス・モロボシ @sokrates_chaos

Peanoシステムから数学的帰納法抜いて代わりに累積帰納法を付け加えても同じ強さの体系になるのかしら (弱くなりそうな気もするけど

ソクラテス・モロボシ @sokrates_chaos

Nについて言及している場合は累積帰納法もフツーの帰納法も同値だから好きな方使えば良いのでは

ソクラテス・モロボシ @sokrates_chaos

帰納法は整列性があるから適用できるのだが……

Masaki Hara @qnighy

記号論理学の岡本先生は逆のことを言っていて、帰納法から累積帰納法は出るが累積帰納法から帰納法を出すには分解できるという性質が別に必要になるから、直感に反して帰納法のほうが強い。

Masaki Hara @qnighy

Wikipedia日本語版の帰納法のページにある無限降下法の定義は帰納法の亜種になってるけど、無限降下法の典型的な適用例といえばルート2の無理性証明だから、普通は累積帰納法の亜種として定義すると思う

スマートコン @mr_konn

そもそも「普通の」帰納法、typeがω-type 未満のでないと正しくない（結局limit stageが入る）しなあ

Masaki Hara @qnighy

僕が先ほど言ったのはNK+PAの話ですね。PAの帰納法図式の代わりとして累積帰納法図式を使うことはできない。

スマートコン @mr_konn

無限降下法、well-foundedness+¬-introでは

スマートコン @mr_konn

従って排中律あれば無限降下法は整礎帰納法になって、つまり完全帰納法になるはず。

スマートコン @mr_konn

えっ、なんでダメなんだろう

Masaki Hara @qnighy

他の公理として何を用意してるかによりそうだけど

Masaki Hara @qnighy

その時説明された公理系では、帰納法のかわりに累積帰納法を使うとnがSucまたは0であることが示せない。(つまり任意の極限順序数がモデルになる？)

スマートコン @mr_konn

あっそっか、その場合∀n(n=0 ∨∃m n=Sm) を公理に入れる必要があるのか

スマートコン @mr_konn

たしかに、ω+ωがモデルになりますね。

スマートコン @mr_konn

帰納法には排中律と従属選択公理がともに関わるから闇

koba @kobae964

cumulative inductionでは自然数がS _か0のどちらかであることが言えないことはわかった

スマートコン @mr_konn

でも∃のformulationに気をつければ(irrelevantでなくwitnessを取り出せるようにすれば)、DCくらいまではギリcomputationalな感じがする

スマートコン @mr_konn

公理はlimit stage指定してないし、ω+1でもモデルになるね

スマートコン @mr_konn

モデル上で同値性議論するのなら、真なる命題は全部同値だし偽なる命題もも全部同値だし1+1=2と完全帰納法も個別帰納法(?)も同値だけど、そういう議論してるんじゃないですよね、と不安になるツイートを見た

mod_poppo @mod_poppo

将来は帰納法になって世界を回したいです

スマートコン @mr_konn

回されるのはお前だ