全体的な印象

まずこの本は非常に丁寧な本だということだ。記述の正確さは当然のことながら、その精密さに驚く。随所に著者による注意が散りばめられ、何が重要なのかを示唆してくれる。またフォーマルとインフォーマルの区別が必ず文章の頭にあって、混乱がなるべく生じないように配慮があるのも嬉しい。一方で冗長と感じる部分もままある。特に邦訳特有の長回しが可読性をほんの少し、僅かながら下げていると言えなくもない。ただそれ以上に誤植が殆ど無いのが優秀。可読性について補足しておくと、「フォーマル」「インフォーマル」とか「セクション」「サブセクション」、「シンタックス」「セマンティクス」とかカタカナが原理上多くなってしまうとかいう程度の話。

著者のサイトは→なげやりアカデミア

第I章集合論

一章の内容は公理的に集合論を展開することなのだが、一つづつ公理を増やしていく構成が面白い。併せて順序数や基数について一般的な理論が展開される。加えて、ここまで書くかと思うところまで書いてあるし、足りない部分は参考文献をしっかり挙げてくれるのが嬉しい。

個人的に一番大事だなと感じた部分は、「順序数上の原始再帰」だろう。ざっくり言えば関数の再帰的定義がwell-definedということだが、論理式のレベルで厳密に構成できるというのが偉大な点。証明もそこそこ込み入っていて、一つの山場という感じ。この定理があるから我々は数学することができるといっても過言ではないと思う。このような記述は普通の数学をやっているとあまり気にしない点なので貴重に感じた。

基数の節から重要な話が続くのだが、演習問題が増えるためか、結果として内容は比較的あっさりしている。一章が長くなり過ぎたことを懸念したのかもしれないが、難度の高い部分なのでもう少し詳しく述べて欲しかったかもしれない。やり過ぎても本書の目的からは遠ざかるのかもしれないけど。

第II章モデル理論と証明論

前半はI章で得た集合論の結果を前提に、シンタックスとセマンティクスの間に成り立つ完全性定理を証明することが一つの山場となっている。まずはシンタックスで使う用語の定義から始まるのはどの本も同じだが、こちらは置き換え・割り当てについてかなり丁寧な記載がある。形式的な記号の列に解釈を与えてセマンティクスを議論するときに大事なのは真理値表。先にコンパクト性定理やレーヴェンハイム・スコーレムの定理などが紹介されている。形式証明は推論規則にモーダス・ポーネンスのみを採用するヒルベルト流だけど、全ての命題論理のトートロジーを公理に加えるなど、キューネンなりの工夫が加えられている。いずれにせよ動機や具体例などの記述は多く、細部に渡る配慮はI章と変わらない。完全性定理の証明も具体例から必要な要素を取り出して、それらを解決する形で構成されていて面白い。

ちなみに172ページの1行目

${ (6) \forall x \neg \varphi \rightarrow \neg \exists x \varphi }$