一阶替换引理 | 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}]}$ 。证明分别对项和公式结构归纳，量词步骤正是自由替入条件发挥作用之处。

直觉

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

例子与边界

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

\forall z\,(x\ne z),

再替换为 $\forall z\,(y\ne z)$ 。同样，把项 $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。

形式陈述 ​

反向链接

形式陈述