Computability and Logic（可計算性與邏輯）

引用

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

章節概要

第五版正文約340頁，共27章，前有第五版序言，末有兩頁的帶註釋參考書目。各章大致分為三條互相交疊的線索：可計算性理論、一階邏輯的元理論，以及建立在二者之上的一組拓展專題。出版社說明，每章末尾附有一組習題。

第1–2章：可列舉性；對角化

全書以兩個短章開篇（第3–22頁），講可列舉性與對角化。它們提供了後文各項限制性結果所依賴的計數與對角論證技巧。

第3–5章：圖靈可計算性；不可計算性；算盤可計算性

這幾章（第23–62頁）介紹兩種計算模型，即圖靈機與算盤機，並有一章討論哪些東西不可計算。算盤機一章比圖靈機一章篇幅更長。

第6–8章：遞迴函式；遞迴集與遞迴關係；可計算性的等價定義

先展開用遞迴函式刻畫可計算性的路徑，再把它應用於集合與關係，這條線索的最後一章把各種可計算性定義匯合到一起（第63–98頁）。

第9–10章：一階邏輯概要：句法；一階邏輯概要：語義

對一階邏輯句法與語義的壓縮回顧（第101–125頁）。“概要”一詞表明，這是寫給已修過相關課程的讀者的複習，而不是初次介紹。

第11章：一階邏輯的不可判定性

可計算性內容的第一項重要收穫：一個關於一階邏輯本身的結果（第126–136頁）。

第12–14章：模型；模型的存在性；證明與完全性

元理論中模型論與證明論的核心部分（第137–186頁）。章名指向通向完全性定理的模型存在性論證。

第15–18章：算術化；遞迴函式的可表示性；不可定義性、不可判定性與不完全性；一致性的不可證明性

不完全性的主線（第187–240頁）。算術化與可表示性鋪墊基礎，下一章把不可定義性、不可判定性與不完全性放在一起處理，最後一章轉向一致性的不可證明性。出版社稱，本版對可表示性的處理是全新的，比以往更簡單。

第19–23章：範式；克雷格插值定理；單謂詞與雙謂詞邏輯；二階邏輯；算術可定義性

狹義邏輯中的進一步專題（第243–294頁），從範式和克雷格插值定理，經單謂詞與雙謂詞邏輯、二階邏輯，到算術可定義性。

第24–27章：不含乘法的算術的可判定性；非標準模型；拉姆齊定理；模態邏輯與可證性

最後幾章（第295–340頁）依次討論不含乘法的算術的可判定性、非標準模型、拉姆齊定理，最後是模態邏輯與可證性。

核心概念

可計算性（第1–8章）

• 可列舉性與對角化：開篇的技巧，用於比較無窮集合的大小，並證明某物不可能出現在給定的列表中。
• 圖靈可計算性與算盤可計算性：關於有效程序能做什麼的兩種形式模型。
• 遞迴函式：可計算性的第三種刻畫，第8章表明它與其他刻畫等價。

一階元邏輯（第9–14章）

• 一階邏輯的句法與語義：元定理所討論的語言、解釋與真。
• 模型與證明：完全性定理所確立的“在所有模型中為真”與“可推導”之間的聯絡。
• 一階邏輯的不可判定性：任何判定有效性的一般程序都受到的限制。

不完全性與拓展專題（第15–27章）

• 算術化與可表示性：用數來編碼句法，並在算術內部表達可計算函式。
• 不完全性與一致性的不可證明性：全書最終通向的限制性結果。
• 插值、二階邏輯、非標準模型、拉姆齊定理、模態邏輯與可證性：後面各章章名中列出的專題。

評析

優點

• 一冊之內涵蓋豐富的主題。 出版社稱，本書既涵蓋中級邏輯課程的常規主題，包括哥德爾不完全性定理，又包括從圖靈可計算性理論到拉姆齊定理的大量選學內容。目錄印證了這一點：第19–27章的章名都是接在主線之後的獨立專題。
• 面向沒有數學背景的學生。 出版社把對這類學生的可讀性視為本書成為經典的原因，在圖靈機之外使用算盤機，是這一定位的一個具體表現。
• 每章末附習題。 據出版社介紹，每章末都附有一組習題，並已針對第五版作了調整。
• 更簡化的可表示性路徑。 本版對遞迴函式可表示性的全新處理，針對的是出版社所說的通向不完全性定理途中的傳統難關。

局限

• 對一階邏輯的回顧很濃縮。 第9、10章只是“概要”，因此本書預設讀者已學過一階邏輯；需要初次講解的讀者應先讀別的書。
• 範圍固定。 從章名看，本書限於可計算性、一階元邏輯及若干拓展；想系統學習證明論或集合論的讀者需要另找他書。
• 選擇路線需要費一番功夫。 全書27章，其中許多是選學，教師或自學者必須自行決定取捨；目錄並未標出哪些是核心。

在課程中的定位

在本課程書單中，這是數學要求最高的一本。《forall x（卡爾加里版）》是免費的入門教材，講真值函式邏輯與一階邏輯，採用菲奇式自然演繹；科匹的教材涵蓋非形式推理、三段論與符號邏輯；兩者都是第一門課。Barker-Plummer、Barwise 與 Etchemendy 的《Language, Proof and Logic》把一階邏輯教材與軟體配合使用，並講到可靠性、完全性和哥德爾第一定理的概述，所以已經觸及本書詳細處理的領域。賽德的《Logic for Philosophy》是為哲學專業學生設計的第二門邏輯課，先證明命題邏輯與謂詞邏輯的結論，再轉向模態邏輯；它是最接近的替代選擇，兩書可以對照閱讀。

《Computability and Logic》適合在學完形式邏輯第一門課之後閱讀，目的是詳細看到圖靈機、不可判定性和不完全性定理的證明。

如何使用本書

本書適合已學完形式邏輯第一門課、想看到限制性定理完整證明的哲學、數學和計算機專業學生。出版社強調不要求數學背景，但這是一本以證明為主的教材，需要有耐心讀證明。

一個可行的計劃：讀第1–8章學習可計算性；把第9–10章當作複習略讀，需要某個概念時再回頭查；讀第11–14章學習不可判定性、模型與完全性；把第15–18章作為一個整體讀，學習不完全性。第19–27章按興趣選讀：第22章（二階邏輯）與第27章（模態邏輯與可證性）對哲學專業的學生尤為合適，第24–25章則適合關心算術及其模型的讀者。完成每章末的習題，因為用過證明技巧之後，證明會更容易讀懂。