Language, Proof and Logic（語言、證明與邏輯）

引用

Barker-Plummer, D., Barwise, J., & Etchemendy, J. (2011). Language, Proof and Logic (2nd ed.). CSLI Publications.

章節概要

Language, Proof and Logic（LPL）是一本與軟體配套的教材。Tarski's World 講授一階語言及其語義，Fitch 是構造和檢查證明的自然演繹環境，Boole 處理真值表，Submit 則把練習檔案提交給自動評分的線上服務 Grade Grinder。導論之後是分為三部分的19章，許多小節都明確標註為「（optional）」。書末有形式證明規則彙總、術語表，以及檔案、練習和綜合索引。據出版社介紹，第二版對原版作了大幅擴充和修訂：擴充了數學歸納法的內容（併為皮亞諾歸納和累積值歸納增加了軟體支持），改進了樸素集合論和策梅洛–弗蘭克爾集合論的講解。

導論

包括邏輯在理性探究中的特殊作用、為什麼要學習一種人工語言、後承與證明等小節；隨後是目錄中標為「必讀」的家庭作業說明，以及給教師的說明。

第一部分：命題邏輯

第1–2章：原子句、原子句的邏輯

第1章介紹個體常項、謂詞符號和原子句，另有關於函數符號、集合論和算術的一階語言以及其他記法的選讀小節。第2章定義有效論證和可靠論證，介紹證明方法和形式證明，說明如何在 Fitch 中構造證明，以及如何證明不構成後承。

第3–4章：布林聯結詞、布林聯結詞的邏輯

第3章講否定、合取和析取，一個用於判定語句真假的遊戲，歧義與括號，同義的不同說法，以及翻譯。第4章區分重言式與邏輯真理、重言等值與邏輯等值、重言後承與邏輯後承，在 Fitch 中處理重言後承，並有關於把否定內移以及合取範式和析取範式的選讀小節。

第5–6章：布林邏輯的證明方法、形式證明與布林邏輯

先講非形式證明：有效的推理步驟、分情況證明和反證法。第6章再給出合取、析取和否定的形式引入規則與消去規則、子證明的正確用法，以及尋找證明的策略和技巧。

第7–8章：條件句、條件句的邏輯

實質條件句和雙條件句、會話含義，以及選讀的真值函項完全性。第8章增加了條件句的非形式與形式證明方法、關於可靠性和完全性的選讀小節，以及第一部分的複習練習。

第二部分：量詞

第9–11章：量化導論、量詞的邏輯、多重量詞

第9章介紹變元、量詞符號、合式公式與語句、量詞的語義和四種亞里士多德形式，並練習翻譯複雜名詞短語。第10章討論一階有效性和後承、包括德摩根律在內的量詞等值式、關於公理化方法的選讀小節，以及引理。第11章處理混合量詞、逐步翻譯法、英語的改寫、歧義與語境敏感性，以及前束範式。

第12–13章：量詞的證明方法、形式證明與量詞

先講非形式方法：有效的量詞步驟、存在例示、一般條件證明以及含混合量詞的證明。隨後是 Fitch 中全稱和存在量詞的形式規則、策略與技巧，以及關於可靠性和完全性的選讀小節。

第14章：再論量化

數量量化及數量命題的證明，「the」「both」「neither」，在一階邏輯中加入其他限定詞，廣義量詞的邏輯，以及一階邏輯表達力的局限。

第三部分：應用與元理論

第15–16章：一階集合論、數學歸納法

第15章展開樸素集合論：空集、子集、交與並、有序對、關係和函數；選讀小節包括冪集、羅素悖論和策梅洛–弗蘭克爾集合論。第16章介紹歸納定義與歸納證明、自然數上的歸納以及 Fitch 中的歸納，並有關於自然數公理化和強歸納的選讀小節。

第17–19章：命題邏輯高階專題、一階邏輯高階專題、完全性與不完全性

第17章證明命題邏輯的完全性，另有關於霍恩語句和歸結法的選讀小節。第18章定義一階結構，重新討論真與滿足，證明一階邏輯的可靠性，並有關於斯科倫化、合一和歸結法的選讀小節。第19章用亨金構造證明完全性定理，接著討論勒文海姆–斯科倫定理和緊緻性定理，最後以哥德爾不完全性定理收尾。

核心概念

第一部分：命題邏輯

• 有效性與可靠性：當結論從前提中得出時，論證是有效的；如果前提也為真，論證就是可靠的。
• 重言後承與邏輯後承：僅憑真值函項聯結詞成立的後承，與更一般地憑意義成立的後承之間的區別。
• 菲奇式自然演繹：由引入規則和消去規則構成、用子證明處理臨時假設的形式證明。
• 真值函項完全性：一組聯結詞能否表達所有真值函項。

第二部分：量詞

• 一階有效性與後承：超出重言後承、僅憑量詞和同一性的意義而成立的後承。
• 翻譯：把英語句子（包括複雜名詞短語和混合量詞）逐步改寫為一階邏輯。
• 存在例示與一般條件證明：形式量詞規則所對應的非形式推理模式。
• 廣義量詞：諸如「most」「both」之類的限定詞，以及一階邏輯所能表達內容的界限。

第三部分：應用與元理論

• 數學歸納法：對歸納定義的集合（包括自然數）進行的證明。
• 可靠性與完全性：證明系統只證明、而且能證明全部有效後承。
• 緊緻性與勒文海姆–斯科倫定理：由完全性推出的、關於無窮語句集和模型大小的結論。
• 哥德爾不完全性定理：在一個一致的形式系統中無法證明全部算術真理的限制。

評析

優點

• 軟體融入學習過程。 據出版社介紹，配套程式讓學生構造世界、真值表和證明，Grade Grinder 能幾乎即時地為數百道上機練習評分。學生能迅速得到回饋，教師也免去了機械的批改工作。
• 先非形式，後形式。 從目錄看，每個邏輯主題都先有一章講非形式證明方法，再有一章講形式證明（第5–6章和第12–13章）。學生既學會在形式系統中推理，也學會用普通的數學語言推理。
• 選讀內容標註清楚。 選讀小節在目錄中有明確標註，課程可以沿著第一、二部分的核心路線推進，再選擇補充內容。
• 從入門到元理論。 出版社說本書不要求任何邏輯基礎，適用於入門課程和第二門課程；Openproof 網站則表示，由於第三部分講到完全性、緊緻性和哥德爾定理，本書從大學部第一門邏輯課到研究生第一門邏輯課都適用。
• 重視翻譯與自然語言。 書中有整節討論翻譯、英語改寫、會話含義和廣義量詞，體現出作者不僅關注證明，也關注語言。

局限

• 與軟體包繫結。 要充分利用本書，需要隨軟體包出售的註冊碼。出版社指出，註冊碼一經啟用便不可轉讓，因此二手書可能無法使用網路應用和評分服務。
• 篇幅長、內容密。 全書約600頁，第三部分遠遠超出第一門課程所需。
• 只講一階邏輯。 目錄中沒有模態邏輯、多值邏輯或其他非經典邏輯；第14章雖討論了一階邏輯表達力的局限，但哲學專業學生學習模態邏輯還需要另一本教材。

在課程中的定位

在這門邏輯課程中，LPL 是兩本採用菲奇式自然演繹的形式邏輯入門書之一。forall x: Calgary 是一本免費、開放許可的教材，用類似的證明系統講授真值函項邏輯和一階邏輯；它更短，也不需要軟體，適合想先輕鬆過一遍的學生。科皮的 Introduction to Logic 在一本書中涵蓋非形式推理、三段論邏輯、符號邏輯和歸納，因此比 LPL 更適合批判性思維課程。

學完 LPL 之後，西奧多·賽德的 Logic for Philosophy 是第二門課程的教材，它更嚴格地處理命題邏輯和謂詞邏輯，並補上 LPL 所缺的模態邏輯。布洛斯、伯吉斯和傑弗裡的 Computability and Logic 展開可計算性理論和各項限制性結果的完整證明；據出版社介紹，LPL 的第19章以哥德爾定理的概要收尾，可以作為通向該書的橋梁。

如何使用本書

本書不要求任何邏輯基礎。在開始做練習之前，先讀導論中關於家庭作業的說明，因為軟體和 Grade Grinder 本身就是練習的做法和提交方式的一部分。第一門課程通常講授第一、二部分（第1–14章）；作者基於這套教材製作的線上課程正好用14章講授這兩部分，並建議大約每週學習一章。第一遍學習時可以跳過選讀小節，除非老師另有安排。

先學非形式方法的章節，再學對應的形式章節；在進入 Fitch 證明之前，用 Tarski's World 把翻譯放到具體的世界中檢驗。第三部分適合第二門課程，或準備進入數學、電腦科學方向的學生：講集合論和歸納法的第15–16章是學習任何以證明為主的數學的良好準備，第17–19章則通向元理論。做練習時，可把書末的形式證明規則彙總和術語表當作參考資料。