日々の流転

λ. 『数学』を数学的に考える

某所で紹介されていたので、読んでみた。扱っている内容は以前に読んだ「算術的階層の厳密性と形式的手法の限界について」とほぼ同じなのかな。

帰納法をΣ_n論理式に制限した IΣ_n というのが出てくるのだけど、これが有限公理化可能と書いてあって驚く。 そのことをTwitterに書いたら、ytbさんが「Hajek-Pudlakのp78に載ってます(定理2.52)。Σn論理式に関する真理述語を使うと、IΣ1の有限部分理論において、Σn論理式をそのゲーデル数と同一視でき、Σn帰納法の公理図式を一つの公理として表現できるとか。」とサクっと答えてくれて、「おお、なるほどー」と思った。 もっとも、これが気になった理由は、有限公理化出来ると定理証明器的に嬉しいのではと思ったためだったので、Σ_n論理式に関する真理述語を使うとなると全然嬉しくなさそうだけどね。

それと、照井先生は「文レベルの局所的な循環性ではなく、対象数学とメタ数学の大域的な循環性に目を向けるべき」と言っていて、そういえばこないだの数学基礎論サマースクール2009の Cut-elimination and Algebraic Completion でも「個別に論理を作ってカット除去とかを証明してというのではなくて、そもそも証明論の限界とは？」という話をしていたのを思い出す。 すごく大域的な視野というかビジョンを持って数学をしている感じがして、やはり凄いと思った。