自由变量与约束变量

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

自由变量像公式的外部参数，其值由环境赋予；约束变量则是量词或绑定器内部的局部名字。真假是否依赖某个变量，取决于它是否自由出现，而不是字面上是否出现。重命名约束变量不应改变含义，但重命名自由变量会改变公式所表达的参数关系。

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

在 $\mathrm{\forall }xR(x,y)$ 中，$x$ 约束、$y$ 自由；外层再加 $\mathrm{\exists }y$ 后成为句子。公式 $R(x)\wedge \mathrm{\exists }xS(x)$ 中第一个 $x$ 自由，第二个被绑定，同名不代表同一作用域。把自由变量 $y$ 替换为 $x$ 可能被 $\mathrm{\forall }x$ 捕获，因此需先改名。

自由变量决定公式真值依赖哪些赋值，并控制泛化规则、替换、lambda 绑定和数据库查询参数。捕获规避是形式推理与编译器实现的基本正确性要求；程序语言中更一般的绑定器—作用域—出现关系见变量绑定公理库变量绑定Variable binding · Binding occurrence把变量的使用出现关联到作用域内声明，并区分自由出现、绑定出现与遮蔽。。

变量赋值公理库变量赋值Variable assignment把自由变量映射到结构论域元素的函数。只需为自由变量提供值，句子的真假与赋值无关。替换引理公理库一阶替换引理Substitution lemma for first-order logic语法上的无捕获项替换与语义上的变量赋值更新相一致。精确处理无捕获代入，量词规则、λ 演算公理库λ 演算Lambda calculus · Untyped lambda calculus以变量、抽象、应用和 β-归约表达高阶函数计算的无类型核心演算。和程序作用域也共享这一绑定结构。