形式逻辑与自然演绎

数学证明会使用逻辑，形式逻辑则把语言、语义和允许的证明步骤明确写出来。本篇从这个角度继续展开，默认读者已经掌握数学基础中的实用语言。布尔代数与布尔函数侧重函数的表示与变换；这里关心的是怎样定义逻辑后承，以及怎样组织可逐步检查的推导。

FIT3080 的逻辑部分提供了从知识库、逻辑后承到推理过程的路线。我们在此补充自然演绎和量词规则的限制条件，让这些内容不只停留在 AI 课程的概览层面 [1][1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5., [2][2] OpenLogicProject, The Open Logic Text. 2026. Complete build, revision 9620cc7, July 12, 2026; CC BY 4.0. https://builds.openlogicproject.org/open-logic-complete.pdf。全文使用经典一阶逻辑，论域非空，函数符号解释为全函数。

语法：什么才是合法公式

一套符号表规定常量、函数和谓词符号，以及各自的元数。项表示对象：变量和常量都是项，把 $n$ 元函数符号应用于 $n$ 个项，仍得到一个项。原子公式断言项之间的关系；若语言包含等号，也可以断言两个项相等。联结词连接公式，量词约束对象变量。

例项与公式做不同的事

设 $a$ 是常量，$f$ 是一元函数符号，$R$ 是二元谓词符号。那么 $f(a)$ 是项，$R(a,f(a))$ 是公式。$\neg f(a)$ 不合法，因为否定作用于公式，不能直接否定一个表示对象的项。同样，$f(R(a,a))$ 在这套符号表中也不合法。

普通一阶逻辑的量词只对对象量化，不对谓词或函数量化。因此，若 $\forall R\,R(a,a)$ 中的 $R$ 真的是一个被量化的关系变量，这已经换到了另一类语言。形式化的第一步就是选定语言，并始终区分对象与关于对象的断言。

变量的某次出现由相应量词约束时，称为约束出现，否则称为自由出现。在 $P(x)\land\forall x\,Q(x)$ 中，第一个 $x$ 自由，$Q$ 中的 $x$ 受约束。没有自由变量的公式称为句子。统一改名一个约束变量不会改变含义，但新名字不能意外捕获别的变量。

语义：解释、模型与逻辑后承

解释 $\mathcal M$ 给出非空论域，为每个常量指定对象，为每个函数符号指定全函数，为每个谓词符号指定关系。变量赋值则为自由变量指定对象。因此，$\mathcal M,s\models\varphi$ 表示公式 $\varphi$ 在解释 $\mathcal M$ 和赋值 $s$ 下为真。句子的真值不依赖变量赋值，可以简写为 $\mathcal M\models\varphi$。

例语法相同，解释不同

考虑句子 $\forall x\,R(x,x)$。在整数上，把 $R$ 解释为 $\le$，句子就为真；解释为 $<$，句子就为假。变化的是解释，公式本身没有变。理论 $T$ 的模型，就是使 $T$ 中每个句子都为真的解释。

对句子集合 $\Gamma$，逻辑后承的定义是：

$$\Gamma\models\varphi \quad\Longleftrightarrow\quad \Gamma\text{ 的每个模型都满足 }\varphi.$$

句子在所有解释中为真，称为有效；至少在一个解释中为真，称为可满足；没有任何解释使它为真，称为不可满足。某个选定模型中的真，不等于逻辑有效。要反驳 $\Gamma\models\varphi$，必须给出一个满足全部前提、却使结论为假的反模型。

例如，$\Gamma=\{P\to Q,P\}$ 后承 $Q$；但 $\{P\to Q,Q\}$ 不后承 $P$，因为 $P$ 假、$Q$ 真就是反模型。若 $\Gamma$ 根本没有模型，那么在经典语义下它后承每个句子；这样的知识库无法区分有用结论与任意断言。

经典逻辑后承具有单调性：增加前提不会取消已有后承，但可能让原本可满足的知识库变得不可满足。这与可撤回的默认推理、概率推理有所不同；知识库里缺少某条事实，并不自动意味着它的否定成立。

推导与自然演绎

$\Gamma\vdash\varphi$ 表示在指定证明系统中，存在从前提 $\Gamma$ 到 $\varphi$ 的有限推导。推理规则规定一次合法的局部操作，证明把这些操作连成序列或树，证明搜索则负责寻找这样的证明。三者可能围绕同一个结论展开，但不是同一件事。

自然演绎按联结词组织引入规则与消去规则。下表描述规则模式，不是可以随意加入证明的新前提。

联结词	引入	消去
$\land$	由 $P$ 和 $Q$ 得到 $P\land Q$	由 $P\land Q$ 得到任一合取项
$\lor$	由 $P$ 得到 $P\lor Q$	由 $P\lor Q$，以及两种情况中各自对 $R$ 的证明，得到 $R$
$\to$	假设 $P$，推出 $Q$，解除假设后得到 $P\to Q$	由 $P\to Q$ 和 $P$ 得到 $Q$
$\neg$	假设 $P$，推出 $\bot$，解除假设后得到 $\neg P$	由 $P$ 和 $\neg P$ 得到 $\bot$

$\bot$ 表示矛盾，在这套系统中可以由它推出任意公式。要得到经典逻辑，还需加入一条经典原则，例如从 $\neg\neg P$ 推出 $P$ 的双重否定消去。仅有表中的规则还不能支持所有经典论证。双条件 $P\leftrightarrow Q$ 可以看成两个方向的蕴涵之合取的缩写。

解除假设是什么意思

临时假设属于一个子证明。解除它，就是关闭该子证明，并把结果记录为条件命题；这不会让原先假设的内容变成无条件成立的事实。

证明合取蕴涵其中一项

不使用任何前提，推导 $(P\land Q)\to P$。

行	公式	理由与作用域
1	$P\land Q$	临时假设，开启子证明
2	$P$	对第 1 行使用合取消去，仍在子证明内
3	$(P\land Q)\to P$	蕴涵引入，解除第 1–2 行的子证明假设

第 2 行依赖尚未解除的假设。最终得到的是一个蕴涵，而不是无条件证明了 $P$。

析取消去需要两个临时假设。从 $P\lor Q$ 出发，分别在假设 $P$ 和假设 $Q$ 的子证明中得到同一个 $R$，才能解除两个假设并推出 $R$。不能只挑一个方便的析取项，把它当成已经成立的事实。

量词规则及其限制条件

替换 $\varphi[t/x]$ 把 $x$ 的自由出现换成项 $t$，并避免变量捕获。下面的限制条件是规则的一部分，不能省略。

• **全称消去：**由 $\forall x\,\varphi(x)$ 得到 $\varphi(t)$，替换必须避免捕获。
• **存在引入：**由合法的实例 $\varphi(t)$ 得到 $\exists x\,\varphi(x)$。
• **全称引入：**对任意的新参数 $a$ 证明 $\varphi(a)$，再推出 $\forall x\,\varphi(x)$。$a$ 不能出现在该证明所依赖的未解除假设中，也不能残留在概括后的结论中。
• **存在消去：**由 $\exists x\,\varphi(x)$，开启一个以 $\varphi(a)$ 为假设的子证明，其中 $a$ 是新参数。若能推出 $\psi$，且 $a$ 不出现在 $\psi$ 或其他有效假设中，就可以关闭子证明并推出 $\psi$。

最后一条允许我们用一个未知见证进行推理，却不允许把关于这个特定见证的断言偷偷带出子证明。forall x: Calgary 的量词章节给出了带这些限制的详细推导 [3][3] OpenLogicProject, “forall x: Calgary, Chapter 36: Basic Rules for First-Order Logic,” . Natural deduction quantifier rules and their side conditions; accessed September 6, 2026. https://forallx.openlogicproject.org/html/Ch36.html。

例为什么要避免变量捕获

在 $\forall y\,R(x,y)$ 中，把自由变量 $x$ 换成 $y$。直接写成 $\forall y\,R(y,y)$，会把新插入的变量也约束起来，改变原意。应先把约束变量改名为 $z$，再替换，得到 $\forall z\,R(y,z)$。新插入的 $y$ 仍然自由。

证明从存在一个成员，推出存在一个满足结论的对象

已知 $\forall x\,(P(x)\to Q(x))$ 与 $\exists x\,P(x)$，证明 $\exists x\,Q(x)$。

行	公式	理由与作用域
1	$\forall x\,(P(x)\to Q(x))$	前提
2	$\exists x\,P(x)$	前提
3	$P(a)$	使用新见证参数，开启子证明
4	$P(a)\to Q(a)$	对第 1 行使用全称消去
5	$Q(a)$	对第 3、4 行使用蕴涵消去
6	$\exists x\,Q(x)$	对第 5 行使用存在引入
7	$\exists x\,Q(x)$	对第 2 行及子证明 3–6 使用存在消去

结论里没有 $a$，两个前提也没有提及它。我们证明了某个对象存在，没有声称一个事先命名的对象一定满足 $Q$。

若语言包含等号，还要使用自反性及等同替换：$t=t$，以及在避免捕获的前提下，把公式中的项换成与它相等的项。等号表示对象相同；不同的常量符号未必指向不同对象，除非另有不等条件。

量词的有效变换与错误变换

除了基础篇的量词否定律，还可以使用以下分配关系：

$$\forall x\,(P(x)\land Q(x)) \equiv (\forall x\,P(x))\land(\forall x\,Q(x)),$$ $$\exists x\,(P(x)\lor Q(x)) \equiv (\exists x\,P(x))\lor(\exists x\,Q(x)).$$

第一式中，任意对象同时满足两个谓词，恰好意味着每个谓词都对所有对象成立。第二式中，某个见证满足至少一个谓词，恰好意味着至少一个谓词存在见证。换成另外两个联结词，就不能无条件照搬。

例如，在 $D=\{0,1\}$ 上，令 $P$ 表示“等于 $0$”，$Q$ 表示“等于 $1$”。每个对象都满足 $P\lor Q$，但两个谓词都不是对所有对象成立。两个谓词各自有见证，却没有对象满足 $P\land Q$。这同时反驳了全称量词对析取、存在量词对合取的一般分配。

若论域有限且已明确列出，可以把全称量词展开为有限合取，把存在量词展开为有限析取。这个方法不能直接用于任意或无限论域。唯一存在写作 $\exists!x\,P(x)$，其展开式为

$$\exists x\bigl(P(x)\land \forall y\,(P(y)\to y=x)\bigr).$$

量词顺序决定依赖关系：$\forall x\exists y\,R(x,y)$ 允许每个 $x$ 有自己的见证，$\exists y\forall x\,R(x,y)$ 则要求所有 $x$ 共用一个见证。后面引入 Skolem 函数时，这个差别会直接影响定理证明器的处理方式。

用谓词描述程序规格

谓词可以描述程序的前置条件与后置条件。Hoare 三元组 $\{P\}\ C\ \{Q\}$ 表示部分正确性：若执行前的状态满足 $P$，而且命令 $C$ 终止，那么执行后的状态满足 $Q$。它本身不保证终止；完全正确性还需要证明这一点。

例如，一个用于计算整数阶乘的过程，可以要求输入 $n\ge 0$，后置条件为 $r=n!$，并约定 $0!=1$。这只是规格，不是任意实现都满足它的证明。还需要结合程序的执行语义与相关不变式进行检查。由此可见，谓词不仅能作为返回真假的测试，还能参与程序正确性的逻辑论证。

一致性、独立性与两种完备性

一致性和可靠性

定义一致性

理论 $T$ 一致，是指不存在句子 $\varphi$，使 $T\vdash\varphi$ 和 $T\vdash\neg\varphi$ 同时成立。在经典逻辑中，矛盾可以推出任意结论，因此一致性排除了这种退化。

可靠性（soundness）说的是推理系统尊重语义：若 $T\vdash\varphi$，则 $T\models\varphi$。它不等于说“任何公理都是真的”；它说的是，在公理都成立的模型中，合法推导不会把我们带到假结论。

证明所列自然演绎规则的可靠性

对推导树归纳，保持如下性质：满足所有未解除假设的解释与赋值，也满足当前结论。假设叶节点直接满足这一性质。合取的引入与消去、析取引入、蕴含消去和否定消去，由真值表保持该性质。析取消去时，至少一个分支的假设为真，对该分支使用归纳假设即可得到共同结论。蕴含引入时，若解除的假设为假，蕴含式直接为真；若为真，子证明给出后件。否定引入时，若解除的假设为真，子证明将推出假命题，故该假设必为假。没有解释满足假命题，因此矛盾消去保持可靠；双重否定消去则由经典真值语义成立。

量词规则使用捕获规避替换引理：计算 $\varphi[t/x]$ 的真值，等于将 $x$ 赋为项 $t$ 的值后计算 $\varphi$。先对项归纳，依次处理变量、常量和函数应用；再对公式归纳，原子谓词使用项的结论，联结词保持真值相等。遇到量词时，先将约束变量改名以避开替换，改变该变量的赋值便与替换 $x$ 互不干扰。这就证明了引理。全称消去和存在引入，只需取项 $t$ 的值作为相应对象。

全称引入时，将新参数解释为任意对象。新鲜性保证所有有效假设仍然成立，子证明因此对每个对象都成立。存在消去时，选择存在前提给出的见证，将新参数解释为该见证；子证明给出结论，而新鲜性保证改变参数既不影响其他假设，也不影响最终结论。等号自反性来自对象的同一性；相等项替换不改变项值，再由同样的结构归纳可知不改变公式真值。以上覆盖全部所列规则，完成归纳。

因此，在可靠的推理系统里，若能找到一个满足 $T$ 的模型，就能说明 $T$ 一致：否则某个句子及其否定都必须在同一个模型中为真。这个模型方法依赖于所采用的背景数学，并不是凭有限次试验就能保证任意理论一致。

公理独立与句子独立

一条公理 $A\in T$ 相对于其他公理独立，是指

$$T\setminus\{A\}\nvdash A.$$

一种证明方法，是找到一个让其余公理都成立、却让 $A$ 为假的模型。可靠性说明，如果其余公理能推出 $A$，这样的模型就不可能存在。

另一个常见说法是“句子 $\varphi$ 独立于理论 $T$”：这通常要求两个方向都不可证，即

$$T\nvdash\varphi \quad\text{且}\quad T\nvdash\neg\varphi.$$

对于 $T=\{P\}$，$P$ 真、$Q$ 真和 $P$ 真、$Q$ 假都是模型，因此 $Q$ 独立于 $T$。加上 $Q$ 或加上 $\neg Q$ 都会选出更小的一类模型。相反，在公理集 $\{P,P\to Q,Q\}$ 中，最后一条 $Q$ 可以从前两条推出，所以它是冗余公理。

平行公设是几何中的经典背景，但必须先说明保留了哪套公理。在适当公理化的中性几何中，可以用满足和不满足平行公设的模型展示其独立性。不能简单把球面上的“直线”换成大圆，就声称除了第五公设之外一切都保持原样；例如对径点之间存在多条大圆，其他条件也需要重新检查。

理论完备性与逻辑完备性

定义理论的句法完备性

理论 $T$ 完备，是指对其语言中的每个句子 $\varphi$，都有 $T\vdash\varphi$ 或 $T\vdash\neg\varphi$。若再要求一致，就不能同时有两者。$T=\{P\}$ 在包含 $P,Q$ 的命题语言中不完备，因为它不能决定 $Q$。

逻辑的语义完备性则是另一个性质：凡在所有前提模型中成立的结论，都能够通过该逻辑的推理规则推出，即

$$T\models\varphi\quad\Longrightarrow\quad T\vdash\varphi.$$

经典一阶逻辑有可靠且完备的标准证明系统。这并不意味着任意一阶理论都能决定每个句子：若不同模型对 $\varphi$ 有不同判断，语义完备性就没有要求理论必须证明其中一边。

哥德尔不完备性定理讨论的是另一层限制：一致、可有效公理化并包含足够算术能力的理论，不能决定其语言中的所有句子。它与一阶逻辑的完备性定理并不冲突，也不表示日常数学里的每道题都无法求解。这里先掌握两种“完备”回答不同问题，严格的元数学证明留待后续学习[2][2] OpenLogicProject, The Open Logic Text. 2026. Complete build, revision 9620cc7, July 12, 2026; CC BY 4.0. https://builds.openlogicproject.org/open-logic-complete.pdf。

练习

练习构造反模型

$\exists x\,P(x)$ 是否后承 $P(a)$？用一个模型说明，并解释为什么存在消去不能支持这一步。

查看解析

解

不能。取论域 $\{0,1\}$，让 $a$ 指向 $0$，只有 $1$ 满足 $P$。前提为真，结论为假。存在消去在子证明中引入一个新参数，不能直接把未知见证认作已有常量所表示的对象。

练习追踪临时假设

由 $P\to R$ 和 $Q\to R$，用自然演绎推出 $(P\lor Q)\to R$。

查看解析

解

假设 $P\lor Q$。在假设 $P$ 的子证明中，由 $P\to R$ 推出 $R$；在假设 $Q$ 的子证明中，由 $Q\to R$ 推出 $R$。用析取消去解除两个分类假设，再用蕴涵引入解除 $P\lor Q$。最初的两个蕴涵仍是整个推导的前提。

练习全称引入不能靠外推

某个证明假设 $P(a)$，随后直接写出 $\forall x\,P(x)$。哪项限制被违反了？给出一个含两个对象的反模型。

查看解析

解

$a$ 出现在推导所依赖的未解除假设里，不满足任意参数的要求。取论域 $\{0,1\}$，让 $a$ 表示 $0$，只有 $0$ 满足 $P$，就会出现假设成立而全称结论不成立的情况。

练习完备性不负责判定每个句子

在含命题字母 $P,Q$ 的语言中，令 $T=\{P\}$。为什么证明系统的完备性不要求从 $T$ 证明 $Q$ 或 $\neg Q$？

查看解析

解

$T$ 的模型中，$Q$ 可以为真，也可以为假，因此两个句子都不是 $T$ 的语义后承。完备性要求语义后承都有证明，并不要求在模型存在分歧时替理论选定一边。

从合法规则走向推理算法

规则说明哪些步骤合法，却没有规定先试哪一步，也没有说明搜索失败是否足以作出否定结论。命题逻辑的自动推理会把模型枚举、Horn 规则、归结和 SAT 写成明确过程；一阶逻辑的归结与定理证明再加入替换、见证依赖与终止性限制。

参考文献

1. [1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5. ↩
2. [2] OpenLogicProject, The Open Logic Text. 2026. Complete build, revision 9620cc7, July 12, 2026; CC BY 4.0. https://builds.openlogicproject.org/open-logic-complete.pdf a b
3. [3] OpenLogicProject, “forall x: Calgary, Chapter 36: Basic Rules for First-Order Logic,” . Natural deduction quantifier rules and their side conditions; accessed September 6, 2026. https://forallx.openlogicproject.org/html/Ch36.html ↩