自由变量与约束变量

要判断自由还是约束，检查的是变量的每一次出现，而不是给整个字母贴标签。沿语法树从该出现向外走，遇到的最近一个同名量词负责绑定它；若没有这样的量词，它就是对外开放的参数。

自由变量集合给出真值可能依赖的参数范围，并不保证每个参数都实际影响结果。例如 $x=x$ 含自由变量 $x$，却在通常带等号的一阶语义中对任何赋值都真。正确结论是：两个赋值只要在所有自由变量上相同，就一定给出相同真值。

按作用域逐层检查 ​

在 $P(x)\wedge \mathrm{\forall }xQ(x,y)$ 中，第一处 $x$ 自由，右侧 $x$ 受全称量词约束，$y$ 自由。因此整个公式的自由变量集合为 $\{x,y\}$。如果只看“公式里已经有 $\mathrm{\forall }x$”就删掉全部 $x$，会错误地丢掉左侧参数。

嵌套公式 $\mathrm{\forall }x(P(x)\wedge \mathrm{\exists }xQ(x))$ 中，$P(x)$ 的出现由外层量词绑定，$Q(x)$ 的出现由内层绑定。为消除阅读歧义，可以改写成 $\mathrm{\forall }x(P(x)\wedge \mathrm{\exists }zQ(z))$；两个量词原本就允许取不同元素。

捕获会真正改变含义 ​

在整数上，$\mathrm{\forall }x(x<y)$ 把 $y$ 留作参数。若要用项 $x+1$ 替换自由的 $y$，直接写成 $\mathrm{\forall }x(x<x+1)$ 会把代入项里的 $x$ 错误绑定，所得句子为真。安全做法先把原量词改名，再代入，得到 $\mathrm{\forall }z(z<x+1)$；它仍依赖外部 $x$，且对任何整数赋值都假。

两者一个恒真、一个恒假，说明避免变量捕获不是书写偏好，而是保持原参数含义的必要条件。先选一个未被使用的新变量，便能在这里安全进行 $\alpha$-重命名。

同样，$\mathrm{\forall }xR(x,y)$ 在再加外层 $\mathrm{\exists }y$ 后成为句子；增加量词改变了断言的参数接口，不能与仅改约束变量名字混同。

变量赋值公理库变量赋值Variable assignment把每个变量映射到结构论域元素、供项求值与量词语义使用的函数。提供外部参数；没有自由变量的句子，其真假与初始赋值无关。替换引理公理库一阶替换引理Substitution lemma for first-order logic语法上的无捕获项替换与语义上的变量赋值更新相一致。则说明无捕获的语法代入如何对应语义上的赋值更新。

全称引入规则必须检查变量是否自由出现在未撤销的假设中。程序语言的局部变量和λ 演算公理库λ 演算Lambda calculus · Untyped lambda calculus以变量、抽象、应用和 β-归约表达高阶函数计算的无类型核心演算。也面对相同问题，但具体绑定器可能不同；更一般的出现与作用域关系见变量绑定公理库变量绑定Variable binding · Binding occurrence把变量的使用出现关联到作用域内声明，并区分自由出现、绑定出现与遮蔽。。