Computability and Logic（計算可能性と論理）

引用

Boolos, G. S., Burgess, J. P., & Jeffrey, R. C. (2007). Computability and Logic (5th ed.). Cambridge University Press.

章の要約

第5版は本文が約340ページ、全27章で、冒頭に第5版への序文、末尾に2ページの注釈付き文献案内が置かれている。章は互いに重なり合う三つの流れに分かれる。計算可能性理論、一階論理のメタ理論、そしてその両方を土台とする発展的な話題である。出版社の説明によれば、各章の終わりに演習問題が付く。

第1–2章：列挙可能性；対角化

本書は二つの短い章（pp. 3–22）で始まり、列挙可能性と対角化を扱う。後の限界定理が依拠する、数え上げと対角線論法の技法がここで用意される。

第3–5章：チューリング計算可能性；計算不可能性；アバカス計算可能性

これらの章（pp. 23–62）では二つの計算モデル、すなわちチューリング機械とアバカス機械を導入し、さらに計算できないものについて論じる章が続く。アバカス機械の章はチューリング機械の章より長い。

第6–8章：再帰関数；再帰集合と再帰関係；計算可能性の同値な定義

再帰関数による計算可能性の捉え方を展開し、それを集合と関係に適用する。この流れの最終章は、さまざまな計算可能性の定義を一つに結びつける（pp. 63–98）。

第9–10章：一階論理の概観：構文論；一階論理の概観：意味論

一階論理の構文論と意味論を凝縮して復習する章（pp. 101–125）。「概観」という語が示すとおり、初めて学ぶ人向けの導入ではなく、すでに一階論理の授業を受けた読者のための復習である。

第11章：一階論理の決定不可能性

計算可能性の議論の最初の大きな成果で、一階論理そのものに関する結果である（pp. 126–136）。

第12–14章：モデル；モデルの存在；証明と完全性

メタ理論のうちモデル論と証明論の中心部分（pp. 137–186）。章題は、完全性定理へとつながるモデル存在の議論を指している。

第15–18章：算術化；再帰関数の表現可能性；定義不可能性・決定不可能性・不完全性；無矛盾性の証明不可能性

不完全性へ向かう一連の章（pp. 187–240）。算術化と表現可能性が下地を作り、次の章が定義不可能性・決定不可能性・不完全性をまとめて扱い、最後に無矛盾性の証明不可能性へ進む。出版社は、この版の表現可能性の扱いを従来より簡潔な新しいものだと説明している。

第19–23章：標準形；クレイグの補間定理；一項述語論理と二項述語論理；二階論理；算術的定義可能性

狭い意味での論理に関するさらなる話題（pp. 243–294）。標準形とクレイグの補間定理から、一項・二項述語論理、二階論理を経て、算術的定義可能性に至る。

第24–27章：乗法を欠く算術の決定可能性；非標準モデル；ラムゼーの定理；様相論理と証明可能性

終盤の章（pp. 295–340）は、乗法を欠く算術の決定可能性、非標準モデル、ラムゼーの定理を順に扱い、最後に様相論理と証明可能性を論じる。

主要概念

計算可能性（第1–8章）

• 列挙可能性と対角化：無限の集まりの大きさを比べ、あるものが与えられたリストに現れえないことを示すための、冒頭の技法。
• チューリング計算可能性とアバカス計算可能性：有効な手続きに何ができるかを表す二つの形式モデル。
• 再帰関数：計算可能性の第三の特徴づけで、第8章で他の定義と同値であることが示される。

一階メタ論理（第9–14章）

• 一階論理の構文論と意味論：メタ定理の対象となる言語、解釈、真理。
• モデルと証明：完全性定理が確立する、すべてのモデルで真であることと導出可能性との結びつき。
• 一階論理の決定不可能性：妥当性を判定する一般的な手続きに課される限界。

不完全性と発展的話題（第15–27章）

• 算術化と表現可能性：構文を数でコード化し、計算可能関数を算術の内部で表現すること。
• 不完全性と無矛盾性の証明不可能性：本書が目指す限界定理。
• 補間、二階論理、非標準モデル、ラムゼーの定理、様相論理と証明可能性：後半の章題に挙げられた話題。

批判的分析

長所

• 一冊に幅広い話題を収める。 出版社は、本書が中級の論理学の授業で定番となる話題（ゲーデルの不完全性定理を含む）に加え、チューリングの計算可能性理論からラムゼーの定理に及ぶ多数の選択的な話題を扱うと述べている。目次もこれを裏づけており、第19–27章の章題は、主線の後に続く独立した話題になっている。
• 数学の素養がない学生を想定している。 出版社は、そうした学生にも読めることを本書が古典となった理由として挙げている。チューリング機械と並べてアバカス機械を用いるのは、この方針の表れの一つである。
• 各章末の演習問題。 出版社によれば、各章は演習問題の選集で終わり、第5版向けに調整されている。
• 表現可能性への簡潔な道筋。 再帰関数の表現可能性についての新しい扱いは、出版社が不完全性定理への道で従来つまずきの石だったと述べる箇所に対処するものである。

短所

• 一階論理の復習が凝縮されている。 第9章と第10章は概観にとどまるため、本書は一階論理の既習を前提としている。初めて学ぶ読者は別の本から始めるべきである。
• 範囲が定まっている。 章題から見る限り、本書は計算可能性、一階メタ論理、およびいくつかの発展的話題に限られる。証明論や集合論を本格的に学びたい読者には別の教科書が必要になる。
• 読む道筋を選ぶのに手間がかかる。 27章のうち多くが選択的であり、教員や独習者は何を省くかを自分で決めなければならない。目次は中核となる章を示していない。

コースにおける位置づけ

このコースの書籍リストの中で、数学的にもっとも要求水準が高い一冊である。『forall x（カルガリー版）』は、真理関数論理と一階論理をフィッチ式の自然演繹で扱う無料の入門書であり、コピの教科書は非形式的推論、三段論法、記号論理を扱う。どちらも最初の授業向けである。バーカー＝プラマー、バーワイズ、エチェメンディの『Language, Proof and Logic』は、一階論理の教科書とソフトウェアを組み合わせ、健全性、完全性、ゲーデルの第一定理の概略にまで達するので、本書が詳しく扱う領域にすでに触れている。セオドア・サイダーの『Logic for Philosophy』は哲学専攻の学生向けの二度目の論理学で、命題論理と述語論理について証明を与えたのち様相論理へ進む。もっとも近い代替となる本であり、二冊を並べて読むこともできる。

『Computability and Logic』は、形式論理の最初の授業を終えたあとで、チューリング機械、決定不可能性、不完全性定理の証明を詳しく見たいときの次の一冊である。

本書の使い方

形式論理の最初の授業を終え、限界定理の完全な証明を学びたい哲学・数学・計算機科学の学生に向く。出版社は数学の素養は不要だと強調しているが、証明を中心とする教科書なので、証明を辛抱強く読む姿勢が必要である。

実用的な進め方は次のとおり。第1–8章で計算可能性を学ぶ。第9–10章は復習として軽く読み、必要な概念が出てきたら戻る。第11–14章で決定不可能性、モデル、完全性を学ぶ。第15–18章は不完全性を扱うひとまとまりとして読む。第19–27章は関心に応じて選ぶ。第22章（二階論理）と第27章（様相論理と証明可能性）は哲学専攻の学生に自然な選択であり、第24–25章は算術とそのモデルに関心のある読者に向く。各章末の演習問題を解くこと。証明の技法を実際に使ってみると、証明が読みやすくなる。