独白

不完全性定理 - 白のカピバラの逆極限 S.144-3で話していてなんか違和感があった理由がわかってきました。他の皆さんは最初から証明の方に重きを置いているので弱い算術とかも割りと普通に受け止められるのではないかと(もしくは切り替えが効いているかですね)。
私にとってはモデルが最初にあって、そこでの現象を把握するために証明があるんです。どちらでも構わないっていうのが健全性＋完全性ではあるわけなんですが、やっぱりイメージはかなり変わってくるかと思います。集合論をやる場合には、普通の証明の言葉で書き直すのが厄介な議論が多いので、モデルを中心にイメージするようになりやすいのではないかと邪推します。そして、集合論における整合性証明なんかはそれで何の問題も無いわけです。連続体仮説が否定されるモデルでは本当に個の実数が存在しているわけですから。
ところが、強い算術と弱い算術の違いをモデルの方で表現しようとすれば、非標準的な自然数を使うしかありません。まあ、強いほうに矛盾が無ければですが。にもかかわらずそれらが記述しているのは標準的な自然数のことであるように書かれている。というところに違和感があったような気がします。
もちろん、標準的な自然数に関して証明できる命題の違いとして強弱の算術を理解することも可能なわけですし、それを皆さんやってらっしゃったような気がします。でも、その感性は私には無いな、と。

このあたり、数学哲学の問題に入ってくるわけなんですが、そちらは聞きかじりなのでこの辺でやめておきます。