第 9 讲 · 谓词公理、可靠完备与判定问题

谓词公理系统在命题系统上增加量词相关的公理和规则。难点不只是多了 $\forall$，而是每个量词规则都有自由变量条件。

谓词逻辑的公理系统

前三个公理模式仍是命题系统的 A1–A3。再加入：

$$\mathrm{A4}\quad \forall xQ(x)\to Q[x/t],$$

其中项 $t$ 对 $Q$ 中的 $x$ 可代入；

$$\mathrm{A5}\quad \forall x(Q\to R(x)) \to (Q\to\forall xR(x)),$$

其中 $x$ 不在 $Q$ 中自由出现。

推理规则包括 MP 与概括规则 UG：

$$Q\quad\Longrightarrow\quad\forall xQ.$$

不同教材对带前提推演中的 UG 还有更严格条件。本课程使用时要特别检查被概括变量是否在前提中自由出现。

完整谓词证明示例

证明

$$\vdash \forall xQ(x)\to\forall yQ(y),$$

其中 $y$ 不在 $Q$ 中自由出现。

1. $$\forall xQ(x)\to Q(y),$$ A4；
2. $$\forall y\bigl(\forall xQ(x)\to Q(y)\bigr),$$ 对第 1 行使用 UG；
3. $$\forall y\bigl(\forall xQ(x)\to Q(y)\bigr) \to \bigl(\forall xQ(x)\to\forall yQ(y)\bigr),$$ A5；
4. 由 2、3 MP 得结论。

每一处变量条件都重要。若 $y$ 在前件中自由出现，第 3 行就不是合法 A5 实例。

谓词系统中的演绎定理

安全版本要求移入前件的 $A$ 是闭公式：

$$\Gamma\cup\{A\}\vdash B \quad\Longleftrightarrow\quad \Gamma\vdash A\to B.$$

若 $A$ 有自由变元，UG 可能把依赖临时假设的变量错误地全称化，命题逻辑中的证明不能原样照搬。

可靠性、完备性和协调性

$$\Gamma\vdash Q\Longrightarrow\Gamma\models Q$$

称为可靠性。证明思路是对推演长度归纳：

• 公理在每个模型中有效；
• 前提在满足 $\Gamma$ 的模型中为真；
• MP 和 UG 保持真值。

$$\Gamma\models Q\Longrightarrow\Gamma\vdash Q$$

称为完备性。

若一个公式集能推出每个公式，就称它不协调；否则协调。经典逻辑中，矛盾前提会“爆炸”，即任意结论都可推出。

因此：

• $\Gamma\vdash Q$ 不能说明 $\Gamma$ 协调；
• 若 $\Gamma$ 不协调，则对所有 $Q$ 都有 $\Gamma\vdash Q$；
• 可靠系统的定理不会在语义上出错，但加入矛盾前提后仍可能推出任意式。

理论与模型

一个理论 $T$ 是某种形式语言中的公理语句集合。若结构 $\mathcal M$ 满足 $T$ 的每条公理，就称 $\mathcal M$ 是 $T$ 的模型。

例如群、环、域都可由若干一阶公理描述。自然数理论则给出 $0$、后继、加法、乘法等符号及其公理。

课件还用量词表达分析概念。例如函数在 $x_0$ 连续：

$$\forall\varepsilon>0\, \exists\delta>0\, \forall x\, \bigl( |x-x_0|<\delta \to |f(x)-f(x_0)|<\varepsilon \bigr).$$

随后可以把“极限唯一”“收敛序列有界”等普通数学证明拆成逻辑前提与推演，说明理论、公理和模型不是抽象装饰，而是在描述数学本身。

带等词的系统

若语言包含等号，还要加入反身性和替换相等对象不改变公式真值的公理，例如

$$t=t,$$

以及从 $t_1=t_2$ 推出函数值或谓词位置上可替换的公理模式。

等号不是任意二元谓词；它在模型中固定解释为对象相等。

判定、半判定与不可判定

一个问题可判定，意味着存在算法对每个输入都在有限步内停机，并正确回答“是”或“否”。

• 命题逻辑有效性可判定：有限真值表总能结束；
• 一阶逻辑有效性半可判定：若公式有效，可以枚举证明并最终找到；若无效，搜索可能永不停止；
• 含足够表达能力的一阶理论通常不可判定。

课件提到 Church 与 Turing 的结果、Gödel 编码及不完全性。要区分：

• 完备性定理：一阶逻辑的语义有效式都可形式证明；
• 不完全性定理：足够强且有效公理化的一致算术理论中，存在既不能证明也不能否证的语句。

前者谈整个一阶逻辑的证明系统，后者谈特定算术理论；二者不矛盾。

Löwenheim–Skolem 的提醒

一阶理论若有无限模型，通常也会有不同基数的模型。形式语言能约束结构，但未必能唯一钉死我们直觉中的那个无限对象。这是“理论”和“预想模型”之间的重要边界。