形式陈述

变量在公式中的一次出现若位于相应量词 $\forall x$$\mathrm{\forall }x$ 或 $\exists x$$\mathrm{\exists }x$ 的作用域内，则该出现被该量词约束；否则自由。自由变量集合递归满足

$$ \mathrm{FV}(\forall x\varphi)=\mathrm{FV}(\varphi)\setminus\{x\}, $$$$\mathrm{FV}(\mathrm{\forall }x\phi )=\mathrm{FV}(\phi )\setminus \{x\},$$

其余联结词取相应并集。公式可同时含同一变量名的自由出现与受约束出现。只改变受约束变量名称且避免捕获的 $\alpha$$\alpha$-重命名不改变语义；句子恰是自由变量集合为空的公式。

直觉

自由变量像公式对外开放的参数，受约束变量只是量词内部的局部名字；作用域决定每次出现由谁控制。

例子与边界

在 $P(x)\land\forall x\,Q(x,y)$$P(x)\wedge \mathrm{\forall }xQ(x,y)$ 中，第一处 x 自由，量词内部 x 受约束，y 自由。$\forall x\,Q(x,y)$$\mathrm{\forall }xQ(x,y)$ 可安全改名为 $\forall z\,Q(z,y)$$\mathrm{\forall }zQ(z,y)$，但若 z 在内部已有自由出现就可能捕获。不能仅看变量字母是否出现在某个量词旁边，必须沿语法树判断作用域。

推论与应用

自由变量决定公式真值依赖哪些赋值，并控制泛化规则、替换、lambda 绑定和数据库查询参数。捕获规避是形式推理与编译器实现的基本正确性要求。

参考资料

• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001，§2.1, scope, free variables, and substitution。
• Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas, Mathematical Logic, 2nd ed., Springer, 1994，Ch. I, free and bound occurrences。