Lecture 2

Abstract

不可证明的公式怎样产生反模型？我们用避开目标公式的极大扩张证明经典完备性与紧致性，再以素理论构造 Kripke 典范模型，建立直觉主义完备性的真值引理。

我们先把上次留下的问题写清楚：我们已经给出了两套证明规则，也给出了两种理解“真”的方法，那么规则允许我们证明的公式，是否恰好就是相应语义下成立的公式？如果只证明规则不会把真命题变成假命题，我们还没有回答最有意思的方向：一个公式确实不能证明时，能不能把这个失败变成一个具体的反模型？

今天我们先在经典命题逻辑中完成这个构造，再看它怎样改造成直觉主义的 Kripke 模型。两种证明会反复用到同一个事实：假设集可以无限，但一份证明总是有限的。

1. 两套证明系统、两种语义和两个方向

我们用 $\Gamma\vdash_{\mathrm I}\varphi$ 表示在直觉主义自然演绎中，从假设集 $\Gamma$ 可以推出 $\varphi$。在这套规则上加上排中律，就得到经典系统，记为 $\Gamma\vdash_{\mathrm C}\varphi$。排中律是

$$\varphi\lor\neg\varphi, \qquad \neg\varphi:=\varphi\to\bot.$$

经典语义中的模型是一份赋值 $v:\mathsf{Prop}\to\{0,1\}$。原子命题的真值一旦确定，复合公式的真值就按照连接词的定义递归确定。例如

$$\begin{aligned} v\models\alpha\land\beta&\iff v\models\alpha\text{ 且 }v\models\beta,\\ v\models\alpha\lor\beta&\iff v\models\alpha\text{ 或 }v\models\beta,\\ v\models\alpha\to\beta&\iff v\not\models\alpha\text{ 或 }v\models\beta. \end{aligned}$$

$v\not\models\bot$，而 $v\models\Gamma$ 表示 $v$ 满足 $\Gamma$ 中每一个公式。因此

$$\Gamma\models_{\mathrm C}\varphi \iff \text{每个满足 }\Gamma\text{ 的赋值都满足 }\varphi.$$

直觉主义模型则允许信息随着时间增长。一个 Kripke 模型 $\mathcal M=(W,\le,V)$ 包括世界集 $W$、可达关系 $\le$ 和每个世界的原子赋值。这里把 $\le$ 取为偏序：它自反、传递、反对称。$w\le u$ 表示 $u$ 是 $w$ 的一种可能未来。信息只能增加，即

$$w\le u\quad\Longrightarrow\quad V(w)\subseteq V(u).$$

$V(w)$ 是在 $w$ 已经确立为真的原子集合。我们用 $w\Vdash\varphi$ 表示 $\varphi$ 在 $w$ 被迫使。合取和析取仍然在当前世界解释，蕴涵则必须检查所有未来：

$$\begin{aligned} w\Vdash p&\iff p\in V(w),\\ w\nVdash\bot,&\\ w\Vdash\alpha\land\beta&\iff w\Vdash\alpha\text{ 且 }w\Vdash\beta,\\ w\Vdash\alpha\lor\beta&\iff w\Vdash\alpha\text{ 或 }w\Vdash\beta,\\ w\Vdash\alpha\to\beta&\iff \forall u\ge w\;(u\Vdash\alpha\Rightarrow u\Vdash\beta). \end{aligned}$$

特别要区分 $w\nVdash p$ 与 $w\Vdash\neg p$。前者只说现在没有确立 $p$；后者说所有可能未来都不可能确立 $p$。如果未来某个世界有 $p$，当前即使没有 $p$，也不能迫使 $\neg p$。

我们相应定义

$$\Gamma\models_{\mathrm I}\varphi \iff \text{对每个 Kripke 模型及其中每个 }w, \quad w\Vdash\Gamma\Rightarrow w\Vdash\varphi.$$

于是要比较的是两个等价关系：

$$\Gamma\vdash_{\mathrm C}\varphi\iff\Gamma\models_{\mathrm C}\varphi, \qquad \Gamma\vdash_{\mathrm I}\varphi\iff\Gamma\models_{\mathrm I}\varphi.$$

从左到右叫健全性，从右到左叫完备性。这是两个系统各自的一对结论，不能把经典赋值与直觉主义证明规则交叉配对。

经典健全性为什么容易

我们先检查证明规则是否保持真。例如合取引入规则是

$$\frac{\Gamma\vdash\alpha\qquad\Gamma\vdash\beta} {\Gamma\vdash\alpha\land\beta}.$$

如果每个满足 $\Gamma$ 的赋值都满足 $\alpha$ 和 $\beta$，它当然也满足 $\alpha\land\beta$。蕴涵引入看起来只是把逗号换成箭头：

$$\frac{\Gamma,\alpha\vdash\beta}{\Gamma\vdash\alpha\to\beta}.$$

但它同样有语义依据。取一个满足 $\Gamma$ 的赋值。如果它满足 $\alpha$，就同时满足前提的全部假设，因此满足 $\beta$；如果它不满足 $\alpha$，$\alpha\to\beta$ 按经典蕴涵的定义已经为真。排中律也成立，因为在一份经典赋值中，$\alpha$ 不是真就是假。

对其他规则做同样的检查，再对有限证明树归纳，就得到

$$\Gamma\vdash_{\mathrm C}\varphi\quad\Longrightarrow\quad \Gamma\models_{\mathrm C}\varphi.$$

真正要做构造的是反方向。我们把它改写为逆否命题：

$$\boxed{\Gamma\nvdash_{\mathrm C}\varphi \quad\Longrightarrow\quad \exists v\;(v\models\Gamma\text{ 且 }v\not\models\varphi).}$$

2. 从假设集到理论：我们究竟允许多大的集合

为了构造赋值，我们先把证明信息集中到一个集合里。今天把理论定义为满足下面两个条件的公式集 $T$：

$$T\vdash\psi\Rightarrow\psi\in T, \qquad T\nvdash\bot.$$

第一个条件是对演绎封闭，第二个条件是一致。不同书会把任意公式集、仅演绎封闭的集合、或兼具一致性的集合都叫作“理论”；我们这里采用上述约定，后面也要说明采用的是哪套证明系统。

从一致的公式集 $\Gamma$ 出发，可以取演绎闭包

$$\operatorname{Cn}(\Gamma)=\{\psi:\Gamma\vdash\psi\}.$$

它不会增加原本推不出的结论。因为如果闭包中的有限多个公式足以证明 $\chi$，把这些公式各自从 $\Gamma$ 的证明代入，就得到从 $\Gamma$ 到 $\chi$ 的证明。特别地，原来一致的集合取闭包后仍然一致。

这里有一个很好的问题：我们是在谈有限个变量，还是可能无限多个变量？一个公式按定义是有限的，所以单独讨论一个公式的有效性时，它只涉及有限多个原子。例如 Peirce 公式

$$((p\to q)\to p)\to p$$

只有 $p,q$ 两个变量，经典赋值只有四种相关情况。但是 $\Gamma$ 可以包含无限多个公式，其中涉及的变量也可以无限多。不能因为结论 $\varphi$ 有限，就把全部前提也当成有限。

为方便显式枚举，我们通常先采用可数原子语言 $\mathsf{Prop}=\{p_1,p_2,\ldots\}$。由于公式是有限字符串，全部公式仍是可数的，尽管 $\Gamma$ 自身不必有限。更一般的语言也能处理，但要使用相应的集合论工具。下面证明中真正关键的有限性，来自证明：

$$\Gamma\vdash\chi \quad\Longrightarrow\quad \exists\Gamma_0\subseteq\Gamma\; (\Gamma_0\text{ 有限且 }\Gamma_0\vdash\chi).$$

我们只需看一份证明实际用了哪些未撤销的假设；证明树有限，所以它们只有有限多个。

3. 极大元引理、选择公理和一个无限帽子问题

我们将需要把一个集合扩大到不能再扩大。这里的“极大”是按包含关系说的：$T$ 是极大元，指不存在严格包含它、同时仍满足指定条件的集合。它并不意味着 $T$ 包含其他所有候选集合；那是“最大元”，是更强的要求。

我们用到的集合论工具通常叫 Zorn 引理，也叫 Kuratowski–Zorn 引理：

如果非空偏序集中的每条链都在该偏序集中有一个上界，那么它有极大元。

链是其中任意两个元素都可比较的子集。上界必须属于原来的偏序集，但不必属于那条链。这个区别在课间的提问中又被确认了一次：证明候选集合族中的链有上界，不能只在更大的环境里随便找一个上界。

一般形式的极大元引理与选择公理等价。选择公理说：给定一族非空集合，可以为每个集合同时选出一个元素。有限个集合的选择通常不会使我们惊讶；无限多次、没有明确选取规则的选择，会带来更特别的结果。我们暂时插入一个帽子问题，说明它的力量。

可数多个囚犯，可以保证只有有限个人猜错吗

设囚犯按自然数编号，每个人戴黑帽或白帽，可以看见所有其他人的帽子，却看不见自己的帽子。他们能事先商定策略，之后每个人根据所见独立猜自己的颜色。要求并不是一个都不猜错，而是：不管帽子怎样分配，错误总数必须有限。

把一次完整分配写成二进制序列

$$x=(x_1,x_2,\ldots)\in\{0,1\}^{\mathbb N}.$$

定义等价关系

$$x\sim y \iff \{n:x_n\ne y_n\}\text{ 是有限集}.$$

也就是说，两种分配只在有限多个位置不同，就属于同一类。利用选择公理，为每个等价类 $[x]$ 预先选定一份代表 $r([x])$，全体囚犯共享这套约定。

第 $n$ 个囚犯不知道 $x_n$，但他能确定真实分配的等价类：把自己未知的帽子补成黑色或白色，所得两份完整序列至多在第 $n$ 位不同，所以一定同类。他就猜代表的第 $n$ 位 $r([x])_n$。所有人确定的是同一等价类，因此使用同一份代表；而代表与真实序列只有有限处不同，正好保证仅有限个人猜错。

这里并没有给出一个可以写成有限程序的代表选取规则。这套共同约定可能需要一个极其庞大的“本子”。可数序列的全部分配不可数；每个等价类却可数，因为相对于固定序列，每份同类序列由一个有限改动集决定，而自然数的有限子集只有可数多个。因此等价类也不可能只有可数多个。这一计数不是策略成立的必要步骤，但提醒我们：选择公理允许的“事先约定”，比日常有限算法强得多。

我们还提到了 Banach–Tarski 悖论：在适当的集合论前提下，可以把一个三维球分成有限个集合，再通过刚体运动重组成两个同样大的球。帽子例子用的对象更简单，所以在这里更容易看出选择公理带来的非直观结果。

可数偏序集中的极大元：把一般引理缩小来看

这不是集合论课，我们不证明一般的 Zorn 引理，但可以解释可数情形。设非空偏序集 $X=\{x_1,x_2,\ldots\}$ 中每条链都有上界。先取 $y_1=x_1$，从 $n=2$ 起依次检查 $x_n$：如果 $y_{n-1}<x_n$，就令 $y_n=x_n$；否则保持 $y_n=y_{n-1}$。于是

$$y_1\le y_2\le y_3\le\cdots$$

是一条链，因而有上界 $u\in X$。如果还有 $z>u$，它必定是枚举中的某个 $x_k$。检查到它时，$y_{k-1}\le u<z$，算法就会把 $z$ 选入链；但 $u$ 又是全链的上界，这与 $z>u$ 矛盾。因此 $u$ 已经是极大元。

这个论证也说明，不能只是说“不断往上走，最后就停了”；必须使用链存在上界的假设和枚举穷尽所有候选的事实。一般不可数情形需要更广义的枚举和集合论论证。还要注意：可数语言的所有公式虽可数，公式的任意子集组成的集合族通常不可数。因此下面若在候选集合族上直接引用 Zorn 引理，用的是一般形式；若希望完全使用逐步构造，则可以直接枚举语言中的对象，后一种写法我们稍后再解释。

4. 经典完备性：极大扩张必须保持“不推出目标公式”

现在回到 $\Gamma\nvdash_{\mathrm C}\varphi$。我们要找一个比 $\Gamma$ 信息更多、但仍不能证明 $\varphi$ 的集合。具体考虑

$$\mathcal X= \{\Sigma:\Gamma\subseteq\Sigma, \ \Sigma\nvdash_{\mathrm C}\varphi\},$$

按包含关系排序。这个集合族非空，因为 $\Gamma\in\mathcal X$。

这里需要把课堂后半段的现场修正带进来：极大性的限制不是单纯“一致”，而是“不推出这一个指定的 $\varphi$”。 如果我们只取一个包含 $\Gamma$ 的极大一致集合，它有可能已经证明了 $\varphi$，就无法产生我们需要的反模型。后面所有“不能再加”的话，都应理解为“再加就会推出 $\varphi$”。

第一步：链的并仍然避开 $\varphi$

取 $\mathcal X$ 中任意一条链 $\mathcal C$，令

$$\Sigma^*=\bigcup_{\Sigma\in\mathcal C}\Sigma.$$

它显然包含 $\Gamma$。如果 $\Sigma^*\vdash_{\mathrm C}\varphi$，一份证明只使用有限多个假设 $\theta_1,\ldots,\theta_m$。每个假设来自链中的某个集合；由于链中各集合可以比较，包含这有限多个假设的若干集合里有一个包含其余所有集合。因此某个 $\Sigma\in\mathcal C$ 已经含有全部证明前提，进而 $\Sigma\vdash_{\mathrm C}\varphi$，与候选条件矛盾。

所以 $\Sigma^*\in\mathcal X$，是这条链的上界。空链的上界可以取 $\Gamma$。Zorn 引理给出一个极大候选 $\Delta$，满足

$$\Gamma\subseteq\Delta, \qquad\Delta\nvdash_{\mathrm C}\varphi.$$

“在极限里突然出现一份证明”是不可能的：证明的所有前提有限，早已一起出现在某个阶段。这正是课间问答中对取并步骤的解释。

第二步：$\Delta$ 是理论

如果 $\Delta\vdash_{\mathrm C}\psi$，却 $\psi\notin\Delta$，那么把 $\psi$ 加进去不会增加任何可证结论：凡是用 $\psi$ 作假设的地方，都可以代入它从 $\Delta$ 的证明。因此 $\Delta\cup\{\psi\}$ 仍不推出 $\varphi$，违反极大性。故

$$\Delta\vdash_{\mathrm C}\psi\iff\psi\in\Delta.$$

它也一致：若 $\Delta\vdash_{\mathrm C}\bot$，由爆炸规则就能推出 $\varphi$。这样，极大扩张自动满足我们对理论的两个要求。

第三步：它对每个公式都有决定

我们要证明，对任意 $\psi$，恰有下面两者之一属于 $\Delta$：

$$\psi\in\Delta\quad\text{或}\quad\neg\psi\in\Delta.$$

两者不能同时出现，否则会推出 $\bot$。如果两者都不在 $\Delta$，极大性分别给出

$$\Delta,\psi\vdash_{\mathrm C}\varphi, \qquad \Delta,\neg\psi\vdash_{\mathrm C}\varphi.$$

再使用排中律 $\psi\lor\neg\psi$ 和析取消去，两个分支都得到 $\varphi$，所以 $\Delta\vdash_{\mathrm C}\varphi$，矛盾。这一处正是经典性的作用。

这样的理论叫作完全理论。它对每个公式都表态，而不仅对每个原子表态。请不要把“完全理论”与“证明系统的完备性”混淆；前者是我们构造的集合的性质，后者是语义与可证性之间的对应。

第四步：把完全理论变成赋值

我们现在令

$$v_\Delta(p)=1\iff p\in\Delta.$$

剩下的关键是真值引理：对每个公式 $\psi$，

$$\boxed{v_\Delta\models\psi\iff\psi\in\Delta.}$$

证明对公式结构归纳。原子情形由定义成立，$\bot$ 情形由一致性成立。复合公式的情况，我们把课堂所说的“按规则与完全性检查”展开到可以复算。

对于合取，由引入和消去规则有

$$\alpha\land\beta\in\Delta \iff\alpha\in\Delta\text{ 且 }\beta\in\Delta.$$

归纳假设把右边变成两者都在 $v_\Delta$ 下为真，恰好是合取语义。

对于析取，如果 $\alpha\in\Delta$ 或 $\beta\in\Delta$，就能引入 $\alpha\lor\beta$。反过来，若 $\alpha\lor\beta\in\Delta$，但两者都不在 $\Delta$，完全性给出 $\neg\alpha,\neg\beta\in\Delta$。对析取做分情况讨论，每个分支都推出 $\bot$，违反一致性。因此

$$\alpha\lor\beta\in\Delta \iff\alpha\in\Delta\text{ 或 }\beta\in\Delta,$$

再用归纳假设即可。

对于蕴涵，若 $\alpha\to\beta\in\Delta$，那么 $\alpha\in\Delta$ 时，蕴涵消去必给出 $\beta\in\Delta$。所以不可能出现 $\alpha$ 为真、$\beta$ 为假的赋值情况，$v_\Delta\models\alpha\to\beta$。

反过来，如果 $v_\Delta\models\alpha\to\beta$，经典语义告诉我们 $v_\Delta\not\models\alpha$ 或 $v_\Delta\models\beta$。后一种情况由归纳假设得到 $\beta\in\Delta$，加一个临时假设 $\alpha$，直接保留 $\beta$，再撤销假设得到 $\alpha\to\beta$。前一种情况给出 $\alpha\notin\Delta$，所以 $\neg\alpha\in\Delta$；临时假设 $\alpha$ 后推出 $\bot$，由爆炸规则得到 $\beta$，再撤销 $\alpha$，同样得到 $\alpha\to\beta\in\Delta$。真值引理成立。

由于 $\Gamma\subseteq\Delta$，赋值 $v_\Delta$ 满足 $\Gamma$ 中所有公式；由于 $\Delta\nvdash_{\mathrm C}\varphi$ 且 $\Delta$ 演绎封闭，$\varphi\notin\Delta$，故 $v_\Delta\not\models\varphi$。我们已经构造出了所需的反模型，经典完备性证明完成。

5. 用更直观的语言重述：逐个决定变量

休息后，我们把同一个构造换成更直观的说法。设 $\Gamma\nvdash_{\mathrm C}\varphi$，依次检查原子 $p_1,p_2,\ldots$。面对 $p_1$，问两个问题：加入 $p_1$ 会不会推出 $\varphi$？加入 $\neg p_1$ 会不会推出 $\varphi$？

两边不可能都推出。因为如果

$$\Gamma,p_1\vdash_{\mathrm C}\varphi, \qquad\Gamma,\neg p_1\vdash_{\mathrm C}\varphi,$$

用排中律做分情况讨论就会从 $\Gamma$ 本身推出 $\varphi$。因此至少可以选一边加入，同时保持目标公式不可证。

在已经为 $p_1$ 作出的选择基础上，再为 $p_2$ 作同样选择，如此继续。得到

$$\Gamma=\Gamma_0\subseteq\Gamma_1\subseteq\Gamma_2\subseteq\cdots, \qquad\Gamma_n\nvdash_{\mathrm C}\varphi.$$

每一步给一个原子选择 $p_n$ 或 $\neg p_n$。如果变量有限，若干步后就结束；如果变量可数无限，就取 $\Gamma_\infty=\bigcup_n\Gamma_n$。证明有限性保证它仍不推出 $\varphi$。

现在所有原子都已有选择，因此这些选择给出一份赋值。为了说明它确实满足 $\Gamma$ 并使 $\varphi$ 为假，可以对每个有限公式 $\psi$ 作归纳：$\psi$ 涉及的原子只有限个，选定它们的文字后，就能在经典系统中推出 $\psi$ 或 $\neg\psi$，与该赋值中的真值一致。合取、析取按对应规则处理；蕴涵为真时，要么后件已可证，要么前件的否定已可证，分别使用蕴涵引入或爆炸规则。蕴涵为假时，前件与后件的否定已可证，从而可推出该蕴涵的否定。

若某个 $\theta\in\Gamma$ 在赋值中为假，$\Gamma_\infty$ 就同时推出 $\theta$ 与 $\neg\theta$，进而推出 $\varphi$，矛盾。若 $\varphi$ 为真，上述归纳直接给出 $\Gamma_\infty\vdash\varphi$，也矛盾。因此这也是一个完整的反模型构造。

这里说的“加入一个选择会不会迫使目标成立”，是在问是否可证，不能暗中把它替换成“所有模型是否满足目标”，否则会在证明完备性时预先使用完备性。逐步方法在可数语言中不需要先对公式子集族使用一般的 Zorn 引理；这给出一个存在性构造。

我们也借此说明健全性、完备性不是命题逻辑独有的口号。例如几何中，一方面可以问每幅满足公理的图形是否都满足某个陈述，另一方面可以问是否能从公理和推理规则推出它。形式化工作的中心，就是精确说明语法、模型与推理之间的关系。

6. 紧致性：全局失败一定有有限证据

现在我们解释为什么要允许无限假设。经典完备性与证明有限性合在一起，会给出一个有应用的结论：

$$\boxed{\Gamma\text{ 可满足} \iff\Gamma\text{ 的每个有限子集可满足}.}$$

这叫作命题逻辑的紧致性定理。从左到右显然：一个满足全部公式的赋值，也满足任意部分。反过来，假设 $\Gamma$ 不可满足，那么没有赋值能满足全部假设。于是 $\Gamma\models_{\mathrm C}\bot$，由完备性有 $\Gamma\vdash_{\mathrm C}\bot$。一份矛盾证明只使用有限个假设，所以某个有限 $\Gamma_0\subseteq\Gamma$ 已经推出 $\bot$；由健全性，$\Gamma_0$ 不可满足。这与“每个有限子集可满足”矛盾。

同样，若 $\Gamma\models_{\mathrm C}\varphi$，就存在有限 $\Gamma_0\subseteq\Gamma$ 满足 $\Gamma_0\models_{\mathrm C}\varphi$。不是说 $\Gamma$ 总能整体压缩成一个固定的有限集合；对于不同结论，所需的有限前提可能不同。

用命题公式表达一张地图的着色

设图 $G=(C,E)$ 的顶点是国家或区域，相邻关系是边。我们想用四种颜色给所有顶点着色，使相邻顶点不同色。顶点可以无限。对每个顶点 $c$ 与颜色 $i\in\{1,2,3,4\}$，设原子

$$p_{c,i}=\text{“顶点 }c\text{ 使用颜色 }i\text{”}.$$

对每个 $c$ 加入“至少一种颜色”的约束

$$p_{c,1}\lor p_{c,2}\lor p_{c,3}\lor p_{c,4}.$$

对每条边 $\{c,d\}\in E$ 及每个颜色 $i$，加入

$$\neg(p_{c,i}\land p_{d,i}).$$

它禁止相邻顶点同色。若希望赋值本身严格表示“每个顶点恰有一种颜色”，再对每个 $c$、每对 $i<j$ 加入 $\neg(p_{c,i}\land p_{c,j})$。只用前两类约束也足够提取正确着色：每个顶点从为真的颜色中选编号最小者；相邻顶点不可能选到同一种颜色。课堂编码的核心是“至少一种颜色”与“相邻不能同色”，这里把“恰好一种”的可选条件单列出来，避免混淆。

令 $\Gamma_G$ 为这些约束的集合。如果存在满足全部约束的赋值，就得到全图着色；反过来，一份正确着色也自然给出赋值。

假设 $G$ 的每个有限子图都可以用四种颜色着色。要应用紧致性，我们必须进一步检查：每个有限公式集 $\Gamma_0\subseteq\Gamma_G$ 都可满足。 一份有限约束只出现有限多个顶点，记作 $C_0$。考虑这些顶点以及它们之间所有原图边构成的有限子图。给它作四着色，就满足 $\Gamma_0$ 涉及的所有顶点、边和颜色约束；没有出现的原子可以任意赋值。故每个有限 $\Gamma_0$ 可满足，由紧致性得到满足整个 $\Gamma_G$ 的赋值，即全图四着色。

所以一般结论是

$$\text{每个有限子图可作 }k\text{ 着色} \quad\Longrightarrow\quad \text{整个图可作 }k\text{ 着色},$$

其中 $k$ 是固定的有限正整数。对无限平面图，有限子图仍然平面，有限图的四色定理保证它们四可着色，紧致性再把结论推广到整个无限图。这项应用以有限图的四色定理为前提。

在可数顶点情形，刚才的可数原子语言已够用；任意基数的顶点集则使用相应语言上的一般紧致性与极大扩张论证。逻辑工具所提供的是“若全局失败，就能在有限部分找到失败”，并非一个自动生成着色的有限算法。

7. 回到 Kripke 语义：修正 Peirce 公式的反例

在讨论直觉主义完备性之前，我们先纠正上次对 Peirce 公式反模型的计算。要处理的是

$$\pi=((p\to q)\to p)\to p.$$

它在经典语义中为真，但不一定在 Kripke 模型的每个世界成立。我们用两个世界组成的链

$$w_0\le w_1, \qquad V(w_0)=\varnothing, \qquad V(w_1)=\{p\},$$

其中 $w_1$ 没有严格后继，两个世界都不迫使 $q$。原子赋值满足持久性。

先看末世界 $w_1$。它迫使 $p$，不迫使 $q$，因此

$$w_1\nVdash p\to q.$$

而 $w_1\Vdash(p\to q)\to p$：后件 $p$ 已真；也可以说，在唯一需要检查的世界里，前件 $p\to q$ 没有被迫使。

再看 $w_0$。如果只看当下，$p$ 尚未被迫使，可能会误以为 $p\to q$“前件不真，所以真”。但 Kripke 蕴涵还要看未来，$w_1$ 迫使 $p$ 却不迫使 $q$，正好是反例。因此

$$w_0\nVdash p\to q.$$

现在检查内层蕴涵 $(p\to q)\to p$。在 $w_0$ 和 $w_1$，$p\to q$ 都没有被迫使；所以每个后继中的条件“如果迫使 $p\to q$，则迫使 $p$”都成立，得到

$$w_0\Vdash(p\to q)\to p.$$

但 $w_0\nVdash p$。外层蕴涵在 $w_0$ 本身就出现“前件被迫使、后件未被迫使”的失败，故

$$\boxed{w_0\nVdash((p\to q)\to p)\to p.}$$

完整检查可以记成下面一张表。表中的“未迫使”就是 $\nVdash$，不能直接改写成迫使否定。

这一处纠错的要点就是：蕴涵的判断不能只停在当前世界。 同时，$w_0\nVdash p$ 并不意味着 $w_0\Vdash\neg p$；实际上 $w_1\Vdash p$，所以 $w_0$ 也不迫使 $\neg p$。

8. 直觉主义健全性：同一条规则，检查所有世界

直觉主义健全性仍然是检查每一条规则保持语义真，再对证明归纳。我们在课堂中选了蕴涵消去作代表：

$$\frac{\Gamma\vdash_{\mathrm I}\alpha \qquad\Gamma\vdash_{\mathrm I}\alpha\to\beta} {\Gamma\vdash_{\mathrm I}\beta}.$$

任取一个模型中的世界 $w$，若 $w\Vdash\Gamma$，两个前提的语义正确性给出 $w\Vdash\alpha$ 与 $w\Vdash\alpha\to\beta$。蕴涵虽然要求所有未来都保持条件，但特别包含当前世界 $w$，所以 $w\Vdash\beta$。

为了把健全性的理由补齐，还要注意迫使的持久性：对每个公式 $\theta$，

$$w\le u, w\Vdash\theta\quad\Longrightarrow\quad u\Vdash\theta.$$

它由公式结构归纳得到。原子是模型条件；合取、析取用归纳假设；蕴涵用可达关系的传递性，因为 $u$ 的每个未来也是 $w$ 的未来。$\bot$ 无世界迫使，不产生反例。

因此蕴涵引入也健全：若从 $\Gamma,\alpha$ 的证明得到 $\beta$，取满足 $\Gamma$ 的 $w$，再取任意 $u\ge w$ 且 $u\Vdash\alpha$。持久性保证 $u\Vdash\Gamma$，于是归纳假设给出 $u\Vdash\beta$；这恰好证明 $w\Vdash\alpha\to\beta$。合取规则直接对应语义，析取消去则由当前世界迫使一个实际的析取分支而成立。爆炸规则的前提 $\bot$ 不会在任何世界成立。故

$$\Gamma\vdash_{\mathrm I}\varphi\quad\Longrightarrow\quad \Gamma\models_{\mathrm I}\varphi.$$

排中律不能加到这一论证中，因为它在一般 Kripke 世界不成立。上面的 $w_0$ 既不迫使 $p$，也不迫使 $\neg p$，所以不迫使 $p\lor\neg p$。由健全性，Peirce 公式在直觉主义系统也不可无条件证明。

9. 直觉主义完备性：世界本身是素理论

我们现在又从不可证性出发：假设

$$\Gamma\nvdash_{\mathrm I}\varphi.$$

模型该怎样构造？此刻我们掌握的信息只有哪些公式能证明、哪些不能证明，因此模型的世界自然应该从公式集合或理论中产生。但不能简单照搬经典的完全理论：如果把每个世界都要求成“$\psi$ 或 $\neg\psi$ 必有一个”，就丢掉了直觉主义信息尚未决定的情形。

我们保留一致和演绎封闭，再加一个针对析取的条件：

$$\alpha\lor\beta\in T \quad\Longrightarrow\quad \alpha\in T\text{ 或 }\beta\in T.$$

满足这一条件的直觉主义理论叫素理论，英文是 prime theory。为什么需要它？因为 Kripke 的析取语义就是在当前世界实际迫使某个分支。如果一个世界作为公式集只包含析取、两个分支却都没有，那么“公式属于集合”就无法与“公式在世界被迫使”对应。

这个性质不是每个理论自动具有的。例如从假设 $p\lor\neg p$ 取直觉主义演绎闭包，就得到一个包含该析取的理论，但它既不能推出 $p$，也不能推出 $\neg p$。可以用单世界经典赋值验证：$p$ 假的单世界满足这个假设而不满足 $p$；$p$ 真的单世界满足假设而不满足 $\neg p$，由健全性得到两个不可证结论。假设“二者之一”与已经拥有其中一个分支的信息，确实不是同一件事。

素扩张引理

我们要证明：若 $\Sigma\nvdash_{\mathrm I}\chi$，就有一个素理论 $T$，使

$$\Sigma\subseteq T, \qquad T\nvdash_{\mathrm I}\chi.$$

还是取所有包含 $\Sigma$、却不推出目标 $\chi$ 的公式集，并取极大元。链的并不推出 $\chi$，理由仍是证明只使用有限假设；这个理由不依赖排中律。极大集合 $T$ 也仍然演绎封闭、一致，证明与经典情形相同。

但这次我们不能在证明系统中使用排中律。所需的素性来自普通析取消去：设 $\alpha\lor\beta\in T$，而 $\alpha,\beta$ 都不在 $T$。由极大性，

$$T,\alpha\vdash_{\mathrm I}\chi, \qquad T,\beta\vdash_{\mathrm I}\chi.$$

用已经属于 $T$ 的 $\alpha\lor\beta$ 作分情况讨论，两边都推出 $\chi$，于是 $T\vdash_{\mathrm I}\chi$，矛盾。因此至少一个分支属于 $T$，它就是素理论。

与经典扩张一样，极大性始终以不推出指定目标 $\chi$ 为条件。

典范模型的三个组成部分

令 $W$ 是这套语言中全部素理论的集合。把可达关系定义为包含关系，把原子赋值定义为原子属于理论：

$$T\le U\iff T\subseteq U, \qquad V(T)=\{p:p\in T\}.$$

集合包含是偏序；如果 $T\subseteq U$，在 $T$ 已经为真的原子在 $U$ 仍然属于集合，所以赋值持久性也自动成立。我们已经得到一个 Kripke 模型。

可以把世界理解为目前确立的全部信息。沿着包含关系前进，就是增加信息，同时保留已有信息。课堂也讨论了没有任何额外假设时可证公式所组成的集合 $\operatorname{Cn}_{\mathrm I}(\varnothing)$，把它看成最少信息的候选世界：任何素理论都包含所有这些定理，而它不包含任何原子 $p$，因为单世界中令 $p$ 为假就能用健全性排除 $\vdash_{\mathrm I}p$。这个候选属于 $W$ 还需要直觉主义定理的析取性质；我们构造反模型时直接使用素扩张引理。

10. 真值引理：成员关系怎样变成 Kripke 的真

典范模型的关键仍然是

$$\boxed{T\Vdash\psi\iff\psi\in T} \qquad(T\in W).$$

注意两边来自不同定义：右边是一个公式是否属于集合；左边是 Kripke 语义按公式结构定义的迫使关系。不能因为世界就是公式集，就省掉两者相符的证明。

对公式结构归纳。原子情形由 $V(T)$ 的定义成立。$\bot$ 不属于任何一致理论，也不在任何 Kripke 世界被迫使，两边同时不成立。

合取情形中，语义说 $T$ 同时迫使两个分支。归纳假设把它变成 $\alpha,\beta\in T$；合取引入与演绎封闭给出 $\alpha\land\beta\in T$。反过来，从合取的成员关系用两个合取消去规则得到两个分支，再用归纳假设得到迫使关系。

析取情形的一个方向也直接：如果 $T\Vdash\alpha\lor\beta$，按语义必有 $T\Vdash\alpha$ 或 $T\Vdash\beta$。归纳假设给出至少一个分支属于 $T$，析取引入给出 $\alpha\lor\beta\in T$。反向才用到世界的素性：从 $\alpha\lor\beta\in T$ 得到 $\alpha\in T$ 或 $\beta\in T$，再用归纳假设和析取语义。

素性正是为了这一处设计的。但蕴涵的价格更高：它的语义涉及全部包含 $T$ 的未来世界，不能只在 $T$ 内检查一次蕴涵消去。

编者补全： 当天转写在引出蕴涵关键方向时结束；以下补齐蕴涵两向及完备性收束。

蕴涵的成员关系推出迫使关系

假设 $\alpha\to\beta\in T$。任取 $U\supseteq T$，且 $U\Vdash\alpha$。由归纳假设有 $\alpha\in U$，由包含关系有 $\alpha\to\beta\in U$。蕴涵消去与封闭性给出 $\beta\in U$，再由归纳假设得到 $U\Vdash\beta$。这对每个未来 $U$ 都成立，因此

$$T\Vdash\alpha\to\beta.$$

不属于理论，就构造一个见证失败的未来

反向用逆否。假设 $\alpha\to\beta\notin T$。由于 $T$ 演绎封闭，$T\nvdash_{\mathrm I}\alpha\to\beta$。若 $T,\alpha\vdash_{\mathrm I}\beta$，撤销临时假设 $\alpha$，蕴涵引入会给出 $T\vdash_{\mathrm I}\alpha\to\beta$，矛盾。所以

$$T\cup\{\alpha\}\nvdash_{\mathrm I}\beta.$$

现在对 $\Sigma=T\cup\{\alpha\}$、目标 $\chi=\beta$ 使用素扩张引理，得到素理论 $U$，满足

$$T\subseteq U, \qquad\alpha\in U, \qquad\beta\notin U.$$

它正是典范模型中 $T$ 的一个未来。归纳假设给出 $U\Vdash\alpha$ 与 $U\nVdash\beta$，因此 $U$ 见证了 $T\nVdash\alpha\to\beta$。这就完成蕴涵情形，也完成真值引理。

从真值引理得到反模型

最后对原来的 $\Gamma\nvdash_{\mathrm I}\varphi$ 使用素扩张引理，找到包含 $\Gamma$、却不包含 $\varphi$ 的素理论 $T_0$。由真值引理，

$$T_0\Vdash\Gamma, \qquad T_0\nVdash\varphi.$$

所以 $T_0$ 就是所需的反模型世界。结合健全性，得到直觉主义证明系统与 Kripke 语义的对应。

经典构造中，一个完全理论已经像一份完整真值表；直觉主义构造中，一个素理论只表示当前信息，我们保留全部可能的信息扩张，用它们检验蕴涵。两种模型的不同，正好对应了两种证明系统的不同。

来源与补全说明

依据 2026 年 9 月 21 日两段完整转写与既有回放帧整理，时间均为段内时间。结构归纳、逐变量构造验证及有限约束到有限子图的步骤作了补全；直觉主义蕴涵真值引理与最终收束为编者补全。未取得可确认的配套课件原件。