形式陈述

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

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

相应的项版本说明 $\llbracket u[t/x]\rrbracket_{\mathcal M,s}=\llbracket u\rrbracket_{\mathcal M,s[x\mapsto\llbracket t\rrbracket_{\mathcal M,s}]}$$[[u[t/x]{]]}_{\mathcal{M},s}=[[u{]]}_{\mathcal{M},s[x\mapsto [[t{]]}_{\mathcal{M},s}]}$。证明分别对项和公式结构归纳，量词步骤正是自由替入条件发挥作用之处。

直觉

先在语法中用项替换变量，与先计算该项的值再在赋值环境中更新变量，得到相同语义；前提是替换不改变原有绑定关系。

例子与边界

在 $\forall y\,R(x,y)$$\mathrm{\forall }yR(x,y)$ 中把 $f(z)$$f(z)$ 替入 x 是安全的，语义等同于把 x 赋为 $f(z)$$f(z)$ 的当前值。把项 y 直接替入 $\exists y\,R(x,y)$$\mathrm{\exists }yR(x,y)$ 的 x 会使原本自由的 y 被量词捕获；应先把受约束 y 改名。省略捕获条件会得到错误引理。对闭项 t，由于其值不依赖 s，更新更简单。

推论与应用

替换引理连接语法操作与 Tarski 语义，是量词实例化可靠性、项模型、程序逻辑赋值公理和形式化证明器 substitution 实现的核心。

参考资料

• 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。