第3卷 第5章 莱布尼茨之梦

学习目标

• 能用四行真值表说明材料蕴含何时为假，并把它改写成 ¬A∨B
• 能区分语义学与句法学，按 F1–F4 判断字符串是否为形式系统 H 的公式
• 能识别 P1–P4、公理实例和 Modus Ponens，复核有限公式序列何时构成证明
• 能沿 L1–L5 重建 A→A 的形式证明，并说明“真”与“可证”的边界

从“若尤里，则非泰朵拉”开始

第3卷第5章从尤里对“若A，则B”的不满开始。她接受前件为真时的两行，却不理解前件为假时，整个蕴含为什么都算真。

先预测：日常语言里的“若……则……”和命题逻辑的\Rightarrow有什么差别？不谈含义，只看字符串，机器怎样判断一行是不是公式、公理或证明？看起来显然成立的A\to A，为什么不能一句“它永远为真”就结束？

本章把学习者带过两座桥：

1. 从含义世界进入式子世界，把推理变成机械变形；
2. 从普通数学进入形式化的数学微缩模型，用数学研究证明本身。

5.1 “若……则……”的含义

A与B各有真假两种状态，因此共有四种组合。为：

A	B	A\Rightarrow B
假	假	真
假	真	真
真	假	假
真	真	真

蕴含只在一行失败：前件A已经为真，后件B却为假。等价式把这件事写得更直接：

$$A\Rightarrow B \equiv \neg A\lor B.$$

要让右侧为假，必须同时有：

$$\neg A\text{ 为假}, \qquad B\text{ 为假},$$

也就是A真而B假。当前件A为假时，\neg A为真，所以整个析取为真。这叫材料蕴含。

尤里尝试把前件为假时的两行也设为假。原章把所有候选列出来后发现：

• 若只在A,B都真时为真，得到的是A\land B；
• 若结果总跟B相同，前件A没有作用；
• 若A,B同真同假时为真，得到的是等价；
• 剩下那个只排除真到假的真值函数，才是材料蕴含。

数学符号的定义是人为约定，但不是任意使用：一旦真值表固定，后续等价变形就必须服从它。

莱布尼茨之梦：让争论变成计算

Leibniz设想把思考变成计算：若概念和规则能被精确符号化，人们面对争议时便可检查计算，而不是继续凭模糊措辞争执。这不是说机器自动理解世间一切，而是提出一条路线：

$$\text{含义世界} \longrightarrow \text{式子世界} \longrightarrow \text{机械变形} \longrightarrow \text{含义世界}.$$

例如“苹果总价”先被翻译成关于未知数x的方程；解方程时暂时不想苹果，只按代数规则变形；得到x=120后，再把120解释成价格。镜子是否有用，取决于最初的形式化是否忠实，以及变形规则是否可靠。

不会消灭含义。它把含义集中在“进入”和“返回”两道边界，中间阶段则尽量让每一步都可重复检查，形成机械性计算。

“理性的界限？”不是现成结论

尤里听人把哥德尔不完备定理概括成“数学不完备，所以理性有界限”。原章在此先挂起判断：尚未定义形式系统、可证明性、一致性和足够强的算术之前，这句话过于宽泛。

哥德尔定理不是“所有数学都失败”，也不是“人类理性被一句话封顶”。后续必须明确：

1. 谈的是哪个形式系统；
2. 系统满足哪些可有效描述、一致性和表达能力条件；
3. “不完备”指存在何种句子不能在系统内证明或否证。

本章的任务是先制造一台足够小、每个零件都看得见的形式系统。

5.2 “若泰朵拉，则非尤里”：学习不能装懂

上学路上，泰朵拉询问如何备战高考。她害怕限时考试，容易卡在一道题上不肯转向。原章给出的办法不是一句“多刷题”，而是把问题拆成可练技能：用计时赛训练时间分配，课堂先保持听讲主线，把疑问快速记下，课后再深挖。

更重要的是不要装懂。即使周围人都说简单，只要自己无法说明根据，就应保留“这里还不懂”的标记。理解可以暂时欠账，但不能把欠账伪装成结清。

这段叙事与形式证明直接相连。课堂上集中听清规则，课后再逐行追问根据；限时能力与深思能力并不互相否定，而是在不同阶段承担任务。泰朵拉从“严谨思考、重视定义、重视语言”获得的自信，也正是后面面对复杂符号串时不逃开的基础。

5.3 “若米尔嘉，则米尔嘉”：语义学与句法学

放学后的教室里，米尔嘉提出构造命题逻辑的形式系统 H。研究逻辑有两种视角：

视角	研究对象	典型问题
语义学（Semantics）	解释、真假值、模型	公式在所有赋值下都真吗？
句法学（Syntax）	字符串、生成规则、证明	公式能从公理和规则推出吗？

前面的真值表属于语义学。本节主动“不使用真假值”，只问形式。形式系统H按顺序定义：

1. 逻辑公式；
2. 公理和推理规则；
3. 证明和定理。

这是“用数学研究数学”的第一步：先把数学推理压缩成可以逐行检查的微缩模型。

逻辑公式：F1-F4的递归语法

形式系统H的公式由四条递归定义规定：

$$\mathrm{F1}\quad \text{若 }x\text{ 是变量，则 }x\text{ 是逻辑公式};$$ $$\mathrm{F2}\quad \text{若 }x\text{ 是逻辑公式，则 }\neg(x)\text{ 是逻辑公式};$$ $$\mathrm{F3}\quad \text{若 }x,y\text{ 是逻辑公式，则 }(x)\lor(y)\text{ 是逻辑公式};$$ $$\mathrm{F4}\quad \text{只有F1-F3生成的字符串才是逻辑公式}.$$

变量取A,B,\ldots,Z,A_1,A_2,\ldots，因此变量数量不受26个字母限制。F2与F3是：

$$A, \quad \neg(A), \quad \neg(\neg(A)), \quad (\neg(A))\lor(A)$$

都能写出有限构造树。

熟悉的：

$$(A)\land(B)$$

不是H的公式，因为F1-F3没有符号\land。字符串A\lor B也不是本章严格语法中的公式，因为F3要求写成(A)\lor(B)。括号不是装饰，而是字符串的一部分。

再定义蕴含为缩写：

$$(x)\to(y): = (\neg(x))\lor(y).$$

因此(A)\to(A)只是(\neg(A))\lor(A)的简写。此刻不能说它“显然为真”，因为当前正在句法世界，尚未调用真值解释。

公理模式P1-P4

H把下列四种形式定义为：

$$\mathrm{P1}\quad ((x)\lor(x))\to(x),$$ $$\mathrm{P2}\quad (x)\to((x)\lor(y)),$$ $$\mathrm{P3}\quad ((x)\lor(y))\to((y)\lor(x)),$$ $$\mathrm{P4}\quad ((x)\to(y)) \to (((z)\lor(x))\to((z)\lor(y))).$$

其中x,y,z可以代入任意逻辑公式，所以P1-P4是公理模式。例如令P1中的x=A：

$$((A)\lor(A))\to(A)$$

是公理。(A)\to(A)虽然在语义上有效，却不是P1-P4的直接实例，因此不是公理。

句法视角下，“公理”并不先解释成“宇宙中自明为真的话”，而是证明序列可无条件使用的起点。公式是否匹配四个模式，可以由公理测定仪机械核查。

推理规则、证明和定理

H只有一条推理规则：

$$\mathrm{MP}\qquad \frac{x\qquad (x)\to(y)}{y}.$$

它叫 Modus Ponens（假言推理）。应用时只比较形式：已有x，又有以同一个x为前件、以y为后件的蕴含式，就可写下y。

形式证明 被定义为有限公式序列：

$$a_1,a_2,\ldots,a_n.$$

每一行a_k必须满足以下之一：

1. a_k是某个公理模式的实例；
2. 存在更早的行a_s,a_t，其中s,t\lt k，可由它们通过MP推出a_k。

的顺序不可打乱，因为依据必须先出现。存在这样一份证明、并位于其最后一行的公式，称为H的形式定理。

5.4 “不是我，还是我”：证明A蕴含A

米尔嘉留下作业：

$$(A)\to(A)$$

是形式系统H的定理吗？

不能用“显然”“同一律”或真值表回答；必须只使用P1-P4与MP，构造以目标为末行的有限序列。

L1：取P1实例

在P1中令x=A：

$$\mathrm{L1}\quad ((A)\lor(A))\to(A).$$

L2：取P4实例

在P4中令：

$$x=(A)\lor(A), \qquad y=A, \qquad z=\neg(A).$$

得到：

$$\begin{aligned} \mathrm{L2}\quad &(((A)\lor(A))\to(A))\\ &\to \bigl( ((\neg(A))\lor((A)\lor(A))) \to ((\neg(A))\lor(A)) \bigr). \end{aligned}$$

L3：取P2实例

在P2中令x=A,y=A：

$$\mathrm{L3}\quad (A)\to((A)\lor(A)).$$

按蕴含缩写，L3也就是：

$$(\neg(A))\lor((A)\lor(A)).$$

若“若……则……”，则……

L1-L3备齐了三块形式材料。现在不解释其中的“若”，而是连续两次把缩写展开、按相同字符串匹配MP。

L4：第一次MP

对L1和L2使用MP，消去L2最外层前件：

$$\begin{aligned} \mathrm{L4}\quad ((\neg(A))\lor((A)\lor(A))) \to ((\neg(A))\lor(A)). \end{aligned}$$

重新使用蕴含缩写，L4等价写作：

$$((A)\to((A)\lor(A))) \to ((A)\to(A)).$$

L5：第二次MP

L3恰是L4的前件，因此再用一次MP：

$$\mathrm{L5}\quad (A)\to(A).$$

L1、L2、L3是公理实例，L4由更早的L1与L2得到，L5由更早的L3与L4得到。五行符合形式证明定义，所以(A)\to(A)是H的定理。

形式的形式与含义的含义

原章把独立解题过程分成“形式的形式”和“含义的含义”。向前搜索容易被无数公理实例淹没；从目标反推最后一步，便能问“MP的y要变成什么”“前件x应取什么”。这是一种证明搜索策略：

1. 固定目标的最外层结构；
2. 枚举可产生该结构的规则；
3. 把规则前提变成较小子目标；
4. 用公理模式填补可直接生成的子目标。

机器可以枚举字符串、匹配模式和执行MP，但“选择怎样的形式系统”“它是否忠实表达原问题”“搜索是否可行”仍需要元层面的研究。莱布尼茨之梦由此从一句愿望变成具体工程：语言、规则、证明检查器与搜索过程都必须明确。

章末，证明完成后，米尔嘉打电话发出周末游乐园邀约。形式系统的低温推理与人物关系的含义世界重新相遇：证明可以机械核查，邀约却不能只靠真值表读懂。

概念证据索引：让每个“根据”可检查

• 莱布尼茨之梦 / 若尤里则非泰朵拉 / 从若尤里，则非泰朵拉开始：从日常邀约的“若尤里，则非泰朵拉”进入，把含义先压缩成可计算符号。
• 若则的含义 / 若……则……的含义 / 蕴含真值表：四种真假组合定义“若则”的含义；真值表不是故事解释，而是固定的计算接口。
• 前件为假时蕴含为真 / 前件为假时，蕴含就没有真假 / 材料蕴含 / 只在前件真、后件假时为假：材料蕴含只排除真到假的一行；前件为假时无论后件真假都输出真。
• A蕴含B等价于非A或B / 含义世界与式子世界 / 机械性计算：A→B≡¬A∨B 把含义翻译为式子，使中间步骤能够机械性计算，再把结果解释回去。
• 理性的界限 / 若泰朵拉则非尤里 / 备战高考 / 计时赛 / 上课 / 不要装懂：哥德尔的宽泛口号不能代替条件；备战高考要用计时赛、保持上课主线，并对不懂的地方不要装懂。
• 若米尔嘉则米尔嘉 / 语义学Semantics / 句法学Syntax / 形式系统H / 用数学研究数学：米尔嘉的形式系统 H 用数学研究数学；语义学看模型和真假，句法学看字符串、规则与证明。
• 逻辑公式F1-F4 / 括号是字符串的一部分 / 递归定义：F1–F4 通过递归定义生成逻辑公式，括号是字符串的一部分，不能用排版直觉删掉。
• 蕴含是非与或的缩写 / 蕴含在H中只是非前件或后件的缩写 / 公理P1-P4 / 公理测定仪：H 中蕴含只是 ¬x∨y 的缩写；P1–P4 是公理模式，公理测定仪可以按字符串匹配实例。
• 证明论 / Modus Ponens / 假言推理 / 形式证明是有限序列 / 形式证明是有限公式序列 / 形式证明被定义为有限公式序列 / 形式定理：证明论研究规则与可证明性；Modus Ponens（假言推理）把 x 和 x→y 推出 y，有限公式序列的末行才是形式定理。
• 不是我还是我 / A蕴含A的证明 / L1-L5 / 沿L1-L5 / 形式的形式 / 含义的含义：不是我还是我这一题沿 L1-L5 展开两次 MP；A→A 的证明属于形式的形式，最后仍要回到含义的含义。
• 若若则则 / 邀约：若“若……则……”，则……的嵌套提醒我们保留括号；证明完成后的周末游乐园邀约把形式规则重新带回关系的含义。

互动实验与四步复盘

先猜：切换到句法视角后，A→A 的“永真”结论会不会自动成为公理？用实验按钮分开真值、字符串和证明，再沿四步图复核根据链。

Leibniz Logic Lab

把“真”“公式”和“可证”分开观察。

重置实验

真值检查句法检查证明检查

结论：A→A 在每个赋值下为真，但这还不是句法证明。

⚡分步1 / 4

1. 1
2. 2
3. 3
4. 4

重置

1. 语义：四行真值表锁定蕴含

先找唯一失败行 A=真、B=假，再用 ¬A∨B 复算，而不是把日常因果带进来。

上一步播放下一步

本章回顾：让根据显露出来

1. 材料蕴含只在前件真、后件假时为假，等价于非前件或后件。
2. 前件为假时蕴含为真，是二元真值函数的完整定义，不等于日常因果判断。
3. Leibniz之梦是把逻辑思考符号化、计算化，让争议转成可检查步骤。
4. 形式化在含义世界与式子世界之间往返，翻译是否忠实仍需判断。
5. 原章先挂起“哥德尔等于理性界限”的宽泛说法，要求之后明确系统和条件。
6. 泰朵拉的备考问题强调计时训练、课堂主线、课后深挖与不装懂。
7. 语义学研究解释和真值，句法学研究字符串、规则与可证明性。
8. F1-F3递归生成H的公式，F4排除所有未生成字符串。
9. 蕴含在H中只是非前件或后件的缩写，当前阶段不调用真假。
10. P1-P4是可实例化的公理模式，而A蕴含A本身不是直接公理。
11. MP根据x与x蕴含y推出y，只按公式形式匹配。
12. 形式证明是有限公式序列，每行必须是公理或由更早行按MP得到。
13. 有形式证明的公式才是H的定理，真与可证在定义上不同。
14. L1-L5用P1、P2、P4和两次MP证明了A蕴含A。
15. 从目标反推最后规则，是比盲目枚举公理实例更有效的证明搜索策略。

练习与答案

练习

1. 问题 1：材料蕴含。 为什么 A→B 只在 A 真、B 假时为假？用 ¬A∨B 复算前件为假的两行。

查看答案

当 A 真时 ¬A 假，析取的真假完全由 B 决定，因此只有 B 假时失败。当 A 假时 ¬A 真，¬A∨B 无论 B 是真还是假都为真。

2. 问题 2：语义还是句法？ 判断 (A)∨(B)、A∨B 和 (A)∧(B) 在本章的 H 中分别是什么，并说明理由。

查看答案

(A)∨(B) 由 F3 生成，是公式。A∨B 缺少 F3 要求的括号结构，不能直接算 H 的公式。(A)∧(B) 使用了 H 没有引入的 ∧，也不是公式。这里检查的是句法，不是在判断真假。

3. 问题 3：MP 检查。 已有 A 和 A→B，能否用 Modus Ponens 得到 B？如果只有 A→B 而没有 A 呢？

查看答案

第一种可以：前件 x=A 与已有公式完全匹配，后件 y=B 就是下一行。第二种不可以，MP 需要两个前提；“蕴含式存在”不等于它的前件已经被证明。

4. 问题 4：L1-L5。 A→A 为什么不是直接公理，却能成为 H 的定理？指出 L4 与 L5 各使用了哪次 MP。

查看答案

P1–P4 是公理模式，A→A 不直接匹配其中一个模式。L1、L2、L3 是公理实例；L4 用 L1 作前件、L2 作蕴含式应用第一次 MP；L5 再用 L3 和 L4 应用第二次 MP，因此 L5 是 H 的形式定理。

名词解释

本章出现的专业名词，用大白话再讲一遍。

材料蕴含

固定的二元真值函数 A→B；只有前件真、后件假时为假。

语义学

研究公式的解释、真假值、模型以及在赋值下是否成立。

句法学

研究字符串、公式生成规则、公理、推理和形式证明。

形式系统

由形式语言、公式规则、公理和推理规则组成的可机械检查模型。

递归定义

从基础项开始，按有限条构造规则逐步生成对象的定义方式。

形式证明

每一行都有公理或更早行作为根据的有限公式序列。