数理逻辑导引 · 从推理的语法到机器的极限

本书怎么读：一门关于「推理能否被机器执行」的学问

这不是一本教材，而是一册入门书：全书只讲一件事——数理逻辑，即「把推理写成符号，再问符号能推出什么」的学问。它回答的问题朴素而尖锐：什么才算一个证明？证明能不能被机械地检查？有没有一种算法判定任一命题的真假？为什么一个足够强的形式系统证明不了自己的一致性？两千多年里，逻辑从亚里士多德的三段论（第一套推理规则）走到弗雷格的《概念文字》（1879，语言的转向），再经希尔伯特纲领（把数学变成符号游戏）、哥德尔的完备性与两条不完备定理（1929／1931）、Gentzen 的切割消除（1934）、图灵机与不可判定（1936），最终长成今天可以在 Lean、Coq 里跑起来的形式化数学。全书按章组织：绪论用三段论、莱布尼茨之梦与希尔伯特纲领提炼主题；第一章把真假变成可计算的真值表；第二章升到一阶逻辑并给出完备性定理，沿途参观希尔伯特几何、一阶算术与 Tarski 初等欧氏几何三套公理系统；第三章让证明本身成为研究对象（相继式、切割消除、证明即程序）；第四章回答「什么能机械地算」（图灵机、停机问题、不可判定）；第五章完整走出哥德尔两条定理，并在此交代希尔伯特第一问题（连续统假设）为何被判「独立」；第六章走向当代——证明助手、同伦类型论、逆向数学与人工智能中的逻辑；综合站用年表、人物谱、概念总图、实验与自查收束全书。

写作的三条约束（本书的自我要求）。① 直觉与图形先行：每个概念都从一张图、一个具体的小例子讲起——先在真值表上逐行穷举、把一条推理画成树、把一台图灵机的纸带摊开看读写头怎样游走、把哥德尔编码逐位译回句子，再抽成定义。② 一步一图：凡能画的都画——推理树、相继式证明的形状、图灵机纸带与状态图、编码对照表、五种几何的模型图。③ 自给自足：所需的集合记号、归纳法与初等数论在书内随用随补，不假设手边另有教材；个别深刻结论（完备性定理、两条不完备定理、力迫法）给出精确陈述与证明路线，计算对拍在实验页随附。

页型节奏。每章以 导引 开篇（一页说清这一章要解决什么）；主体是 讲义 页（定义、定理、证明，一步一图）；每章配 例题 与 习题（末附提示）；每章收在 地图（依赖关系）＋小结＋思想卡（把技术升成观念）＋挑战与实验（动手核验）；另有 〖札记〗格物札记做中西思想传统的对照。每页右上角标页码，页眉灰色小字标出所属章与页题。

难度标记。讲义页首行用 ★–★★★★★ 标出阅读难度：★ 高中基础即可，★★ 需要集合与计数的基本功（书内自给），★★★ 需要一点抽象经验（等价关系、商结构，书内自给），★★★★ 需要形式证明与归纳的功夫（书内自给），★★★★★ 触及不完备性、力迫法与前沿（第五章、第六章）。若只求理解主线，读绪论、第一章、第二章的完备性定理、第四章的停机问题即可；若求完整掌握，按章顺序逐页推进，并把每章习题做完。

三条线索贯穿全书：

① 明线——从三段论到可运行的证明：先把推理写成符号（绪论），再把真假变成真值表（第一章），升到一阶逻辑并证明完备性（第二章），让证明成为研究对象（第三章），回答机器能算什么（第四章），走到可证性的边界（第五章），最后看见数学在计算机里被逐行验证（第六章）——这正是逻辑一百八十年从「辩论术」长成「工程学」的轨迹。

② 暗线——每一次「显然」都要过形式化的关。「这句话是真的」显然吗？说谎者悖论说否。「这个证明没错」显然吗？切割消除定理要求它可被机械检查。「这个系统不会自相矛盾」显然吗？第二不完备定理说它证明不了。「所有几何都用同一套公理」显然吗？五种几何的模型给了否定的答复。找出「哪些直觉可信、哪些必须形式化、哪些命题永不可判」，是全书反复演练的判官功夫。

③ 接口——通往四个邻域。数理逻辑是数学与计算的共同语法：与集合论（ZFC 与力迫法，第五章、第六章直接合流）、模型论（公理与模型、可判定性，第二章、第三章）、计算（图灵机、复杂度、程序验证与证明助手）、数学基础与哲学（构造主义、希尔伯特纲领与它的终结）四条战线相通。相邻领域中的序数、基数、选择公理与力迫法，在本册中被反复调用与重讲，对读互证。

写法约定（TEX 标准）：命题用 p, q, r、公式用 φ, ψ（变量斜体）；联结词 ¬ ∧ ∨ → ↔、量词 ∀ ∃、可证 ⊢、满足 ⊨、结构用花体 𝒜, ℬ, ℳ、理论记 T、图灵机记 M、停机问题记 H、连续统假设记 CH。变量斜体，系统名与算子（ZFC、PA、Prov、Con、LK）正体；关键一步配图，直觉与证明逐章对照。

绪论 推理的语法：从三段论到符号本册导引：把「推理」写成符号

人每天都在推理。看见天边压着乌云，就断定要下雨；听说某人身在另一座城，就断定他此刻不在家。这些「从已知滑到未知」的动作顺滑得几乎不需要练习。可一旦追问一句：这一步凭什么成立？换一个人来做，会不会滑向别的结论？——问题立刻变得既朴素又尖锐。数理逻辑的全部工作，正是把这种「滑」的动作用符号钉下来，再逐字检查它。

本册讲一门既古老又年轻的学问：数理逻辑。说它古老，是因为源头可以追溯到公元前四世纪的亚里士多德；说它年轻，是因为真正的现代化要到十九世纪末才起步，而它最锋利的结论——证明有极限、机器有盲区——全部诞生在二十世纪。本册要回答四个问题。第一，什么是形式语言：像 p → q 这样的符号串怎么读、怎么算。第二，什么是证明：从公理到定理的那一串符号，凭什么算作证明。第三，什么是可计算：机器能做的推理与做不到的推理，边界画在哪里。第四，什么是可证的极限：为什么足够强大的形式系统也证明不了自己的清白。

为看清这条线索，本册反复回到三个场景。真值表把一切可能逐行穷举，是「语义」的化身；证明树把推理的每一步摊开，是「语法」的化身；纸带把计算交给一台只懂读写与移动的机器，是「可计算」的化身。三者合起来，就是二十世纪逻辑学的主干。

本册还有一条自我约束值得先交代：凡「显然」，必过形式化的关。一个论断「显然为真」不足为凭，它要么能被规则推出来，要么就不是定理；一个系统「显然不会自相矛盾」也不足为凭，哥德尔会说明，这件事系统自己说不清。全书就是持续的「过秤」：把直觉放上去，看它几斤几两。

读法建议：凡标有「完整证明」的定理，都在纸上跟着写一遍。逻辑这门学问的特点是——看懂不等于会做，会做才算看懂。

绪论 推理的语法：从三段论到符号亚里士多德的三段论：第一套推理规则

★ 逻辑作为一门有规则的技艺，起点通常定在公元前四世纪的雅典。亚里士多德在《工具论》的《前分析篇》里第一次系统地写下：什么样的推理形式，无论把词换成什么内容，都必然有效。这套学说叫三段论（syllogism），它统治了此后两千年的逻辑教学。

三段论处理的是直言命题，即断定某类对象与某类对象之间包含或不包含关系的句子。亚里士多德区分出四种形式，后世用四个元音字母称呼它们。

一个三段论由两个前提、一个结论组成，句中只出现三个词项：大词 P（结论的谓词）、小词 S（结论的主词）、中词 M（只在两个前提里出现、负责搭桥）。中词摆放的位置决定格，四个字母的搭配决定式；格与式合起来，就定死了推理的形状。

三段论的关键在于形式：只要形状对，内容随便换都成立。「所有猫是动物；所有动物是生物；所以所有猫是生物」和「所有 M 是 P；所有 S 是 M；所以所有 S 是 P」是同一个推理的两副面孔。亚里士多德甚至把二十余种有效形式逐一列出，让「有效性」第一次成为可以对照清点的对象。

两千年后的裂缝。三段论只认得「主词—谓词」这一种结构，遇到关系就失灵。有一条显然有效的推理：「所有人是动物，所以所有人之头是动物之头。」结论必然成立，却带着一个前提里没出现过的词——「头」。要表达「x 是 y 的头」这种两项之间的关系，直言命题的语言不够用；「每个数都有一个比它大的数」这样的多重量词，也找不到安身之处。这些裂缝一悬就是两千三百年。

补一句常被忽略的公案：与亚里士多德平行的还有公元前三世纪的麦加拉—斯多亚学派（克里西普斯等人）。他们研究的不是主谓包含，而是「如果……那么……」这种联结结构，相当于另一条通往命题逻辑的支线。两支流派要到很晚才真正汇合。

绪论 推理的语法：从三段论到符号莱布尼茨之梦：把争论交给计算

★★ 亚里士多德把推理写成了规则，可规则仍要靠人来执行。能不能再进一步，把推理本身交给计算？这个大胆的念头，最早由莱布尼茨在十七世纪明确说出。

莱布尼茨（Gottfried Wilhelm Leibniz，1646–1716）身兼哲学家与数学家，发明了微积分的符号体系，也发明了二进制。他一生念念不忘两样东西：一套普遍文字（characteristica universalis），把人类全部概念分解为基本概念、各配一个符号；一部推理演算（calculus ratiocinator），让符号按固定规则运算，从而把一切结论推出来。

他给这套设想留下了一句流传最广的话：Calculemus——让我们计算。设想两人意见相左，不必再吵，只需说一声：让我们算一算。算完，谁对谁错自然见分晓。这几乎是「把推理变成可检查对象」最早的宣言。

莱布尼茨还亲自做了准备：他设计二进制，主张一切推理都可归约为符号的机械操作。可这梦想要搁浅两百年——不是缺勇气，是缺工具：当时既没有成熟的符号语言，也没有一套能把「且、或、非」当作运算的代数。

两百年后的 1847 年，英国数学家布尔（George Boole，1815–1864）让一本小册子《逻辑的数学分析》问世，把逻辑第一次真正代数化。七年后的 1854 年，他写出《思维规律的研究》，直言推理的法则就是「思维的规律」，可以写成方程。布尔的做法惊人地简单：把「类」（集合的雏形）当作运算对象，让 xy 表示「既是 x 又是 y」的类，让 x + y 表示「是 x 或是 y」的类，让 1 − x 表示「不是 x」的类。于是推理变成了解方程。

布尔逻辑里有一条与算术分道扬镳的定律：x² = x（对同一个类重复取交集，结果不变）。这条幂等律宣告逻辑代数不是普通代数，而是一种新代数；后世的「布尔代数」正由此得名，第一章将专门重访它。

不过布尔的逻辑仍停留在类与主谓的层面：他有了运算，还没有量词——说不出「对一切」与「存在」，也说不出两项之间的关系。要把莱布尼茨之梦真正推进一步，需要一次语言的革命。

绪论 推理的语法：从三段论到符号弗雷格与《概念文字》：语言的转向

★★★ 布尔让逻辑会算数了，却还算不出「对一切」与「存在」。补上这一环的是德国数学家、逻辑学家弗雷格（Gottlob Frege，1848–1925）。1879 年，他出版了一本只有几十页的小书——《概念文字》（Begriffsschrift），副标题是「一种模仿算术语言构造的纯思维的形式语言」。今天公认，现代逻辑从这一页开始。

弗雷格做了三件破天荒的事。

第一，把「所有」和「有的」变成算子。在三段论里，「所有 S 是 P」是一个整体句式；弗雷格把它拆成：对每一个个体 x，若 x 是 S 则 x 是 P，前面再加一个「对一切」的符号。量词一旦成为算子，就能一层套一层地嵌套。

第二，把「关系」请进逻辑。三段论说不出的「x 是 y 的头」，在弗雷格的语言里只是把单项谓词 P(x) 换成两项的 R(x, y)。前面那条显然有效却无处安放的关系推理立刻可以形式化，「所有人之头是动物之头」不再是逻辑的漏网之鱼。

第三，用「函项—自变量」取代「主词—谓词」。弗雷格把概念看成不完整的函项：像 x² = 1 这样的表达式缺一个自变量，填进去才成句。命题与概念于是被统一到同一种分析下——这正是后来一阶逻辑「项与公式」两分的雏形。

语言的转向。这三件事合起来，是一次研究对象的迁移：逻辑不再直接盯着「思维」，而盯着表达思维的符号语言。既然推理要用语言承载，那就先把语言造得没有歧义，再在符号上谈推理。史称这场迁移为「语言的转向」。

弗雷格的雄心不止于逻辑。1884 年的《算术基础》里，他提出逻辑主义纲领：算术的真理归根到底是逻辑的真理，数可以用逻辑概念定义。为落实它，他写了两卷《算术的基本法则》。可惜的是，正当第二卷付印之时，他收到罗素的一封来信——信中一个悖论，恰好击中全书的根基。弗雷格在附录里写下那句沉痛的告白：一个科学家所能遭遇的最难堪的事，莫过于自己大厦将倾之际，被人指出地基早已开裂。

绪论 推理的语法：从三段论到符号希尔伯特纲领：把数学变成符号游戏

★★★ 十九世纪末二十世纪初，数学正经历一场地基大检视：微积分被严格化推着重写，集合论刚由康托尔开创，罗素的悖论又给朴素集合论凿开一个洞。面对满地裂缝，希尔伯特（David Hilbert，1862–1943）提出一个雄心勃勃的回应：与其零敲碎打地修补，不如把整个数学一次性建成一个可控的形式系统。

1900 年，希尔伯特在巴黎国际数学家大会上提出著名的 23 个问题，为二十世纪的数学列出清单。清单的第二个问题语出惊人：证明算术公理系统是一致的——从它推不出矛盾。这个要求看似技术，实则致命：一个能推出矛盾的数学系统，原则上可以证明任何命题，一切结论同时为真又同时为假，谈不上「可靠」二字。

二十年代，希尔伯特把这一诉求发展成一整套纲领。它的构想分三层：

这套纲领有一个立竿见影的副产品：它把「证明」本身变成了一门可研究的对象。既然证明是符号串，那么证明的长度、形状、能否化简，统统成了数学问题。这正是证明论（proof theory）的诞生，第三章会给它一整章的篇幅。

1928 年，希尔伯特与阿克曼出版《理论逻辑原理》；同年，他在波隆那的国际数学家大会上，把纲领里最后一个悬而未决的问题正式摆上台面——判定问题（Entscheidungsproblem）：是否存在一个机械程序，对任意给定的一阶命题，都能在有限步内判定它是否可证、是否有效？换句话说，数学的真理能否被一台忠实执行规则的机器一网打尽？

希尔伯特对这套纲领充满信心。1930 年，他在柯尼斯堡的演讲以一句口号收尾：我们必须知道，我们必将知道（Wir müssen wissen, wir werden wissen）。讽刺的是，正是在同一年，年轻的哥德尔在这个城市的同一系列会议上宣布：一个足够强的形式系统，若一致，必不完备——纲领的完备性与可判定性两端，注定落空。

绪论 推理的语法：从三段论到符号逻辑的三次危机：悖论、不完备与不可判定

★★★ 从亚里士多德到希尔伯特，逻辑一路在壮大：推理被写成规则、写成代数、写成量词，最后被写成一场符号游戏。可就在这座大厦看似封顶之际，接连落下三记重击。它们合称「逻辑的三次危机」——说「危机」，是因为每一次都让当时的最高期望落空；说「不是危机」，是因为每一次都长出了一片新天地。

第一次：罗素悖论（1901）。朴素集合论有一条看似天经地义的原则：任何一个明确的「性质」，都对应一个集合，由满足该性质的对象组成。罗素（Bertrand Russell，1872–1970）盯上了这条原则本身。定义集合 R 为「一切不把自己当作元素的集合」：

R = { x : x ∉ x }.

现在问一句：R 是不是它自己的元素？若 R ∈ R，按定义它必须满足「不自属」，即 R ∉ R；若 R ∉ R，它又满足定义、应被收进 R，即 R ∈ R。两头一逼，得到

R ∈ R　⟺　R ∉ R,

一个自相矛盾的等价式。这记重拳正中弗雷格刚刚结卷的《算术的基本法则》：那个悖论用的正是他赖以定义数目的概括原则。修补之道是收缩原则——罗素与怀特海在《数学原理》（1910–1913）中用类型论分层，策梅洛（Zermelo）1908 年给出公理化集合论（后经扩充为 ZFC），把「想造什么集合就造什么集合」改成「按公理逐条造集合」。

第二次：哥德尔不完备（1931）。希尔伯特指望用有穷方法证明算术一致，哥德尔（Kurt Gödel，1906–1978）证明这条路走不通。他的两条定理是：一个一致且能表达基本算术的形式系统，必定存在既不能证明也不能否证的命题（第一不完备定理）；并且这样的系统无法在自身内部证明自己的一致性（第二不完备定理）。这里有一个常被混淆的对照必须分清：1929 年，哥德尔先证明了一阶逻辑的完备性——凡是逻辑有效的公式都可被推出；两年后，他证明的是算术理论的不完备性。完备性属于逻辑，不完备性属于数学理论，两句话一点也不矛盾。

第三次：图灵不可判定（1936）。还剩一线希望：即使系统不完备，也许存在一个机械程序，能逐一判定任意命题是否可证？图灵（Alan Turing，1912–1954）用一个极简的抽象机器（图灵机）给「机械程序」下了精确定义，随即证明：不存在这样的程序。他先证明著名的停机问题不可判定——没有任何算法能对任意机器与输入判断它会不会停；据此推出希尔伯特的判定问题无解。同年丘奇（Church）用另一套工具得到相同结论，这就是丘奇—图灵论题的由来。

危机的另一面。三记重击并非全盘否定，而是划定边界：逻辑证明了自己能做什么（一阶逻辑完备、证明可机械检查），也证明了自己不能做什么。可计算性理论与证明论这两门学科，正是从危机中长出来的新大陆。本册后半程将逐一走进这三记重击的内部。

绪论 推理的语法：从三段论到符号本册路线图：六章的远征

★★ 前面几页把「从哪里来」讲完：三段论、莱布尼茨之梦、弗雷格的转向、希尔伯特纲领、三次危机。从第一章起，旅程正式出发，共六章，每章解决一个大问题，同时沉淀一批标准工具。

第一章　命题逻辑：真值表与推理的骨架。先把真假本身变成可计算的对象：五个联结词、真值表、重言式、范式、函数完备性，然后是形式证明与健全性、完备性。命题逻辑足够简单，简单到能被完整地算清楚——它是全书的地基，也是「可判定」的第一个成功范例。

第二章　一阶逻辑：量词、结构与完备性。加入量词、变元、关系与结构，逻辑的表达力跃升；再证明哥德尔完备性定理：逻辑有效的公式都可被推出。沿途参观希尔伯特几何、一阶算术与 Tarski 初等欧氏几何三套公理系统，看形式化如何落地。

第三章　证明论：相继式、自然演绎与切割消除。把「证明」自身当作对象：自然演绎的引入与消去、相继式演算、Gentzen（1934）的切割消除定理、直觉主义的分岔，直到「证明即程序」的深层对应。

第四章　可计算性：图灵机与不可判定。给「机械地算」下定义，走进停机问题的完整证明，再用归约把不可判定性扩散开来，最后看一眼 P 与 NP 的资源世界与算法的边界地图。

第五章　不完备性：哥德尔的两条定理。哥德尔编码、可证性谓词、对角线引理，完整走出两条不完备定理；并交代连续统假设为何被判「独立」于集合论公理。

第六章　逻辑的当代面孔。证明助手（Coq、Lean、Isabelle）、同伦类型论、构造主义与逆向数学，以及逻辑在数据库、模型检测与人工智能中的身影——逻辑正在变成一门工程。

三条线索贯穿全书。明线是从三段论到可运行的证明——把推理写成符号，再把符号交给机器；暗线是每一次「显然」都要过形式化的关——哪些直觉可信，哪些必须形式化，哪些命题永不可判；接口是逻辑与集合论、模型论、计算、数学基础四条战线相通。行李清单并不长：集合与映射的基本记号、归纳法、一点初等数论，这些在书内随用随补，不假设手边另有教材。

绪论 推理的语法：从三段论到符号绪论小结与预习清单

本页任务。把绪论的行李清点一遍：哪些年份必须记准，哪些概念必须带走，哪些问题留作路标。

概念清单。① 三段论与直言命题：亚里士多德用 A、E、I、O 四种句式把推理形式化，中词搭桥，格与式定形状；② 莱布尼茨之梦：普遍文字加推理演算，Calculemus「让我们计算」；③ 布尔代数：把「且 / 或 / 非」变成「乘 / 加 / 补」，x² = x 的幂等律划开逻辑与算术；④ 弗雷格的转向：量词成为算子、关系进入逻辑、函项取代主谓，「语言的转向」由此发生；⑤ 希尔伯特纲领三问：一致性、完备性、可判定性；⑥ 三次危机：罗素悖论、哥德尔不完备、图灵不可判定。

年表（史实年份须记准）。

路标问题（各章的靶心）。① 命题逻辑为何可判定？（第一章）② 一阶逻辑为何完备？（第二章）③ 证明能否化简、能否机械化？（第三章）④ 什么是可计算、什么是不可判定？（第四章）⑤ 足够强的系统为何不完备？（第五章）⑥ 逻辑如何走进工程？（第六章）

预习提示。第一章会密集使用集合记号、归纳法与一点初等数论。若手感生疏，自测三件小事：① 把「p 与 q 中至少一个为真」写成符号；② 用归纳法证明 1 + 2 + ⋯ + n = n(n + 1)2；③ 复述「等价关系」的三条性质。三件小事都顺手，第一章可以放心加速。

行李点清，出发。第一章的号令只有一句：先把真假变成可以计算的东西。

第一章 命题逻辑：真值表与推理的骨架第一章导引：让真假可以计算

绪论把「推理」立成一个必须被逐行核对的物件，也留下一个问题：最小的那块砖长什么样？本章给出答案——把每一句陈述的真假压成一个符号 0 或 1，把每一个连接词压成一张有限的小表。于是推理不再玄妙：一句话对不对，或者把一张表算到底，或者把一串规则查到底。

这条路分两股。一股是语义：给命题变元指派真假，用真值表穷举一切可能，看哪些公式在所有指派下都取真（重言式），哪些公式彼此同真同假（逻辑等价）。另一股是语法：把「允许的推理步」写成规则，把「证明」定义成一串可以逐行验收的符号，完全不提真假，只看符号怎样变形。本章最重的两块基石，正是最后证明这两股路合流：语义上恒真的公式，恰好就是语法上可证的公式——命题逻辑的健全性与完备性。

五阶路线如此展开。第一阶（§1.1–1.4）语义：五个联结词、真值表、重言式与逻辑等价、析取与合取范式——把「真假」变成可计算的对象。第二阶（§1.5）完备性：证明单独一个 NAND 或 NOR 就能搭出全部联结词，语言由此可以极简。第三阶（§1.6–1.8）语法：肯定前件与假言三段论、演绎定理、自然演绎、形式证明的定义——让「证明」成为一串可检查的符号。第四阶（§1.9–1.11）元定理：健全性、完备性、紧致性、布尔代数——回答「语法与语义为什么一致」。第五阶（§1.12–1.15）机器：可判定性、开关电路、SAT 与 NP 完全、卢卡西维茨公理系统——让逻辑落到硅片上，也落到公理的骨架里。

常驻嘉宾：一个公式。本章从 §1.2 起反复使用一个具体公式——「若 p 蕴含 q，且 q 蕴含 r，则 p 蕴含 r」，写成符号即

((p → q) ∧ (q → r)) → (p → r).

它小到真值表只有八行，却足够承载全章的概念：在 §1.2 它是真值表的第一号标本；在 §1.3 它是重言式的样板；在 §1.6 它是假言三段论规则的另一副面孔；在 §1.7 它由一个演绎定理的证明兑现；在 §1.10 它再次作为紧致性里的有限片段出场。与它保持熟络——读完本章，应当能在三分钟内默写出它的真值表，并说清它为什么恒真。

读法建议：凡标着「完整证明」的定理，纸笔重写一遍。逻辑这门手艺的特点是——看懂只算见过，写对才算学会。

第一章 命题逻辑：真值表与推理的骨架1.1 命题与联结词：五个按钮

★ 逻辑的最小单位是一句话的真假。本节把「一句话」切成两样东西：不可再分的原子（命题变元），与把它们拼接起来并决定真假的黏合剂（联结词）。五个联结词就是五个按钮，每个按钮的行为由一张有限的小表写死。

五个联结词分别是：否定 ¬（一元），合取 ∧、析取 ∨、蕴含 →、等值 ↔（二元）。关键在于它们不是靠「意思」定义的，而是靠「表」定义的——表怎么定，词就怎么算。下表就是这五个按钮的全部说明书。

逐列读这张表，各联结词的性格一目了然。¬ 只做一件事：把 0 翻成 1、把 1 翻成 0。∧ 苛刻，只有两真才真。∨ 宽容，只要有一真即真（注意这是兼容的「或」，不是日常「要么这样要么那样」的排他或——排他或将成为习题里的明星）。↔ 数「相同」：两值一样则真。

真正需要停一秒的是 →。表告诉我们：p → q 只有在 p 真而 q 假时才是假，其余三行一律为真——这叫实质蕴含。它带来的第一个「反直觉」是：前件为假时整个蕴含自动为真。于是「若 2 + 2 = 5，则雪是黑的」按此定义是一个真命题。这不是诡辩，而是形式化的纪律：若要把「如果……那么……」当成一个只依赖真值的算子，它的表只能这么填——否则推论规则（下一节）就无法成立。把「→ 不是因果，也不是推理过程」这句话记牢，本章后半程会反复回来算这笔账。

为省括号，约定结合优先级由紧到松为 ¬ > ∧ > ∨ > → > ↔；同级的 ∧ 与 ∨ 左结合。例如 p ∨ q ∧ r 读作 p ∨ (q ∧ r)。凡省略会引起歧义处，一律补括号，宁可啰嗦。

练习式观察。把日常语言翻译成符号：令 r 表示「下雨」、u 表示「带伞」，则「如果下雨，我就带伞」写作 r → u；「既没下雨也没带伞」写作 ¬r ∧ ¬u；「或者下雨，或者带伞（至少一件）」写作 r ∨ u。第一句翻成 → 之后，它在「没下雨」的两行自动为真——这正是形式化必须付出的代价与获得的收益。

第一章 命题逻辑：真值表与推理的骨架1.2 真值表：穷举一切可能

★★ 一个公式含 n 个命题变元，每个变元只有真、假两种取值，于是全部可能的指派恰有 2ⁿ 种。真值表就是把它们一行一行摊开，逐行算出公式的值。这是本章最笨、也最可靠的方法：它把一个「是否恒真」的疑问，换成一次有限的查表。

造表的纪律是「由内向外、逐列求值」：先给每个变元列出全部取值的组合，再按公式的构造顺序，先算子公式、后算母公式。以常驻嘉宾 φ = ((p → q) ∧ (q → r)) → (p → r) 为例，它有三个变元，八行，需要依次计算 p → q、q → r、(p → q) ∧ (q → r)、p → r，最后一列才是整个公式。

末列八个 1，无一例外。亲手补一遍中间几列——这是全章唯一一次可以「按机械劳动换确定性」的机会，务必亲手走过。观察一个易错点：第 3 行里 q → r 取 0，于是合取列取 0；但合取为 0 只说明前提包没被满足，母公式的前件为假，整个蕴含反而为真。这条「前件假 ⇒ 蕴含真」的规则是全表恒真的关键，也是初学者最容易数错的地方。

真值表把「恒真」这个性质变成了一次可完成的检查。但它有一个代价，本页先把账记下、留到 §1.12 细算：行数随变元数指数增长。n = 10 时 1024 行尚可忍受，n = 20 时上百万行，n = 60 时已超过宇宙原子的数量级。真值表是「原则上可达」的，却未必是「实践上可行」的——这条裂缝，最终撕出了计算复杂性这一整片天地（§1.14）。

另一种读法。真值表还可以反过来用：它是一张「公式的行为指纹」。两个公式若真值表逐行相同，就在一切场合表现一致——这正是下一节「逻辑等价」的定义来源。所以真值表不只回答「是否恒真」，更提供了一个判等、分类与查错的通用仪表盘。

第一章 命题逻辑：真值表与推理的骨架1.3 重言式与逻辑等价

★★ 真值表把公式按「行为的脾气」分成三类。本节给这三类命名，并由此引出全章最常用的一件工具——逻辑等价，以及它背后一条精美的对称律：对偶原理。

三类之间的换算值得记牢：φ 是重言式 ⟺ ¬φ 不可满足；φ 是矛盾式 ⟺ ¬φ 是重言式。重言式与可满足性是一枚硬币的两面——这一点在 §1.14 会变成「判定重言式与判定可满足性同样难」的复杂度等价。

符号上要分清两把不同的尺子：↔ 是语言内部的联结词，它造出一个新公式；而 ≡ 是语言外部的断言，它说「这两个公式恒同真值」。同理 ⊨ 也是外部记号。此时不妨先把「内部 vs 外部」这条线记住，§1.8 会把它升格为「对象语言 vs 元语言」。

下表列出最常备的等价律，它们是把复杂公式化简、改写、变形的基本钳工工具。

「蕴含改写」与「逆否」是本章出现频率最高的两条。p → q ≡ ¬p ∨ q 把蕴含化成纯粹的和差，下一节的范式构造全靠它；逆否律 p → q ≡ ¬q → ¬p 则解释了「反证法为什么合法」：要证 p → q，可以改证它的逆否命题。

对偶原理的直觉来自德摩根：把「非」推入括号内层，∧ 会翻成 ∨、∨ 会翻成 ∧。于是给一个公式整体取反，等价于给它对偶化后再把每个变元取反。这条律省下了大量重复劳动：证了一条分配律，它的对偶版本自动到手；写了一份真值表，它对偶版的表也一并写好了。

本节的落点可以一句话概括：真值表把公式分类，等价律把公式变形，对偶律让变形成对出现。下一节要证明一件更强的事：无论公式多复杂，它都能被整理成两种标准形状之一——析取范式与合取范式。这等于宣布，命题逻辑里「所有的公式」其实只长成有限几种样子的组合。

第一章 命题逻辑：真值表与推理的骨架1.4 范式：析取与合取的规范写法

★★ 等价律能做变形，但变形可以千变万化，缺少一个「终点」。本节给出两种标准终点：析取范式与合取范式。令人安心的是，终点不但存在，而且在固定变元集合的意义下唯一——任何一个公式，都有一张只属于它的「标准身份证」。

构造法（真值表法）。先写真值表，再「照抄真行」。设 φ 在某行的取值为 1。把该行中取 1 的变元写成自身、取 0 的变元写成其否定，再把这些文字全部用 ∧ 连成一个合取子句——这个子句只在该行取 1，称为该行对应的极小项。把 φ 所有取 1 的行对应的极小项全部用 ∨ 连起来，就得到主析取范式：它恰好在 φ 为真的那些行取 1。对偶地，把 φ 取 0 的行对应的极大项（取 0 的变元写自身、取 1 的写否定，再用 ∨ 连）全部用 ∧ 连起来，就得到主合取范式。

唯一性为什么成立。主析取范式为真的行集合，恰是它所含极小项的指标集合；若两式等价，则两式的真值列相同，故极小项指标集合相同，于是两式只差子句次序。这就是「不计次序唯一」的全部内容——唯一性不是深奥的定理，而是「真值列决定一切」的直接推论。由此还得到一条极好用的判据：两个公式等价，当且仅当它们的主析取范式（在同一变元集合下）相同。

唯一性带来一个漂亮的计数：含 n 个变元的公式，其主析取范式由「选哪些极小项」完全决定，而极小项共 2ⁿ 个，故不同的真值函数共有 2²ⁿ 个。这条计数将直接支撑下一节的函数完备性——「所有 n 元布尔函数」不是一团不可名状的东西，而是一个可以被数出来的有限集合。

范式还有一个实践上的用途，将在 §1.14 兑现：把公式写成 CNF 之后，「哪些指派能满足它」变成一个可以交给机器的查表问题。SAT 问题的输入标准就是 CNF。所以本节不只是理论整理，它同时在为「机器如何读逻辑」制定文件格式。

第一章 命题逻辑：真值表与推理的骨架1.5 函数完备性：NAND 独自撑起一切

★★★ 范式告诉我们：任一公式都等价于「选取若干极小项」的组合。既然选极小项要用到 ¬、∧、∨ 三个联结词，那么这三件工具是否够用了？本节把这个问题问到底，并把答案推到极端——只用一个联结词就够。

证明。任取公式 φ，由定理 1.6，φ 等价于其主析取范式 (l₁₁ ∧ … ∧ l_1n) ∨ … ∨ (l_k1 ∧ … ∧ l_kn)，其中每个 l 是变元或其否定。该范式只用到 ¬、∧、∨ 三者，故它们能表达任意 φ。∎

证明。先看 {¬, ∧}：析取可用德摩根律写出 p ∨ q ≡ ¬(¬p ∧ ¬q)，于是在完备集 {¬, ∧, ∨} 里把每个 ∨ 替换成该式即得只用 {¬, ∧} 的表达式。{¬, ∨} 对称地由 p ∧ q ≡ ¬(¬p ∨ ¬q) 得证。{¬, →} 则由蕴含改写 p ∨ q ≡ ¬p → q 与 p ∧ q ≡ ¬(p → ¬q) 得到。∎

到此为止，每去掉一个联结词，都需要「否定」留守——¬ 似乎是不可替代的。真的如此吗？下面这个联结词将证明 ¬ 也可以一并省去。

证明。只需用 ↑ 表达出完备集 {¬, ∧} 的两个成员，再由定理 1.10 的传递性即得。

证明。平行地：¬p ≡ p ↓ p；p ∨ q ≡ (p ↓ q) ↓ (p ↓ q)；p ∧ q ≡ (p ↓ p) ↓ (q ↓ q)。于是 ↓ 表达了完备集 {¬, ∨}，故完备。∎

这两个定理把「语言的最小化」推到极限：整个命题逻辑，可以只用一种门来建造。它并非纸上奇观——真实的数字电路正是以 NAND 门为基本砖块，工程师偏爱它，因为它的晶体管实现最省、最稳（§1.13 再看）。一个更一般的问题留作余韵：哪些联结词单独够用？答案是 ↑ 与 ↓ 这两个「独裁者」。Post 在 1920 年代给出了完整的分类定理，在习题中尝到它的边角。

第一章 命题逻辑：真值表与推理的骨架1.6 推理规则：肯定前件与假言三段论

★★ 前五节都在描述公式的真假，接下来要问：怎样从一组前提出发，合法地走到结论？本节给出第一批推理规则，它们是形式证明的螺丝钉。

把「有效」落成可执行的检验，只需一张真值表：凡是前提全真的行，结论那一列也必须真。只要找到一行前提全真而结论为假——这叫反例指派——论证立即无效。一票否决，干脆利落。

下面两条规则是本章使用频率最高的推理动作。

为什么这两条规则合法？用真值表一击即可：只要 p 与 p → q 同真，p → q 的真值表就逼着 q 为真（否则蕴含为假）；HS 的合法性则正是 §1.2 那张八行表恒真的另一种说法——常驻嘉宾公式说的就是「HS 有效」。推理规则与重言式，其实是同一件事的两副面孔：一个说「这样写合法」，一个说「这样写导出的公式恒真」。

常用的规则还有一批，列在下面的卡片里。它们都可以用真值表逐条验证，自证其中两条。

与规则同样重要的是认清谬误。肯定后件（由 p → q 与 q 推 p）与否定前件（由 p → q 与 ¬p 推 ¬q）都无效：把 (p,q) = (0,1) 代入，前件假、后件真，p → q 仍真，却足以让这两个「推理」的结论翻车。承认 → 只谈真假、不谈因果，就是避免踩进这两个坑的关键。

本节留下的问题是：这些规则用法千变万化，如何保证「每一步都合法」？答案是把证明当作一个符号序列，逐步验收——这正是 §1.7 与 §1.8 的主题。

第一章 命题逻辑：真值表与推理的骨架1.7 演绎定理与自然演绎

★★★ 人在推理时会说「假定 φ 成立……于是 ψ 成立，所以 φ → ψ」。这个日常动作要合法化，就需要演绎定理；而把各类规则组织成一套贴近人的证明书写法，则得到自然演绎。

证明（要点）。右推左方向容易：若 Γ ⊢ φ → ψ，那么在原证明后再接一步「由 φ 与 φ → ψ 经 MP 得 ψ」，其中 φ 现成取自新增的前提——于是 Γ ∪ {φ} ⊢ ψ。左推右方向对证明的长度作归纳：设 ψ₁, …, ψ_n 是从 Γ ∪ {φ} 出发到 ψ 的证明。逐行证明每个 Γ ⊢ φ → ψ_i：若 ψ_i 是公理或属于 Γ，则 ψ_i 可证，再由公理 ψ_i → (φ → ψ_i)（即 §1.15 的第一条公理 A1）与 MP 得 φ → ψ_i；若 ψ_i 就是 φ 本身，则 φ → φ 可证（§1.15 将演示）；若 ψ_i 由前面两行 ψ_j 与 ψ_j → ψ_i 经 MP 得到，则用归纳假设得 φ → ψ_j 与 φ → (ψ_j → ψ_i)，再由公理 A2 (φ → (ψ_j → ψ_i)) → ((φ → ψ_j) → (φ → ψ_i)) 两次 MP 得 φ → ψ_i。归纳到底即 Γ ⊢ φ → ψ。∎

演绎定理的实践意义叫条件证明：要证 φ → ψ，可以先「假定 φ」，把 φ 当作临时前提推出 ψ，然后宣布蕴含成立。这条策略把许多难证的目标化成一个顺着走的推导。

自然演绎干脆把这条策略写进规则。它给每个联结词配一对动作：引入（把该联结词造出来）与消去（把它拆开用）。核心规则如下。

看 →I 的运作方式：把「假定 φ」这一段的推导放进一个假设盒，盒内可以自由使用 φ；当盒内推出 ψ，就把盒子关上，在盒外写下 φ → ψ。盒内的 φ 不能拿到盒外使用——这条「封装」纪律正是演绎定理在书写层面的化身。若把 →I 与演绎定理并读，会发现二者说的是同一件事：「临时假设」与「蕴含」是一体两面。

自然演绎与下一节的「公理系统 + 规则」路线形式不同，效力却一致：两者可证的东西完全相同（可互相模拟）。前者像人，直观、好写；后者像机器，条目统一、易于分析。命题逻辑的健全性与完备性，对两者都成立——§1.9 就走元定理那条路。

第一章 命题逻辑：真值表与推理的骨架1.8 形式证明：证明的语法是什么

★★★ 「证明」这个词在数学里一直靠默契运转。形式逻辑要做的事，是把它变成一件可以机械检查的物件。本节给出定义：一个证明，就是一串符号，加上一台逐行核对器。

先说两种语言。逻辑学家区分对象语言与元语言。对象语言是被研究的符号系统本身（公式 p → q、联结词、公理）；元语言是我们谈论对象语言时用的语言（「φ 是重言式」「Γ ⊢ ψ」）。本页的定理都是元语言里的陈述，而它们说的对象是对象语言里的符号串。这条区分是读懂整个元数学的前提。

定义里每个字都在为「机器可检」服务。序列有限，所以检查会终止；每个 φ_i 的身份只依赖「是否公理 / 是否假设 / 由前面哪几项按哪条规则得到」，所以检查只需逐步查表，不需要任何「洞察」。

形式证明有几条立刻可用的性质，都由定义直接读出。

注意「有限性」这条看似平淡的性质，会在紧致性里放大成定理。形式证明的力量恰恰来自它的贫瘠：它只允许有限的符号操作，因而每一步都能被审计。把推理限制到可检查的程度，换来的是确定性——这是本册反复出现的主旋律。

最后留一句预告。Γ ⊢ φ 是一条存在性陈述：存在某个符号序列。它与 Γ ⊨ φ（一条普遍性陈述：一切指派都如此）看上去毫不相干。下一节要证明的，恰恰是这两条看似无关的陈述其实处处同步——这就是命题逻辑的健全性与完备性。

第一章 命题逻辑：真值表与推理的骨架1.9 健全性与完备性（命题版）

★★★★ 语法说「符号能变形到」，语义说「真假处处如此」。本节证明它们步调一致——先证「能证的必真」（健全性），再证「必真的能证」（完备性）。后者是本章的顶点，走极大一致集（又称 Lindenbaum 扩张）路线。

证明。对证明长度归纳。设公理系统的一切公理都是重言式（§1.15 的三条公理各自如此，又任意代换入公理仍得重言式）。取任一满足 Γ 的指派 v，归纳证明序列中每一项 φ_i 都满足 v(φ_i) = 1：若 φ_i 是公理，则是重言式，故取 1；若 φ_i 是假设，由 v 满足 Γ 故取 1；若 φ_i 由 φ_j 与 φ_j → φ_i 经 MP 得到，则两项的归纳假设给出二者皆真，而 v(φ_j) = 1 与 v(φ_j → φ_i) = 1 逼出 v(φ_i) = 1。特别地末项 φ 取 1。由于 v 是任取的满足 Γ 的指派，得 Γ ⊨ φ。∎

完备性走一条等价的路。先证一个形式上更整齐的命题：每个一致的公式集都可满足。它与完备性等价，但结构更清晰。

把两条定理合起来：Γ ⊢ φ ⟺ Γ ⊨ φ。符号的变形能力与真值的必然性完全吻合——这正是希尔伯特所说的「逻辑的可靠性」：形式系统不会证出假的东西（健全），也不会漏掉真的东西（完备）。

这一路线的每一块砖都已在本章铺好：一致与矛盾的语法定义（§1.8）、演绎定理（§1.7）、蕴含改写为析取（§1.3）。完备性定理并非孤立奇观，而是本章前半全部工具的合流。命题逻辑的第一个伟大定理，就此收口。

第一章 命题逻辑：真值表与推理的骨架1.10 紧致性的命题版：从有限到无限

★★★★ 上一节的完备性有一个立竿见影的推论：整体可满足，只取决于每个有限片段可满足。这条性质看似平淡，却能把无穷多个条件的问题压缩成有限次可检验的条件，是本章最有「魔术感」的一条定理。

证明。一个方向是显然的：若 v 满足整个 Γ，则它自然满足 Γ 的任一子集，特别地满足每个有限子集。

另一个方向用反证。设 Γ 的每个有限子集都可满足，但 Γ 本身不可满足。由定理 1.24 的逆否（不可满足蕴含不一致），Γ 不一致，即存在 φ 使 Γ ⊢ φ 且 Γ ⊢ ¬φ。而任何证明都只有有限行（§1.8），两个证明实际动用的假设合起来仍只有有限多条——记为 Γ₀ ⊆ Γ，则 Γ₀ ⊢ φ 且 Γ₀ ⊢ ¬φ。由健全性（定理 1.23），Γ₀ ⊨ φ 且 Γ₀ ⊨ ¬φ；但这不可能，因为满足 Γ₀ 的指派会同时逼出 φ 与 ¬φ 都取 1。于是 Γ₀ 不可满足，与「每个有限子集可满足」矛盾。故 Γ 可满足。∎

证明短得近乎狡猾：它没有直接构造满足 Γ 的指派，而是绕道「不可满足 ⇒ 不一致 ⇒ 有限个假设就够用 ⇒ 某个有限子集不可满足」。整条链的关键，是证明的有限性——那个在 §1.8 里不起眼的性质，在这里变成了从无穷跨向有限的桥。

这个例子的震撼之处在于：结论本身是「存在一个全局着色」，而所用的全部证据只是「每个有限部分都有着色」。紧致性把「整体存在」悄悄换成了「局部存在的可检查总和」。同样的手法可以推出「任意偏序集可扩张为全序」的有限版本，以及一阶算术存在非标准模型（含大于一切自然数的元素）——后者是第五章哥德尔定理的舞台布景。

与完备性一样，紧致性的所有部件都来自本章：一致性（§1.8）、健全性与完备性（§1.9）、证明的有限性（§1.8）。它也是把命题逻辑的经验抬升到一阶逻辑的经验——第二章的完备性与紧致性，走的仍是这条「有限片段撑起整体」的路。

第一章 命题逻辑：真值表与推理的骨架1.11 布尔代数：把逻辑变成代数

★★★ 前九节把真假当作真值表来算，本节换一副眼镜：把 ∧, ∨, ¬ 看成三种「运算」，把等价律看成「运算律」。于是命题逻辑忽然成了代数的一个分支，可以像解方程那样去变形。

把 §1.3 的等价律表与上面的公理逐条对照，会发现它们一一对应：逻辑里的 ≡ 正是代数里的 =，逻辑里的重言式正是代数里恒成立的等式。于是「化简公式」与「化简代数式」变成同一门手艺。¬ 是求补，0 / 1 是下界与上界。

布尔代数还能装上「序」。定义 a ≤ b 当且仅当 a ∧ b = a（直觉：a 不比 b 强）。可验证这是一个偏序，且任两元有最小上界（a ∨ b）与最大下界（a ∧ b），故布尔代数首先是一个格。在幂集代数里，这个序就是 ⊆；在公式代数里，它就是「a → b 是重言式」。

Stone（1936）给出的证明路线极具启发：把布尔代数的「超滤子」（对 ∧, ∨ 封闭、不含 0 且对每个 a 恰含 a 或 ¬a 的最大家庭）全体记为 S(B)，配以适当拓扑成为布尔空间；再证明 B 同构于 S(B) 上闭开集的代数。超滤子扮演的角色，就是「完备性证明里的那个赋值 v」——把每个命题送向真或假。§1.9 的极大一致集，在代数语言里正是林登鲍姆–塔斯基代数的一个超滤子。于是完备性定理获得了第二种证法：存在足够的超滤子来区分一切元素（布尔素理想定理）。

本节的收获可以概括为三步并作一步：等价律是公理、公式类是元素、赋值是超滤子。同一件事被三种语言描述，各有各的方便——这正是二十世纪数学「结构主义」的典型面貌。下一节回到最具体的层面：既然一切都能算，那么命题逻辑的判定，究竟要付多少代价？

第一章 命题逻辑：真值表与推理的骨架1.12 判定问题：命题逻辑为何可判定

★★★ 到目前为止，「是否重言式」「是否可满足」都是靠人算出来的。本节问一个更硬的问题：有没有一种机械程序，对任意输入公式都能在有限步内给出「是/否」？命题逻辑的答案是肯定的，而这道肯定恰好是一整片否定结果的对照物。

算法。输入含 n 个变元的公式 φ。枚举全部 2ⁿ 个指派（每一指派可看作一个 n 位二进数 0, 1, …, 2ⁿ − 1），对每个指派按语法树自底向上求值；若某指派使 φ 取 1，输出「可满足」，否则输出「不可满足」。停机性来自枚举有限：循环次数恰为 2ⁿ，必停。正确性来自真值表的定义 1.2：逐行覆盖了一切可能，无遗漏。

这条定理的分量，在它的对照物面前才显出来。谓词逻辑（一阶逻辑）没有这样的程序——是否存在一个算法判定任意一阶公式是否有效，这就是希尔伯特 1928 年提出的判定问题（Entscheidungsproblem）。Church 与 Turing 在 1936 年各自独立给出否定回答：一阶逻辑不可判定。命题逻辑与一阶逻辑之间隔着的，正是量词 ∀ ∃（第二章登场）——量词把「有限的穷举」升级成「无穷的搜索」，判定性就此失守。这条分界线是全书最重要的一条分界线之一。

不过「可判定」只保证存在一个总会停机的程序，并不保证它快。真值表算法的时间是 O(2ⁿ)：n = 10 要一千次求值，尚可；n = 30 要十亿次，吃紧；n = 100 则连宇宙寿命都不够。指数增长意味着原则上可判定、实践上不可行——这条裂缝，下一节将把它生产成整片计算复杂性理论。

把本节的措辞收紧一点：「可判定」是关于存在性的断言，「复杂度」是关于资源量的断言。两者分属两个年代——前者是 1930 年代逻辑学的主要关切，后者是 1970 年代理论计算机科学的主要关切。命题逻辑同时落在两个战场的正中央：它既可判定（逻辑的好消息），又藏着一个 NP 完全问题（计算的最难谜题之一）。下一节正面迎战后者。

第一章 命题逻辑：真值表与推理的骨架1.13 开关电路与逻辑门：逻辑的物理化身

★★ 逻辑能不能被造出来？能。1937 年， Shannon 在硕士论文《继电器与开关电路的符号分析》中证明：布尔代数与开关电路是同一个东西的两副面孔。这一篇论文，是数字时代的开工令。

于是任何命题公式都能被翻译成一张电路图，任何电路也都能被读成一个公式。公式的求值与电路的导通判定是同一件事：给每个开关定开合状态，看整条线路通不通——这正是一次真值指派下的公式求值。

把开关抽象成符号，就得到逻辑门：AND 门、OR 门、NOT 门，以及 §1.5 的主角 NAND 门与 NOR 门，还有常用的 XOR 门（异或，记 ⊕，恰是「相异为真」的排他或）。门电路的输入输出都是 0/1 电平，行为由真值表写死。两个门拼在一起做一个小任务，就得到可复用的组合元件——其中最有名的是加法器的半成品：

这里出现了本章与工程世界最要紧的一段对话。§1.5 证明了 NAND 单独完备，工程上又发现 NAND 门的晶体管实现最省——两者一配合，结论就是：整台计算机的逻辑，可以完全用 NAND 门搭出来。从真值表到 NAND 完备性再到芯片版图，一条直线走通。逻辑不是对推理的比喻，而是芯片上电流的真实走向。

本节还留了一个技术疑点给电路设计者：一个组合电路的「输出是否正确」，本质上是一次公式求值，可以逐位核对；但要让电路「更省、更快」，就要找同样功能里最短的表达式——这是布尔函数最小化问题，与下一节的复杂度话题同宗。

第一章 命题逻辑：真值表与推理的骨架1.14 SAT 与复杂性：第一个 NP 完全问题

★★★★ 上一节证明了命题逻辑可判定，也指出了代价的指数墙壁。本节把这个问题正式命名、正式量化，并迎来逻辑学对计算理论的最大一次馈赠——SAT 是第一个 NP 完全问题。

SAT 之所以自然，是因为 §1.4 已把「任意公式」标准化成 CNF，所以「任意公式是否可满足」都能翻译成一个 SAT 实例。而判定一个公式是否重言式，等价于判定其否定是否不可满足，故重言式问题与 SAT 同难。

归约思路（要点）。设 L 是任一 NP 语言，由多项式时间验证器 V 刻画：x ∈ L 当且仅当存在见证 y（长度多项式有界）使 V(x, y) 停机接受。把 V 在输入 (x, y) 上的整段计算历史摊成一张二维表格：行是时刻 0, 1, …, T，列是纸带格。引入命题变元，刻画三条事实：①每一时刻机器恰处于一个状态；②每一时刻读写头恰在一个位置；③每一时刻每个带格恰含一个符号；再用子句强制相邻两行遵守转移函数（本次与下次格局合法）、首行编码初始格局（x 固定、y 用待填变元）、末行含接受状态。所得 CNF 的规模是 T 的多项式，而 φ_x 可满足 ⟺ 存在见证 y 使 V 接受 ⟺ x ∈ L。这就是把「存在一条接受计算路径」翻译成「存在一个满足指派」的全部内容。

Cook 与 Levin 的结果意义深远：它给 NP 里所有问题立了同一把标尺。此后一旦证明某个新问题能多项式归约自 SAT，它就立刻晋升 NP 完全——今天已知的 NP 完全问题已逾四千个，覆盖排课、装箱、旅行商、蛋白质折叠、电路布线。它们如同被同一根锁链拴住：只要其中任何一个有多项式算法，则全部都有，P = NP 成立；反之若认定 P ≠ NP，则它们全体都无法被高效求解。P 是否等于 NP，是克雷数学研究所七大千禧年问题之首，悬赏百万美元，至今未决。

本章到此完成了从真值表到复杂性的整条链：真假 → 联结词 → 真值表 → 范式 → 可判定性 → 复杂度。逻辑最初是一套讲「怎样算推得对」的规矩，走到这里，它已经把「机器能不能高效判定」这一整个领域纳入了自己的疆域。下一节回到起点，用最省的符号把这条链的骨架重搭一遍——卢卡西维茨的三条公理。

第一章 命题逻辑：真值表与推理的骨架1.15 公理化的命题逻辑：卢卡西维茨三公理

★★★★ 本章一路用了自然演绎与推理规则，却始终没有把「公理」正式列出。本节补上最经典的一套：卢卡西维茨三公理系统。它只用两个联结词、三条公理、一条规则，就撑起了整个命题逻辑——极简到几乎苛刻。

唯一的推理规则是肯定前件 MP：由 φ 与 φ → ψ 得 ψ。其余联结词按习惯缩写：φ ∨ ψ := ¬φ → ψ，φ ∧ ψ := ¬(φ → ¬ψ)，φ ↔ ψ := (φ → ψ) ∧ (ψ → φ)。「代入例式」的含义是：把公理中的 φ, ψ, χ 换成任意公式，得到的新公式仍算公理——这一条使公理从三条膨胀成无穷多条，却也使证明的机械检查依旧可行。

这三条为什么是这三条？A1 说的是「一个真命题被任何命题蕴含」；A2 说的是「蕴含可以沿括号分配」，它是 MP 在证明内部运作所需的燃料；A3 说的是「逆否等价」，它把否定与蕴含焊接起来，是反证与经典逻辑的支柱。三条合起来恰好完备——这是上一节完备性定理的一个实例：这套系统能证出全部重言式。

证明。下列五公式构成一个证明序列，每行的身份都注明在括号内。

末行即所求，证毕。∎

这段证明只有五行，却是本章「证明即符号序列」这一观念的极致标本：没有一步依赖「p → p 看起来显然」的直觉，每一步都能被机器按「是公理 / 由前两行 MP」逐字核对。任何一位，只要愿意，都能拿一张纸逐行验收它。亲手对一遍——这是全章唯一一次把「形式证明」四个字落到实处的机会。

有了 ⊢ p → p 与 A1、A2，配上演绎定理（§1.7，其在系统 L 内的证明恰好用到 A1、A2），就能派生出自然演绎里的一切规则。那条为了显示严苛而牺牲可读性的公理路线，就这样与直觉友好的自然演绎路线在同一片天空下汇合。

第一章 命题逻辑：真值表与推理的骨架例题课（一）：语义与真值表的实操

解。两变元，四行。逐行算：(p,q) = (0,0) 时 ¬p → q 为 1 → 0 = 0、p → q 为 0 → 0 = 1，析取得 1；(0,1) 时两分支皆 1，得 1；(1,0) 时第一支 0 → 0 = 1，得 1；(1,1) 时两支皆 1，得 1。末列全 1。

答。四行皆真，故为重言式。∎

解。用等价律变形，不必列八行表。对左式两次用蕴含改写 α → β ≡ ¬α ∨ β：p → (q → r) ≡ ¬p ∨ (¬q ∨ r) ≡ ¬p ∨ ¬q ∨ r。对右式先用德摩根：(p ∧ q) → r ≡ ¬(p ∧ q) ∨ r ≡ (¬p ∨ ¬q) ∨ r ≡ ¬p ∨ ¬q ∨ r。两式化到同一个析取式。

答。等价。这条等价律在数学写作里叫括号合并（「多前提的蕴含可打包成合取前件」），是化简证明的常备招式。∎

解。真值表四行：(0,0),(0,1),(1,1) 三行取 1，(1,0) 一行取 0。主析取范式取三行极小项之析取：

(¬p ∧ ¬q) ∨ (¬p ∧ q) ∨ (p ∧ q).

主合取范式取取 0 行的极大项：该行 (p,q) = (1,0)，取 0 的变元 q 写自身、取 1 的 p 写否定，得 (¬p ∨ q)。

答。主析取范式如上，主合取范式为 (¬p ∨ q)。这条合取子句正是 §1.3 的蕴含改写——范式法竟「自动」发现了等价律：极小项与极大项这两套标准写法，把等价关系完全暴露在纸面上。∎

解。由 §1.5，¬q ≡ q ↑ q，且 p → q ≡ ¬(p ∧ ¬q) ≡ p ↑ (¬q)。代入得 p → q ≡ p ↑ (q ↑ q)。验证：q ↑ q = ¬q，故 p ↑ (q ↑ q) = ¬(p ∧ ¬q) = ¬p ∨ q = p → q。四行代入 (0,0),(0,1),(1,0),(1,1)，依次得 1,1,0,1，与蕴含表逐行吻合。

答。p → q ≡ p ↑ (q ↑ q)。整式的每个联结词都换成了 NAND，若画成电路，只需两个与非门。∎

复盘。例 1.38 用真值表、例 1.39 用等价律、例 1.40 用范式、例 1.41 用完备性——本章语义部分的四大件各出一手。做题顺序的纪律是：先估规模（两三个变元就查表，多了就化式），再选工具，能不动真值表就不动。

第一章 命题逻辑：真值表与推理的骨架例题课（二）：证明与推演的实操

解。把三段前提依次摆出，再用 MP 两次。

证明序列。① p（前提）；② p → q（前提）；③ q（由 ①、② 经 MP）；④ q → r（前提）；⑤ r（由 ③、④ 经 MP）。末项即结论。∎

这正是假言三段论 HS 的「展开版」：p → q 与 q → r 合成 p → r，再与 p 一碰，得 r。把两步写开而不直接引用 HS，是为了示范「每一步都是原始规则」。

解。由演绎定理，只需证 {p ∧ q} ⊢ p。这是一个单步推导：由合取消去（化简规则）∧E，从 p ∧ q 直接得 p。于是 {p ∧ q} ⊢ p，演绎定理回代，得 ⊢ (p ∧ q) → p。

答。证毕。这里体现了演绎定理的省力之处：把「证一个蕴含」换成「假定前件、推出后件」，往往一步到位。∎

解。自然演绎的证法是把假设盒与否定引入拼起来。

答。证毕。这条证明展示了否定引入 ¬I 的标准用法，也解释了反证法为何合法：「假定某式推出矛盾」本身就是「该式的否定成立」的证明。∎

解。用演绎定理把目标拆成两层。目标形如 ⊢ A → (B → C)，故只需证 {q → r} ⊢ (p → q) → (p → r)；再用一次演绎定理，只需证 {q → r, p → q, p} ⊢ r。后者的证明序列：

答。由演绎定理回代两次，即得所求蕴含式。注意整条链只用了 MP 与演绎定理，而演绎定理在系统 L 内的证明（§1.7）只用到 A1、A2——于是这条「三段论变形」被彻底还原成三条公理与一条规则。∎

复盘。证明题的通用策略是从结论往回看：结论是蕴含就上演绎定理，结论是否定就上否定引入，结论是合取就分开证两半。本题的四道例各自穿过一条通路，做题时应先认路再动笔。

第一章 命题逻辑：真值表与推理的骨架习题课（一）：联结词与语义

习题 1-1（判类型）。用真值表判断下列公式属于重言式、矛盾式还是可满足式（非重言亦非矛盾）：① (p → q) ↔ (¬p ∨ q)；② p ∧ ¬p；③ (p ∧ q) → p；④ p ∨ q。

提示。① 把 → 改写成 ¬p ∨ q，左右两式恒同，故为重言式；② 第二、四行分别为 (1,0)、(0,1) 时取 0，全表无 1，为矛盾式；③ 化简规则的公式版，重言式；④ 只在 (1,1)、(1,0)、(0,1) 为 1，非重非矛，是可满足式。

习题 1-2（判等价）。判断下列各组公式是否逻辑等价：① p → (q ∨ r) 与 (p → q) ∨ (p → r)；② ¬(p ↔ q) 与 p ⊕ q（异或）。

提示。① 左式 ≡ ¬p ∨ q ∨ r；右式 ≡ (¬p ∨ q) ∨ (¬p ∨ r) ≡ ¬p ∨ q ∨ r——等价。② 写出定义：p ⊕ q := (p ∨ q) ∧ ¬(p ∧ q)，四行核对与 ¬(p ↔ q) 逐行相同——等价。这道题说明「异或」就是「等值的否定」，也解释了 §1.13 半加器为何用 XOR。

习题 1-3（求范式）。求 φ = (p ∨ q) ∧ ¬r 的主析取范式与主合取范式。

提示。三变元。φ 取 1 的行是「r = 0 且 p ∨ q 为真」，即 (0,1,0),(1,0,0),(1,1,0) 三行；极小项相析取得主析取范式。取 0 的五行使极大项，可先写出简化 CNF (p ∨ q) ∧ ¬r，再把每个子句补齐缺失变元：p ∨ q ≡ (p ∨ q ∨ r) ∧ (p ∨ q ∨ ¬r)，¬r ≡ (p ∨ ¬r) ∧ (¬p ∨ ¬r) 后再补。

习题 1-4（NAND/NOR 化）。只用 ↑ 表示 p ↔ q；只用 ↓ 表示 p ∨ q。

提示。用 §1.5 的三块积木：¬a ≡ a ↑ a、a ∧ b ≡ (a ↑ b) ↑ (a ↑ b)、a ∨ b ≡ (a ↑ a) ↑ (b ↑ b)。先把 p ↔ q 化为只用 {¬, ∧, ∨} 的式子再逐处替换。NOR 侧：a ∨ b ≡ (a ↓ b) ↓ (a ↓ b)，两个或非门即可。

习题 1-5（完备性的边界）。证明：仅用 ∧ 与 ∨ 两种联结词不能表达 ¬p，故 {∧, ∨} 不完备。

提示。关键观察：若公式 φ 只由 ∧, ∨ 与变元构成，则它是单调的——把所有变元从 0 改成 1，φ 的值绝不下降。用对构造的归纳证明：变元情形显然；φ ∧ ψ 与 φ ∨ ψ 的单调性由归纳假设直接得到。于是把全部变元取 0，任何这样的 φ 都取 0；而 ¬p 在 p = 0 时取 1——矛盾，故不可表达。本习题的要点是「不完备性」也需证明，用的是单调性这条结构性质。

第一章 命题逻辑：真值表与推理的骨架习题课（二）：证明、公理与边界

习题 1-6（形式证明）。给出 {p → q, q → r, r → s, p} ⊢ s 的形式证明，并指出哪一步用了 HS。

提示。序列：① p；② p → q；③ q（MP ① ②）；④ q → r；⑤ r（MP ③ ④）；⑥ r → s；⑦ s（MP ⑤ ⑥）。若把 ②④⑤ 写成 HS 一步，则「合成链」处用了 HS；两种写法都对，区别只在是否显式引用导出规则。

习题 1-7（演绎定理）。用演绎定理证明 ⊢ (p → (q → r)) → (q → (p → r))（前件交换律）。

提示。两次演绎定理把目标化为 {p → (q → r), q, p} ⊢ r。证明：① p；② p → (q → r)；③ q → r（MP ①②）；④ q；⑤ r（MP ③④）。回代两次即得。要点：演绎定理允许自由引入与释放假设，但释放的顺序必须与引入相反。

习题 1-8（自然演绎）。证明 ⊢ (p ∨ q) → (q ∨ p)。

提示。由 →I，只需证 {p ∨ q} ⊢ q ∨ p。对 p ∨ q 用 ∨E：分两种情形。情形一（假设 p）：由 ∨I 得 q ∨ p；情形二（假设 q）：由 ∨I 得 p ∨ q……注意方向，应得 q ∨ p。两情形同得 q ∨ p，故 ∨E 给出结论。核心是 ∨E 的「两情形都得同一结论」纪律：分支里可以各取所需，但出口必须一致。

习题 1-9（公理与导出规则）。在系统 L 中，说明假言三段论 HS 并非必需的原始规则，并给出它的导出思路。

提示。先用 A2 的例式 (q → r) → ((p → q) → (p → r))（见例题 1.45 的完整还原）。给定 p → q 与 q → r 作假设：① 由 A1 得 (q → r) → (p → (q → r))；② 用例题 1.45 的式子两次 MP 得 (q → r) → ((p → q) → (p → r))；③ 与 q → r 作 MP，再与 p → q 作 MP，得 p → r。要点：一切导出规则都能被还原到 A1、A2、A3 与 MP。

习题 1-10（边界讨论）。已知命题逻辑可判定，一阶逻辑不可判定。解释：为什么 SAT 属于 NP，而「判定任意一阶公式是否有效」不属于 NP？

提示。关键是见证的长度。SAT 属于 NP，因为一个候选指派就是多项式长度的见证，验证只需逐子句核对——「是」答案有多项式可验证的凭证。「一阶有效性」说的是「在所有结构中都为真」，量词允许搜索无穷多的结构，任何有限凭证都无法覆盖全体的检验；更根本地，一阶逻辑的有效性问题（Church–Turing 1936）根本不可判定，而 NP 中的问题都至少是可判定的（做一个穷举总会停）。故一阶有效性连 NP 都进不去。本习题的落点：可判定性（会不会停）与复杂度（多快能判）是两个层次的问题，量词把第一个层次都击穿了。

第一章 命题逻辑：真值表与推理的骨架本章地图：概念依赖与推理线路

本章十五节不是平行地摊开的，而是一棵树。箭头 A → B 读作「B 的定义或证明用到 A」。读图时特别盯住居中的那个金色节点——它是全章两条主干的合流处。

通向外部的接口。① 完备性与紧致性 → 第二章一阶逻辑的对应定理（同一套路，量词添乱）；② 正规形式与真值表 → 第三章证明论的切割消除（范式化的语法版本）；③ 可判定性与 SAT → 第四章可计算性与复杂性（判定性问题在此升级为「不可判定」）；④ 形式证明的「可机械检查」→ 第六章证明助手（Lean、Coq 逐行验收）。章内概念树是自足的——读完本章，后五章每一步都能在此找到根系。

第一章 命题逻辑：真值表与推理的骨架本章小结（上）：语义篇

本页任务。把 §1.1–1.5 的语义装备压缩成几张随身卡片；语法与元定理的卡片在下页。

一个必背实例。常驻公式 ((p → q) ∧ (q → r)) → (p → r)：八行真值表末列全 1，是重言式；它是假言三段论 HS 的公式版，也是本章语义部分的第一个标本。

三个一分钟快检。① 判类型：末列全 1 / 全 0 / 其余；② 判等价：把两式都化成主析取范式比指标集合，或就地用等价律化简；③ 判完备：试着用给定的联结词造出 ¬ 与 ∧，造得出则（多半）完备，造不出要找结构性理由（如单调性）。

下一步。语义篇回答「式子何时为真」，语法篇回答「式子怎样被证」。两篇的最后会证明它们同步——翻页。

第一章 命题逻辑：真值表与推理的骨架本章小结（下）：语法篇

本页任务。把 §1.6–1.15 的语法与元定理装备收进卡片，并以方法论的封印收束全章。

方法论的封印。本章全部推理只动四样东西：查表（真值表穷举）、化式（等价律变形）、写序列（形式证明）、造赋值（极大一致集／超滤子）。调用成本依次升高，实战顺序恒定：能查表就查表，查不动就化式，证明题先摆前提，元定理才赋值。这套「成本阶梯」是逻辑工作的纪律。

下一站。把命题变元换成带量词的公式，会发生什么？需要新的公理吗？完备性还成立吗？判定性还守得住吗？——这三个问题就是第二章的全部议程。

第一章 命题逻辑：真值表与推理的骨架思想卡：把「如果」当成算子

第一章 命题逻辑：真值表与推理的骨架挑战：为一种几何设计一阶公理

任务。本章的联结词只能谈「真假」，不能谈「所有」「存在」。下一章将加入量词 ∀ ∃，届时就能把整门几何写成公理。本挑战提前预演：为一种最朴素的几何——只有点与直线，只有「点在直线上」一种关系——设计一套一阶公理，并检查它的模型。

语言。取一元谓词 P(x)（x 是点）、L(z)（z 是线），二元谓词 I(x, z)（点 x 在线 z 上）；等号 = 可用。函数符号一概不用——几何的朴素关系不必借助作图工具。

分步引导。① 先把参考公理组抄成公式，逐条说明它排除了哪些「退化模型」（例如「所有点都不在线上」的空模型）；② 求它的最小模型：直觉上应是「三点不共线、三条线两两相交」的三角形，公式验证三角形满足全部公理；③ 若再加一条射影公理「任意两条不同直线恰交于一点」，模型的形状会怎样变化？有限模型还够用吗？（提示：射影平面 PG(2,2) 恰有 7 点 7 线，正是本文 §1.9 与第二章将重逢的对象。）

进阶（选做）。把这套公理组看成一个理论 T。① 用紧致性（§1.10）的思想讨论：若 T 的每个有限子集都有模型，T 是否有模型？② 查阅资料了解 Tarski 的初等欧氏几何（1948）是全称可判定的：为什么「只有关联关系的几何」比「含实数算术的几何」更容易判定，并把这条直觉记下，第五章与第六章会回来兑现。

第一章 命题逻辑：真值表与推理的骨架实验：形式系统的程序化对拍

实验目的。§1.9 证明了「⊢ φ 与 ⊨ φ 同步」。这句话在纸上是一条定理，在机器上则是一次可以逐条打印的对拍。本实验把两条主干各写成一短段程序：语义侧用真值表枚举判重言式，语法侧把「公式恒真」翻译成「它的否定的合取范式被归结反驳掉」，然后让二者在同一批公式上逐条比对。若完备性定理为真，则两侧的判定必须字字相同。

def to_cnf_clauses(f):
    """¬f 的 CNF 子句集：对每个使 f 为真的赋值，取被它证伪的极大项。"""
    vs = sorted(atoms(f))
    out = []
    for bits in itertools.product([0, 1], repeat=len(vs)):
        if eval_f(f, dict(zip(vs, bits))) == 1:
            out.append([(v, bits[i]) for i, v in enumerate(vs)])
    return out

def resolve(c1, c2):
    """找一对互补文字消去；无互补对返回 None。"""
    for lit in c1:
        comp = (lit[0], 1 - lit[1])
        if comp in c2:
            return [l for l in c1 if l != lit] + [l for l in c2 if l != comp]
    return None

def refute(clauses):
    """归结闭包：导出空子句即反驳成功（¬f 不可满足）。"""
    S = [c for c in clauses if not is_taut_clause(c)]
    if not S:
        return False
    changed = True
    while changed:
        changed = False
        for i in range(len(S)):
            for j in range(i + 1, len(S)):
                r = resolve(S[i], S[j])
                if r is None:
                    continue
                if len(r) == 0:
                    return True
                if r not in S:
                    S.append(r); changed = True
    return False

报告要求。① 给出自选五条公式的两侧判定，注明是否一致；② 说明为什么「使 φ 为真的赋值」生成的是 ¬φ 的子句，而不是 φ 的子句；③ 把第四步的随机测试扩到四条变元，观察归结闭包的规模增长速度，并解释它与真值表 2ⁿ 的增长为什么不同。本实验的完整脚本见本章配套的 exp_c1.py。

第一章 命题逻辑：真值表与推理的骨架〖札记〗中西推理传统的对照

亚里士多德在《前分析篇》里把三段论拆成格与式，配上换位规则，做成了人类第一套可检查的推理清单。几乎同一时期，东方的名辩之学也在处理「推」这件事，只是走了一条不同的路。《墨经》里的《经上》《经下》《大取》《小取》四篇，留下了一批关于「辩」的条目：有对「故」（理由）与「类」（类推的根据）的讨论，有「以类取，以类予」的推论原则，也有对「悖」的自指警告。战国之世，惠施讲「历物之意」，公孙龙以「白马非马」「坚白离」立说，惠施、公孙龙这一路把概念辨析推到了极限——可惜这些讨论多以具体命题的胜负收场，少有把「推理形式本身」抽出来列为公理的自觉。

古印度的因明学提供了一条更接近形式化的旁证。陈那（约五至六世纪）把旧因明的五段论简化为「三支作法」：宗（待证命题）、因（理由）、喻（同喻与异喻的例证）。《因明入正理论》与《集量论》里对「因三相」的规定，实际上已经在追问「什么样的理由才算有效」，与亚里士多德对中间项的要求遥相呼应。不过因明服务于论辩胜负，讨论大量围绕过失与成立展开，也未能长成一部纯粹的推理演算。

近代的转折靠翻译与重写完成。严复译出《穆勒名学》（1905）与《名学浅说》（1909），第一次把「逻辑」这个学科名搬进汉语；章士钊、金岳霖随后把这个学科带进课堂与自己的体系——金岳霖 1937 年出版《逻辑》，把演绎系统的观念正式引进；沈有鼎 1980 年出版《墨经的逻辑学》，用现代逻辑的眼光回头清点《墨经》里的推理材料。至此两千年悬置的问题有了新的问法：说一种传统「没有形式逻辑」，究竟是说它没有推理，还是说它没有把推理和对象分离？

把这三条线放在一起看，本册后面的路就更好理解了：形式化不是唯一处理「推」的方式，却是一种能让机器接手的处理方式。第三章的相继式演算、第四章的图灵机、第六章的证明助手，都是把「推」的规则从人手里取出来、交给符号去执行的结果；而本页的三条传统提示，这条路上还有别的走法与别的问法。

第一章 命题逻辑：真值表与推理的骨架本章速查表：符号、公理与定理卡

本页把第一章的全部装备压成一张表：左边是要查的条目，中间是内容，右边标注它第一次出现的位置。复习时先盖住中间一列自查，答不出再回读对应小节。

三句自测。① 拿到一个公式，能在三十秒内用真值表定其类型吗？② 能说出「完备性」与「可判定性」的区别吗（一个是语义与语法的重叠，一个是存在判定程序）？③ 能讲清为什么 {∧, ∨} 造不出否定吗（提示：单调性）？三句都能答，本章的骨架就算立住了。

第二章 一阶逻辑：量词、结构与完备性第二章导引：从「真」到「对一切」

第一章把「如果……那么」炼成了真值表，于是「这句话在什么情况下为真」可以被穷举。可真值表有一块够不着的天窗：它看不见句子内部。「所有素数都大于 1」与「2 是素数」在命题逻辑眼里只是两个互不相干的代号 p 与 q，而「所以 2 大于 1」这一滑步，真值表永远算不出来——因为「所有」「存在」「大于」这些词根本没有对应的格子。

本章要补上这块天窗，造一门能谈「对象」的语言。办法是加三样东西：名字（常量符号，让语言指称具体对象）、构造（函数符号，让语言拼出新对象）、关系与量词（关系符号判断对象之间的性质，∀ 与 ∃ 说出「对每一个」与「存在一个」）。三样装齐，就得到二十世纪最有用的形式语言——一阶逻辑。它的影响遍及数学基础、程序验证与人工智能，本册余下各章都站在它的地基上。

本章的路线是一道「先语义、后语法、再合流」的台阶，每一级都踩在前一级上：

第一阶（§2.1–2.5）——语义先行。从符号表出发，递归地定义「项」与「公式」，分清哪些变元被量词管住（约束）、哪些还露在外面（自由）；再由结构 𝒜 = (A; …) 与解释给出满足关系 ⊨ 的递归条款。这一阶的全部工作，是把塔斯基 1933 年那句「φ 为真当且仅当……」写成一串可以逐条核对的规则。

第二阶（§2.6–2.9）——语法登场，完成会师。列出一套希尔伯特式公理与两条推理规则，定义「可证」⊢；随后证明本章的顶点——哥德尔完备性定理（1929）：凡在所有结构中为真的，都能被形式推出。语义与语法这两条平行线，第一次在一阶逻辑里握上了手。它的直接推论是紧致性定理，一台造模型的机器。

第三阶（§2.10–2.16）——装备与实例。处理相等号与商模型，学会把公式拧成前束范式、看清 ∃∀ 与 ∀∃ 谁更强；再把「公理系统」当作研究对象，清点一致性、独立性、完备性、范畴性、可判定性五个元数学概念。最后参观三套真实系统：希尔伯特几何、一阶算术 PA、塔斯基初等欧氏几何，并把群、环、域这些代数公理拿来对照。

第四阶（§2.17 与章末）——算账与动手。清点形式化的代价与收获，做例题、习题、实验，把本章的概念接成一张网。

随身行李只需三件：第一章的真值表、一点集合语言、写递推定义的耐心。行李齐备时直接迈上第一级台阶。出发前先认识本章的常驻嘉宾。

常驻嘉宾：自然数结构 𝒩 = (ℕ; 0, S, +, ·, <)。它是本章出镜率最高的结构——语言最小、性质最深。§2.3 用它演示解释，§2.4 用它算真值，§2.9 用它长出非标准模型，§2.14 把它公理化成一阶算术 PA。它小到可以手算，又深到能承载哥德尔的不完备定理，是全书反复回来的坐标原点。

第二章 一阶逻辑：量词、结构与完备性2.1 一阶语言：符号表与项

★★ 造语言的规矩只有一条：先把词汇表定死，再谈句子。一阶语言的词汇表分两栏——任何语言都带的逻辑符号，与这门语言自选的非逻辑符号。

三样非逻辑符号各司其职。常量符号是「专名」，一个符号钉住论域里的某个对象；函数符号是「构造器」，吃进若干对象、吐出一个对象；关系符号是「判词」，吃进若干对象、给出一句可判真假的话。三者在句法上分工，恰好在语义上对应论域里的三类东西（§2.3 把这份对照列成表）。

五门常用语言。记住它们的符号表，本章反复出场。① 算术语言：常元 0，一元函数 S（后继），二元函数 + 与 ·，二元关系 <。② 群语言：二元函数 ·，常元 e，一元函数求逆。③ 序语言：只含二元关系 <。④ 集合论语言：只含二元关系 ∈。⑤ 图语言：只含二元关系 E。语言越瘦，能说的越少——这正是下一节要小心的。

项是「名字」，不是「话」。S(S(0)) 是一个项，它在标准算术结构里指称 2；x + S(0) 也是一个项，指称「比 x 多 1 的那个数」——但「多 1」相对于 x 取什么值而言，要等赋值出场（§2.4）才说得清。项只说「哪个对象」，从不说「真或假」；真假的活儿交给公式（§2.2）。

唯一可读性。项由括号分层，任一符号串至多有一种剖析方式：任何项只有一个语法树。这条「唯一可读性」保证了后面「归纳地定义项的值」不会撞车——凡是递归定义，前提都是每一步的构件唯一。下一节把项装配成公式，并引入本章第一对主角概念：自由变元与约束变元。

第二章 一阶逻辑：量词、结构与完备性2.2 公式与自由变元

★★ 有了名字，就能开口说话。最朴素的一句是「这几个对象满足某关系」，再往上用联结词与量词层层搭积木。本节把「公式」的递归定义写死，并分清哪些变元被量词管住、哪些还露在外面。

自由与约束。量词是「管辖」符号：一旦写下 ∀x，紧随其后的那段公式里 x 的每次出现都被它管住。递归地判定一个变元出现是约束还是自由：① 在 ∀x φ 与 ∃x φ 中，x 的一切出现都约束；② 在原子公式中，一切变元出现都自由；③ 联结词不改变出现方式——¬φ 与 (φ □ ψ) 中，出现保持原样。

四个例子（盯住管辖范围）。① ∀x(x < x + S(0)) 是句子。② x < S(0) 中 x 自由，不是句子。③ ∀x(P(x) → R(x, y)) 中 x 被 ∀ 约束、y 自由——管辖范围在 → 之后依然有效。④ (P(x) ∧ ∃x Q(x))：第一个 x 自由，第二个被 ∃ 约束——同名变元各归其主，它可以在同一公式里「半自由半约束」。

代入与捕获（预告）。把公式 φ(x) 中的 x 换成项 t 记作 φ(t)。若 t 中含变元 y，而 φ 里恰好有管辖 y 的量词，代入后 y 会被「顺手抓走」——这叫变元捕获。安全的代入要求 t 对 x 是可代的，§2.6 的量词公理要靠它，§2.10 与 §2.11 会两次回访这个坑。

下一节把公式放进「结构」里，让这些符号第一次获得意义。

第二章 一阶逻辑：量词、结构与完备性2.3 结构：论域、函数与关系

★★ 句法只管符号怎么排，语义要回答符号指什么。这一步由「结构」完成：它给符号表上的每个非逻辑符号指派一个具体的数学对象。

注意两件事。第一，论域非空——否则 ∀ 的条款会变得别扭（§2.4）。第二，关系符号被解释成「有序 n 元组」的集合，因此 R(a, b) 真当且仅当有序对 (a, b) ∈ R^𝒜。这是把「是非句」翻译成「属于集」的关键一步，也是塔斯基语义的全部秘密所在。

三个标本。① 标准算术结构 𝒩 = (ℕ; 0, S, +, ·, <)：论域是自然数集，S 是后继，+、· 是通常运算，< 是通常顺序。② 实数域 ℛ = (ℝ; 0, 1, +, ·, <)：同样一串符号，落到实数上长出完全不同的性质——§2.12 会看到这套公理是「完备、可判定」的。③ 图结构 𝒢 = (V; E)：论域是顶点集，E^𝒢 是边的有序对集合。

怎样比较两个结构。若两个 L-结构之间有一个双射 h，保常量、保函数、保关系（(a₁, …, a_n) ∈ R^𝒜 当且仅当 (h(a₁), …, h(a_n)) ∈ R^ℬ），则称它们同构，记 𝒜 ≅ ℬ。同构的结构在所有一阶句子面前「同生共死」——这是 §2.12 讨论范畴性时的标尺。

赋值。结构解释了符号，还没管变量。给每个变量指派一个论域中的对象，得到赋值 s : {x₁, x₂, …} → A。有了结构与赋值，一个项才算「指定了」某个对象。下一节就把结构、赋值与公式三者拼在一起，写下满足关系的递归条款。

第二章 一阶逻辑：量词、结构与完备性2.4 满足关系：语义的递归定义

★★★ 万事俱备：语言给符号，结构给意义，赋值给变元。本节写下本章最核心的一段机器——塔斯基 1933 年的满足关系 ⊨，它把「φ 在 𝒜 中于赋值 s 下为真」定义成一个纯递归、可逐条执行的程序。

其中 s(x ↦ a) 表示把 x 的值改成 a、其余不变的新赋值。这段定义值得逐行咀嚼：(S1) 把「为真」还原成「有序组属于某集合」，语义问题由此变成集合论问题；(S5)(S6) 是全章的枢纽——∀ 要求对整个论域逐一兑现，∃ 只要求找到一处见证。塔斯基的关键洞察是：量词不是模糊的「所有」，而是「对论域的每个元素做一次检查」这一可执行的指令。真值因此有了不依赖人直觉、只依赖结构的机械判据。

句子的真值。句子没有自由变元，由命题 2.8，它的真假与赋值无关，于是可以直接写 𝒜 ⊨ φ，读作「𝒜 满足 φ」或「φ 在 𝒜 中为真」。这颗定心丸是全章的地基：从下一页起，本册谈论的「真」，都是句子在某个结构中的真。

，这台机器在有限论域上完全可执行：逐个元素检查 ∀ 与 ∃，真值必然算得出。可一旦论域无穷，「逐点检查」就成了一件需要无穷多步的事——第 §2.5 节开始，我们的兴趣就转向那些「一步到位、无需逐个检查」也仍然为真的公式。这一转向，正是从「算真值」走向「证明」的起点。

第二章 一阶逻辑：量词、结构与完备性2.5 有效式与逻辑后承

★★ 有了满足关系，就能给「真」分层：有的句子只在一个结构里真，有的在所有结构里真。后者是逻辑学的珍宝，本节的中心概念。

两个立刻的等式。① ⊨ φ 当且仅当 ∅ ⊨ φ——有效式是「无前提的后承」。② Γ ⊨ φ 当且仅当 Γ ∪ {¬φ} 不可满足——后承问题可以翻译成可满足性问题，后者是模型论的通用「证件」。这条翻译会在 §2.8、§2.9 反复出场。

为什么「有效」比「碰巧为真」珍贵。「2 是素数」在 𝒩 里真，换个结构就未必；而 ∀x(P(x) → P(x)) 在任何结构、任何解释下都真——它真得与符号的含义无关，只与符号的形状有关。有效式因此是可被纯符号规则认出的真，这条路直通下一节的「证明」。

与第一章的分水岭：命题逻辑的有效式可以靠真值表逐行穷举判定；一阶逻辑没有等价的真值表（论域可无穷）。它失去判定的捷径，却换来「表达一切数学结构」的能力——这笔交易是否值得，带着问题读下去。

第二章 一阶逻辑：量词、结构与完备性2.6 推理规则与希尔伯特系统

★★★ 语义说「什么为真」，语法说「什么推得出」。本节立下一套极简的推理装置：几条公理模式加两条规则。它的部件越少，后面的完备性证明就越干净。

可靠性的预告。这套装置有一条底线：凡公理都有效、两条规则都保有效性。公理 (A1)–(A3) 是命题重言式的模式，(Q1)(Q2) 在 §2.5 例 2.11 已验证有效；MP 保真、Gen 在任意赋值下保真。故结论：若 ⊢ φ 则 ⊨ φ（可靠性，§2.8 正式陈述）。语法难不倒语义——真正惊人的是反方向也成立，那是 §2.7 的正戏。

也许已经在抱怨：证明 φ → φ 竟然要五行，而它「显然」成立。这个抱怨——它正是 §2.17 讨论形式化代价的起点。眼下先忍住，去看这台笨机器如何造出一件惊人的成就。

第二章 一阶逻辑：量词、结构与完备性2.7 哥德尔完备性定理（完整证明）

★★★★ 全章顶点。它说：语义给的东西，语法全都够得着。凡在一切结构中为真的，都能被形式推出。证明的思想只有一句话——把一个一致集「喂」成自己的模型。

证明。本章只讨论可数语言（符号可数），不可数情形留待更专门的处理。全程只用「把 Γ 撑大」这一个动作。

第二章 一阶逻辑：量词、结构与完备性2.8 完备性的推论：一致即满足

★★★ 上一节的技术成果，一转身就变成一条极简的元定理：语法上不矛盾，语义上就住得下。一致与可满足，是一枚硬币的两面。

证明。（⇐ 可满足 ⟹ 一致）这就是可靠性：设 𝒜 ⊨ Γ。公理 (A1)–(A3)、(Q1)(Q2) 都在一切结构中为真（§2.5 例 2.11、§2.6），而 MP 与 Gen 把真句子送到真句子。由归纳，证明的每一行都在 𝒜 中为真，故 Γ ⊢ φ 蕴含 𝒜 ⊨ φ。特别地不可能从 Γ 证出矛盾（矛盾句无处为真），故 Γ 一致。（⇒）这正是定理 2.16。∎

证明。（⇒ 可靠性）由定理 2.17 前半证的同一归纳。（⇐ 完备性）设 Γ ⊨ φ。若 Γ ⊬ φ，则 Γ ∪ {¬φ} 一致，由定理 2.17 有模型 𝒜 ⊨ Γ ∪ {¬φ}，这与 Γ ⊨ φ 相矛盾。故 Γ ⊢ φ。∎

两句话记住这张图。可靠性说「⊢ 不越界」：能推的都是真的；完备性说「⊢ 不遗漏」：真的都能推。⊢ 与 ⊨ 之间的关系，不是包含，而是相等。这是命题逻辑第一章「语义＝语法」会师的升级版——这一次，语言能谈对象、能量化，会师依然成立。

特别分清两件常被混为一谈的事：本节的完备性是「语言对世界完备」（为真即可证）；第五章的不完备性是「理论对真理不完备」（存在既不可证也不可否证的句子）。前者是一个结构对一切理论成立的正面定理，后者是足够强的理论自身的局限——一正一反，正是本册最需要分清的对照。

第二章 一阶逻辑：量词、结构与完备性2.9 紧致性定理

★★★ 完备性定理有一件副产品，看似技术、实则威力无穷：只要每一小撮公理都能被满足，整堆公理就能被同时满足。局部可行，则整体可行——这条「紧致」，是造模型的第一利器。

证明。（⇒）若 𝒜 ⊨ Γ，则 𝒜 显然满足任一有限子集。（⇐）设每个有限子集都有模型，要证 Γ 可满足。反设 Γ 不可满足，由定理 2.17 它不一致，即 Γ ⊢ ⊥。任何证明只用到有限多条前提，故存在有限子集 Γ₀ ⊆ Γ 使 Γ₀ ⊢ ⊥，即 Γ₀ 不一致；又由定理 2.17，Γ₀ 不可满足——与「每个有限子集有模型」矛盾。故 Γ 有模型。∎

证明的关键只有一句：证明是有限的。矛盾若要出现，必由有限多条前提促成——这条「有限性」正是「紧致」二字的来源：无穷多条件被判为整体可行，只因它的每一小块都可行。

两个连锁推论。① 「有限性」不可一阶刻画：若一组句子只在有限结构里真，则由「每个有限子集有模型」将给出无穷模型，矛盾——故不存在一阶句子集恰好刻画「论域有限」。② 无穷论域不可被单个句子锁死大小：任何有任意大有限模型的理论，必有无穷模型。这条推论的普遍形状是：紧致性把「所有有限情形都成立」自动升级为「无穷情形也成立」，代价是模型里多出「非标准」的元素。

紧致性属于「语法定理造出的语义工具」，它对本册后文的重要性无论怎样强调都不过分：§2.12 用它证明公理独立，第五章用它讨论不可判定与独立性，第六章用它构造出人意料的模型。把「有限子集」与「整体」在脑中并置，随时准备用一次紧致性完成从局部到全局的跳跃。

第二章 一阶逻辑：量词、结构与完备性2.10 等词逻辑：相等号怎么处理

★★★ 数学里最常用的符号是 =。可「相等」在一阶语言里既不是常量、也不是函数或关系符号——它是逻辑符号，需要自己的公理。本节讲清相等号怎么被规则管住，以及它如何反过来帮我们造模型。

为什么替换性这么强。(E2) 说的不是「= 是个等价关系」，而是「= 在任何语境中都不可分辨」：对象一旦相等，就再也无法用语言把二者分开。这条「不可分辨者同一」的原理，是数学里把「同一个东西」写进符号的正式语法。

证明思路。把每个元素换成它所在的等价类；函数与关系在类上重新定义，相容性保证定义不依赖代表的选择（这正是「良定义」）。然后对 φ 归纳：原子公式的每个元解释都被类替换，真值不变；联结词与量词沿归纳假设平移。∎

回到完备性证明。§2.7 第五步的项模型正是本定理的一次壮丽应用：那里的 ∼ 由 (t = u) ∈ Γ* 定义，论域就是项的等价类。语法世界里的「相等」被商成了语义世界里的「同一」——这一步若不做，项模型里会出现「两个不同的项却相等」的尴尬。

方法论小结。等号在一阶逻辑里有双重身份：作为被公理管住的符号（(E1)(E2)），它保证替换与推理干净；作为被商掉的冗余（定理 2.23），它让「伪模型」总能归正。两条合起来，是本章一切模型的卫生标准。

第二章 一阶逻辑：量词、结构与完备性2.11 前束范式与量词的交换律

★★ 量词一旦叠起来，次序就成了门户。本节先把量词统统拧到公式最前（前束范式），再逐一清点：哪些次序可以互换、哪些一旦互换就变弱。

证明思路（一组重写规则）。① 改名：有界变元可换成不曾出现的新名，避免冲突；② 对偶：¬∀x φ ≡ ∃x ¬φ、¬∃x φ ≡ ∀x ¬φ；③ 提出量词（当 x 不在 ψ 中自由）：(∀x φ) ∧ ψ ≡ ∀x(φ ∧ ψ)，(∀x φ) ∨ ψ ≡ ∀x(φ ∨ ψ)，(∃x φ) ∧ ψ ≡ ∃x(φ ∧ ψ)，(∃x φ) ∨ ψ ≡ ∃x(φ ∨ ψ)；对 → 则视方向把量词对偶地推到另一侧。反复应用，量词逐个外提，直到全部落在最前。∎

记忆口令。「存在一个万能的」蕴含「各人都有各自的」，反之不然。把这句话和 §2.7 见证性质对照：Henkin 常元之所以必要，正因为 ∃x 的见证可能随机而异，不允许一个常元包打天下。

第二章 一阶逻辑：量词、结构与完备性2.12 公理系统的一般理论：独立性与相对一致性

★★★ 前三章反复说「公理」「理论」「模型」，本节把话说全：评价一套公理系统，有五个标准问题。它们是元数学的仪表盘，也是本册后续所有「某某定理不可证」讨论的词汇表。

方法一：独立性的模型法。要证 A 独立于 T ∖ {A}，只需造出一个模型使 T ∖ {A} 为真而 A 为假——由完备性，T ∖ {A} ⊬ A。这就是「相对一致性」：要证「A 反了也不出矛盾」，就把「¬A」摆进一个具体世界里展览。

方法二：范畴性与完备性的区别。二者极易混淆。范畴性谈「模型之间像不像」，完备性谈「句子能不能判」。一阶逻辑里，范畴性极难：由紧致性，任何有无限模型的一阶理论都有非标准模型（§2.9），故一阶理论几乎不范畴；而二阶逻辑可以做到范畴（如二阶算术的唯一模型），代价是失去完备性。这条「范畴性↔完备性」的跷跷板，是一阶逻辑设计的根本取舍。

可判定性的两个极端。命题逻辑可判定（真值表）；一阶逻辑不可判定（丘奇–图灵 1936，第四章）。但个别理论仍可判定：无等号的一元关系理论可判定、实闭域理论可判定（塔斯基 1948）。语言的强弱与可判定性成反比——这条规律是第四章的中心议题。

第二章 一阶逻辑：量词、结构与完备性2.13 实例：希尔伯特的几何公理系统

★★★ 1899 年，希尔伯特出版，把欧几里得两千年来「看图说话」的几何，重写成一套严格的公理系统。它是一阶逻辑最早的、也是最著名的实例之一。

希尔伯特只放三个原始概念：点、直线、平面；只放三种原始关系：关联（在……上）、介于（在……之间）、合同（全等）。其余一切几何概念，都要靠这六个词与五组公理定义出来。五组如下。

三处用心，值得逐一指出。其一，原始概念被刻意「留白」：公理不给点和直线下定义，而是隐定义——任何满足这五组的对象系统都叫「几何」，点线可以不是直觉里的点线。其二，平行公理自成一组：把它换成「过外点至少两条平行线」，得到双曲几何；换成「没有平行线」，得到椭圆几何——三种几何共用其余四组公理，由模型法（§2.12）证明第五公设独立。其三，连续公理把「数」请进几何：V₁ 让线段可以拿整数去量，V₂ 保证直线上不多不少——这两条使实数模型 ℝ² 成为几何的「标准解」。

史实补注：希尔伯特的原书还含用于空间情形的关联公理 I₄–I₈，通常与 I₁–I₃ 合称为「关联组」。本页按平面几何列出十六个基本条款，它已足够支撑欧氏平面几何的绝大部分定理。

第二章 一阶逻辑：量词、结构与完备性2.14 实例：一阶算术 PA 的公理

★★★ 几何之外，另一套最重要的实例来自数论：把自然数的全部性质编成一阶公理，得到的系统叫皮亚诺算术（PA）。它短小、著名，且藏着本册最重要的一处陷阱。

PA 的语言只含常量 0、一元函数 S（后继）、二元函数 + 与 ·、二元关系 <。公理共七条（其中第七条是一个模式）。

陷阱就在这里。(P7) 不是一条公理，而是一族：语言里有多少个公式 φ，就有多少条归纳公理——无穷多条。因此 PA 不能被有限多条公理替换：任何有限的公理集，只要在 𝒩 中为真，就还容许非标准模型（由紧致性，§2.9）。这是「无穷公理模式」与「有限公理」的分水岭。

很多模型，一个标准。标准结构 𝒩 当然是 PA 的模型；但 §2.9 造出的非标准模型 ℳ 也是。于是 PA 不范畴（模型不同构），也不完备（存在句子在 𝒩 真而在 ℳ 假，故 PA 判不出它——这是第五章哥德尔不完备性的雏形）。𝒩 的特殊在于它是所有模型里「最小的」：它是 PA 的标准模型，其余都在它头上长出无穷大元素。

把三套实例并置，可见一阶逻辑的三种姿态：几何公理描述关系（点线关联），PA 描述运算（后继、加乘），两者都是一阶理论的实例。下一节补上第三套——塔斯基的初等欧氏几何，它把几何几乎整个装进一阶语言。

第二章 一阶逻辑：量词、结构与完备性2.15 实例：Tarski 的初等欧氏几何

★★★ 希尔伯特把几何公理化，却仍站在集合论的台阶上；塔斯基追问更进一步的问题：几何能不能整个装进一阶逻辑——不用「点集」「子空间」，只用一阶量词？答案是可以，而且这个一阶理论既完备又可判定。

塔斯基（1926 年起，1951 年发表）的方案极其克制：论域就是「点」，原始关系只留两个——介于 β(x, y, z)（y 在 x 与 z 之间）与等距 δ(x, y, z, u)（线段 xy 与 zu 一样长）。仅此二词，就能定义线段、直线、角、全等、圆，乃至一切初等几何概念。

与希尔伯特的关键差别。希尔伯特把「连续」写成一条关于点集的公理，那是二阶的；塔斯基把它拆成无穷多条一阶模式，于是整个理论落在完备性定理的势力范围内。塔斯基 1948 年证明：初等欧氏几何是完备且可判定的——存在一台机器，对任何几何命题判定其真伪。这与 PA 的不可判定形成刺眼对比（§2.16 会解释为什么）。

实闭域模型。标准模型是平面 ℝ²：点是有序实数对，β 与 δ 按通常欧氏几何解释。更一般地，任何实闭域 K（如实数、实代数数）的 K² 都是模型。塔斯基理论的完备性，本质上是「实闭域理论完备」的几何翻译——这条翻译通道，下一节会再次走上。

第二章 一阶逻辑：量词、结构与完备性2.16 实例：群、环、域的公理与几何的对照

★★ 把本章的三套几何实例与代数里最常见的三类结构并置，会照出一件深刻的事实：同是一阶理论，「能说什么」的差异决定了「能判定什么」。

代数与几何，两种「原始概念」。代数理论的原始符号是函数（运算），几何理论的原始符号是关系（点线的位置）。这一差别看似只是记号口味，实则决定了可处理性：函数结构允许我们把项写成一串运算，于是代数判断常能归约为解的消去；关系结构则更贴近几何，但一阶表达力也随之改变。

一条分界线：量词消去。实闭域之所以可判定，是因为它能消去量词：理论中每个公式都等价于一个不含量词的公式（由多项式等式与不等式拼成）。一旦量词消失，真值就变成代数方程组的可解性，判定便有了算法。PA 缺的正是这个——它的量词无法被有限地消除，算术的表达力又刚好够编码「可证性」本身（§第五章），于是掉进不可判定。可判定与不可判定之间的那道墙，就立在量词能否被消去上。

历史与工程注记。群论的字问题（判定两词是否代表同一元素）由 1955 年 Novikov 与 1958 年 Boone 独立证否——存在有限呈示的群其字问题不可判定；而交换群的字问题可判定。这再次印证本节的主线：结构越「狭窄」，判定越有希望；结构越「自由」，判定越渺茫。

第二章 一阶逻辑：量词、结构与完备性2.17 从公理到定理：形式化的代价与收获

★★ 本章走了很长的路：从符号表到满足关系，从希尔伯特系统到完备性。收束之前，值得停下来算一笔总账：把数学塞进形式系统，究竟付出了什么、又拿回了什么？

代价之一：冗长。形式证明不允许跳过任何一步。§2.6 里「φ → φ」要写五行；怀特海与罗素《数学原理》（1910–1913）中「1 + 1 = 2」的证明要熬到第 379 页（编号 110·643），还附一句著名的评论：这个命题「偶尔有用」。形式证明的长度与人的直觉严重脱节。

代价之二：直觉被抹平。形式语言只说它能说的事。几何直觉里「两点之间直线最短」的图画感，在一阶公理中化为一段无图像的符号串；「显然」二字在形式证明里没有位置——每一步都要报出公理或规则的名字。这份迂腐，正是 §2.17 想让人亲眼看见的。

收获之一：无歧义与可检查。形式化把「这句话什么意思」的争论，换成「这串符号合不合规则」的机械核对。证明对象一旦写全，正确性就变成可被机器逐行验证的性质——这是第六章 Coq、Lean 得以存在的全部前提。

收获之二：元定理成为可能。正因为系统被写死，才能对系统本身发问并作答：本章的完备性、紧致性，以及每一个「独立」「不可判定」结论，都建立在形式化的基础上。没有形式化，就没有「某某定理不可证」这类断言——因为「可证」这个词还没有定义。

收获之三：统一。几何、算术、群环域，统统落入同一套语言与语义。公理化方法由此显形为三步：用公理隐定义概念（点线不必是直觉的点线）、用模型给公理找解释（相对一致性）、用证明论审问系统本身（独立性、完备性、可判定性）。第三步正是本册后四章的全部内容。

本章到此收束。三条主干已经立好：语义（结构与 ⊨）、语法（公理与 ⊢）、会师（完备性 —— 二者相等）。下一章把镜头对准「证明本身」：它长什么样、如何化简、与程序有何关系。在那之前，先做例题与习题，把这些机器亲手转一遍。

第二章 一阶逻辑：量词、结构与完备性例题课（一）：语义与真值表的实操

例题 2-1（在结构中算真值）。取标准算术结构 𝒩 = (ℕ; 0, S, +, ·, <)。判断下列句子的真值：① ∀x∃y(x < y)；② ∃y∀x(x < y)；③ ∀x(x < S(x))。

解。① 真。任给 x，取 y = S(x) 即得 x < x + 1。② 假。若存在 y 大于一切自然数，取 x = S(y) 便矛盾——没有最大的自然数。③ 真。对每个 x，x 小于它的后继，由 (S5) 逐点兑现。注意①②的真假相反：两者只差量词次序（§2.11）。∎

例题 2-2（判断有效式）。判断 ⊨ ∀x P(x) → P(c)（c 为常量符号）是否成立。

解。成立。设 𝒜 是任一结构、s 是任一赋值，且 𝒜 ⊨ ∀x P(x)[s]。由 (S5)，对一切 a ∈ A 有 𝒜 ⊨ P(x)[s(x ↦ a)]；特别地取 a = c^𝒜，得 𝒜 ⊨ P(c)。因 𝒜 任意，故 ⊨ ∀x P(x) → P(c)。∎ 注：证明用到论域非空（否则 c^𝒜 可能不存在）；这正是定义 2.5 逼论域非空的回报。

例题 2-3（自由变元的清点）。公式 φ := ∀x(P(x) → R(x, y)) ∧ ∃y Q(y) 是句子吗？若不是，写出它的全部自由变元。

解。不是句子。逐处清点：∀x 管辖 (P(x) → R(x, y))，其中两处 x 均被约束，y 在此自由；∃y 只管辖 Q(y)，其中 y 被约束。故自由变元集为 {y}（来自 R(x, y) 中的那个 y）。同名 y 一处自由、一处约束——§2.2 的管辖规则在此登场。∎

例题 2-4（有限结构上手工判真）。取论域 A = {0, 1}，二元关系符号 R 解释为「不相等」：R^𝒜 = {(0,1), (1,0)}。判断 ∀x∃y R(x, y) 与 ∃y∀x R(x, y) 的真值。

解。逐个元素验证。① ∀x∃y R(x, y)：x = 0 时取 y = 1；x = 1 时取 y = 0——两处都有见证，故真。② ∃y∀x R(x, y)：若 y = 1，需 R(1, 1) 真，但 (1,1) ∉ R^𝒜，失败；若 y = 0，需 R(0, 0) 真，失败。故假。两个句子真假相反，再次印证 ∀∃ ⊭ ∃∀。∎

第二章 一阶逻辑：量词、结构与完备性例题课（二）：证明与推演的实操

例题 2-5（推演：量词分配）。在希尔伯特系统中证明 Γ ⊢ ∀x Q(x)，其中 Γ = {∀x(P(x) → Q(x)), ∀x P(x)}。

解。给出一行行可核对的推演（每步注明依据）：

答。推演成立，Γ ⊢ ∀x Q(x)。∎ 复盘：Gen 的使用有条件——x 不得在前提中自由，否则会把「前提对某个特定的 x 成立」误抬成「对一切 x 成立」。此处前提是句子，条件满足。

例题 2-6（定理：假言三段论）。证明 ⊢ (φ → ψ) → ((ψ → χ) → (φ → χ))。

解。先用演绎定理（可由 (A1)(A2) 证明的元定理：若 Γ, φ ⊢ ψ 则 Γ ⊢ φ → ψ）。在 Γ = {(φ → ψ), (ψ → χ)}、假设 φ 下推演 χ：① φ（假设）；② φ → ψ（前提）；③ ψ（①② MP）；④ ψ → χ（前提）；⑤ χ（③④ MP）。故 (φ→ψ), (ψ→χ), φ ⊢ χ。对 φ 用一次演绎定理得 (φ→ψ), (ψ→χ) ⊢ φ → χ；对 (ψ→χ) 再用一次得 (φ→ψ) ⊢ (ψ→χ) → (φ→χ)；最后对 (φ→ψ) 用一次，即得 ⊢ (φ→ψ) → ((ψ→χ) → (φ→χ))。∎

例题 2-7（紧致性的应用）。证明：不存在一组一阶句子 T，使 𝒜 ⊨ T 当且仅当 A 有限（即「有限性」不可一阶刻画）。

解。反设这样的 T 存在。对每个 n ≥ 1 令 σ_n 表示「至少有 n 个不同元素」：∃x₁…∃x_n ⋀_i<j x_i ≠ x_j。考虑 T′ = T ∪ {σ_n : n ≥ 1}。任取 T′ 的有限子集，它只含有限多个 σ_n，取一个够大的有限结构即可同时满足 T 与这些 σ_n。故每个有限子集有模型，由紧致性 (定理 2.20)，T′ 有模型 ℬ；但 ℬ ⊨ σ_n 对一切 n，故 B 无限，于是 ℬ ⊨ T 却有无限论域——与 T 只容许有限模型矛盾。∎

例题 2-8（换序的另一方向）。判断 ∃x∀y R(x, y) → ∀y∃x R(x, y) 是否有效。

解。有效。设 𝒜 ⊨ ∃x∀y R(x, y)[s]，则由 (S6) 存在 a ∈ A 使 𝒜 ⊨ ∀y R(x, y)[s(x ↦ a)]，即对一切 b 有 𝒜 ⊨ R(x, y)[s(x ↦ a, y ↦ b)]。于是对每个 b，取 x = a 作为见证，便有 𝒜 ⊨ ∃x R(x, y)，从而 𝒜 ⊨ ∀y∃x R(x, y)[s]。因 𝒜, s 任意，故该式有效。∎ 注：换个变量名看，这正是 §2.11 的 ∃∀ ⊨ ∀∃；反方向由例题 2-4 的两个句子真假相反而失败。

第二章 一阶逻辑：量词、结构与完备性习题课（一）：联结词与语义

习题 2-1（热身·清点变元）。指出下列公式的全部自由变元，并判定哪些是句子：① ∀x(P(x) → R(x, y))；② ∃x R(x, x) ∧ ∀y S(y)；③ P(x) → ∀x P(x)。

提示。① y 自由（x 被 ∀ 约束），不是句子。② 两处量词各自管住 x、y，无自由变元，是句子。③ 前半的 x 自由、后半的 x 被 ∀ 约束——量词只管到紧随的小公式，管不到前面的 P(x)；故自由变元为 {x}，不是句子。答案要点：先画管辖范围，再逐处标记。

习题 2-2（有限结构判真）。取论域 A = {0, 1, 2}，二元关系符号 < 解释为通常的小于。判断：① ∀x∃y(x < y)；② ∃x∀y(y < x ∨ y = x)。

提示。① x = 2 时找不到更大的 y，故假。② x = 2 时对 y = 0, 1, 2 都有 y < 2 ∨ y = 2，故真（2 是最大元）。答案要点：有限论域上，∀ 逐个兑现、∃ 找一个见证，必能算完。

习题 2-3（有效或反驳）。判定下列公式是否有效，有效者说明理由，无效者给出反例结构：① ∀x(P(x) ∨ Q(x)) → (∀x P(x) ∨ ∀x Q(x))；② (∃x P(x) ∧ ∃x Q(x)) → ∃x(P(x) ∧ Q(x))。

提示。两者都无效，同一结构同时反驳：取 A = {0, 1}、P^𝒜 = {0}、Q^𝒜 = {1}。则① 前件真、后件假；② 前件真（两类各非空）、后件假（无一元素同时属于两类）。答案要点：全称对 ∨ 不分配、存在对 ∧ 不分配。

习题 2-4（次序反例）。给出一个结构使 ∀x∃y R(x, y) 真而 ∃y∀x R(x, y) 假；再判断 (∃y∀x R(x, y)) → (∀x∃y R(x, y)) 是否有效。

提示。取 𝒩 = (ℕ; <)：前者每个数都有更大的数（真），后者要求一个数大过一切数（假）。第二问有效——同一个见证 b 自然可以给每个 x 用（§2.11 (ii)）。答案要点：强弱只在一处——见证能否随 x 变化。

习题 2-5（翻译成可满足性）。利用「Γ ⊨ φ 当且仅当 Γ ∪ {¬φ} 不可满足」，判定 {∀x P(x)} ⊨ P(c) 是否成立。

提示。检查 Γ′ = {∀x P(x), ¬P(c)}。若 𝒜 ⊨ ∀x P(x)，由 (S5) 对一切元素（含 c^𝒜）都有 P 真，故 𝒜 ⊭ ¬P(c)——两个句子不可能同时满足，Γ′ 不可满足，故后承成立。答案要点：把「蕴含」翻译成「反面不可满足」，是语义证明的通用套路。

第二章 一阶逻辑：量词、结构与完备性习题课（二）：证明、公理与边界

习题 2-6（推演·∀ 对 → 的分配）。在希尔伯特系统中证明 {∀x(φ → ψ)} ⊢ ∀x φ → ∀x ψ。

提示。先用 (Q1) 从前提得 φ → ψ（t = x）；再证 ∀x φ ⊢ φ（(Q1)），两次 MP 得 ψ，一次 Gen 得 ∀x ψ；最后用演绎定理收口。注意 Gen 要求 x 不在前提 {∀x(φ→ψ), ∀x φ} 中自由——两者皆句子，合法。答案要点：这与例题 2-5 是同一台机器，只是把 P, Q 换成一般公式。

习题 2-7（紧致性·任意大的有限模型）。证明：若一组句子 T 有任意大的有限模型（对每个 n 都有一个基数 ≥ n 的模型），则 T 有无穷模型。

提示。照抄例题 2-7 的骨架：令 σ_n 表示「至少 n 元」，考察 T ∪ {σ_n : n ≥ 1}。任一有限子集只需有限多条 σ_n，由一个够大的有限模型满足；紧致性给出整体模型，其论域无限。答案要点：「任意大有限」+ 紧致性 =「无穷」，这一步是造非标准模型的通用发动机。

习题 2-8（模型法·证明独立）。说明乘法交换律 ∀x∀y(x · y = y · x) 独立于其余群公理。