久しぶりに戸次先生の数理論理学を読みました。演習問題をひたすら解きながら思ったのですが、駒場で受けた記号論理学の講義はだいぶまずい構成だったのではないかな。述語論理の意味論をきちんとやらずに証明論をやっていた気がする。意味論をきちんと定義して、その意味論と証明体系の証明が一致するというのがあのへんの計算のなんかすごいところなのであって、それを抜きにした証明の練習ってただのゲームじゃん、みたいな。まあ、僕の出てない日に扱ってたのかもだけれど。
とはいえあの講義のおかげで僕は意味を無視して形式を考えることの面白さを学んだわけで、それはすごく良かったと思います。
そういえば最近は形式ではなく処理系があるのだということを考えています。
