「現代数理論理学序説」（古森雄一・小野寛晰）

現代数理論理学序説

本日、Amazonより到着。現代的な数理論理学について知りたければ最適*1の入門書だと思います。計算機科学の人にもお勧め*2。出版社のwebsiteによると章の構成は以下の通り。

• 第1章　命題論理
  • 1.1　論理学と形式的体系
  • 1.2　命題論理の体系
  • 1.3　ゲンツェンの基本定理
  • 1.4　古典命題論理の意味論
• 第2章　述語論理
  • 2.1　述語論理の体系
  • 2.2　ゲンツェンの基本定理
  • 2.3　古典述語論理の意味論
• 第3章　ラムダ計算の世界
  • 3.1　ラムダ計算の計算能力
  • 3.2　ラムダ項の型付けとη変形
• 第4章　非標準論理
  • 4.1　直観主義論理
  • 4.2　論理と代数
  • 4.3　様相論理
  • 4.4　部分構造論理

内容に関してですが、

• 古典論理の意味論の話が第一章の後半まで出てこないので、伝統的な教科書に慣れた人は面食らうかもしれません（そういう人ほどこの本を読んで欲しい）。
• 前半では、命題論理・述語論理に証明論的にアプローチ・
  • 命題論理パートは、組み合わせ論理(combinatory logic)→ヒルベルト流→λ計算と自然演繹→列計算と言う流れ。そして証明の正規化とλ項の正規化をほぼ同時に扱うあたり、非常に現代的なアプローチ。
  • λ項の変換の話と、証明の式変形の話を同時並行に進めるため、自然にカリー・ハワード対応が頭に入るようになっています。これは、非常にうまいやり方だと思います*3。
  • 命題論理・述語論理共に、グリベンコの定理を前面に押し出し*4、演繹の構成に関するメタの帰納法による証明法の題材としています。
    • その意味で、単に多種多様な論理体系を紹介するだけではなく、異なる論理体系間の対応関係に注目しているため、有益だと思います。
    • ちなみに、他に演繹の構成に関する帰納法の代表例として有名なカット除去はグリベンコの定理の次、そして古典論理の完全性定理はその次に扱われています*5。
• 後半ではλ計算（決定不可能性定理など）に一章、非古典論理（直観主義論理・代数的論理学・様相論理・部分構造論理！）に一章。
  • とくに、代数的論理学に関する部分は必見。
  • 後半の二章に関しては、スタンド・アローンで証明を最後までみっちりという形ではなく、最新の話題に関するaccessibleな紹介として見た方がいいでしょう。しかし、それにしても、「序説」を謳う日本語の本で、 BCK論理とかバーコフの定理とかカテゴリ文法とランベック計算といった話題を見る日が来ようとは思わなかった…。

なお、本書を企画された亀書房さんのweb site で、将来的には、練習問題の答えを掲載されるそうです。

*1:というか類書を知らない

*2:哲学の人にもお勧め…と言いたいところだけど…彼らの場合、入門の教科書というよりは最先端の論理学の研究分野の（ハイレベルな）案内書として捉えるべきかも。

*3:が、せっかくなら、古典論理の紹介の前に、BCK論理を紹介し、BCK→FLe→直観主義→古典として欲しかった…

*4:そういえば、小野先生の教科書でも、グリベンコの定理は結構大きな扱いでした。

*5:通常の教科書では、古典論理の完全性定理で〆とするものが多いので、その意味でも扱いの差が面白く思えます。