一阶替换引理 | Codeboy's Blog

形式陈述

设项 $t$ 可自由替入公式 $\varphi$ 中变量 $x$ 的位置，即替换不会让 $t$ 中由自由与受约束变量区分出的自由变量被 $\varphi$ 的量词意外捕获。则一阶替换引理为

\mathcal M,s\models\varphi[t/x] \quad\Longleftrightarrow\quad \mathcal M,s[x\mapsto\llbracket t\rrbracket_{\mathcal M,s}]\models\varphi.

相应的项版本说明 $\llbracket u[t/x]\rrbracket_{\mathcal M,s}=\llbracket u\rrbracket_{\mathcal M,s[x\mapsto\llbracket t\rrbracket_{\mathcal M,s}]}$ 。证明分别对项和公式结构归纳。量词步骤可把无捕获条件的作用写清楚：设公式为 $\forall y\,\psi$ ，其中 $y\ne x$ 且 $y\notin\mathrm{FV}(t)$ ，记 $c=\llbracket t\rrbracket_{\mathcal M,s}$ 。对任意论域元素 $d$ ，改变 $y$ 的赋值不会改变 $t$ 的值，所以 $\llbracket t\rrbracket_{\mathcal M,s[y\mapsto d]}=c$ ；两个不同变量的更新因此满足

(s[y\mapsto d])[x\mapsto c] =(s[x\mapsto c])[y\mapsto d].

对每个 $d$ 应用归纳假设，再用全称量词的语义，便有

\begin{aligned} \mathcal M,s\models\forall y\,(\psi[t/x]) &\iff \forall d,\ \mathcal M,s[y\mapsto d]\models\psi[t/x]\\ &\iff \forall d,\ \mathcal M,(s[x\mapsto c])[y\mapsto d]\models\psi\\ &\iff \mathcal M,s[x\mapsto c]\models\forall y\,\psi. \end{aligned}

若 $y=x$ ，该量词阻止替换进入其作用域；语义上，全称量化也会重新遍历 $x$ 的所有取值，覆盖先前对 $x$ 的更新。若可能捕获 $t$ 的自由变量，先把绑定变量合法改名为不在 $t$ 中出现的新变量，再用上述步骤；不存在待替换的自由 $x$ 时则无需改变公式。存在量词把同一论证中的“对每个 $d$ ”换成“存在 $d$ ”。

直觉

替换引理精确说明：先在语法中把项 $t$ 代入变量 $x$ ，与先计算 $t$ 在原赋值下的值、再更新赋值的 $x$ 分量，得到相同语义。它是语法操作与模型解释之间的交换律，但前提是替换不改变原有绑定关系；无捕获条件若被省略，自由变量会意外改由量词绑定，语义等式也随之失效。

例子与边界

在 $\forall y\,R(x,y)$ 中把 $f(z)$ 替入 $x$ 是安全的，语义等同于把 $x$ 赋为 $f(z)$ 的当前值；对闭项 $t$ ，其值不依赖赋值，更新还会更简单。危险来自变量捕获。考虑公式 $\exists y\,(x\ne y)$ ：若把自由项 $y$ 直接替入 $x$ ，会得到 $\exists y\,(y\ne y)$ ，原本自由的 $y$ 被量词捕获。正确做法是先把绑定变量改名：

\exists z\,(x\ne z),

再替换为 $\exists z\,(y\ne z)$ 。在两元素论域 $\{0,1\}$ 中，正确结果对每个 $y$ 的赋值都为真，因为总能选另一个元素；被捕获的 $\exists y\,(y\ne y)$ 却恒假。两个结果因此有不同的真值。同样，把项 $y$ 代入 $\exists y\,R(x,y)$ 的 $x$ 前，也必须先重命名受约束的 $y$ 。替换引理中的“项对变量可自由代入”正是排除这种捕获；证明时必须同时跟踪项求值、赋值更新和绑定变量的新鲜性，否则得到的引理就是错误的。

推论与应用

替换引理把一阶句法中的符号替换与变量赋值更新精确对应，是量词规则可靠性的核心技术步骤。它支撑自然演绎中的全称实例化、项模型构造、程序逻辑的赋值公理，以及证明助手中的捕获规避替换；若忽略新鲜变量条件，句法变换便不再保持满足关系。

参考资料

David Marker, Model Theory: An Introduction, Springer, 2002，§1.1, substitution theorem for terms and formulas。
Wilfrid Hodges, Model Theory, Cambridge University Press, 1993，Ch. 1, substitution and satisfaction lemma。

形式陈述 ​

反向链接

形式陈述