巨大数とビジービーバー

Takayuki Kihara @tri_iro

@non_archimedean ご丁寧に説明ありがとうございます。ああなるほど、超越整数は、ZFC-可証全域計算可能関数だけに制限したビジービーバーみたいなことをしてるわけですね。

p進大好きbot @non_archimedean

@tri_iro そうです！　僕の好きな計算可能巨大数生成システムの１つです！

Takayuki Kihara @tri_iro

@non_archimedean ありがとうございます。こちらからのビジービーバーに関するコメントはこれくらいです。どうも長々とお付き合い頂きありがとうございました。

Takayuki Kihara @tri_iro

@non_archimedean （他にもACA_0がペアノ算術と同じ強さ、Z_2＋PDとZFCとn-Woodin基数の証明力が同じ、など不正確な記述（proof-theoretic strengthという用語の勘違い？）もありますが、まあこの辺はふぃっしゅさんに直接言うのがいいですね）

p進大好きbot @non_archimedean

@tri_iro こちらこそありがとうございます。あと決定性公理についてもいろいろ教えてくださってありがとうございます。いつか勉強したら決定性公理でも巨大関数作りたいです。

p進大好きbot @non_archimedean

@tri_iro その辺は僕が個別の証明力や表現力について疎いので全然気に留めてませんでした。確かに公理系の『強さ』は界隈全体として（というか形式体系そのものを扱わない数学全体として？）結構雑な言い方をすることも多いと思うので、どこか間違っていたらご指摘してあげて下されば幸いです。