变量赋值 | Codeboy's Blog

形式陈述

对$L$-结构 $\mathcal M$ ，变量赋值是函数 $s:\mathrm{Var}\to M$ 。项的值递归定义：

\llbracket x\rrbracket_{\mathcal M,s}=s(x),\qquad \llbracket f(t_1,\ldots,t_n)\rrbracket_{\mathcal M,s} =f^{\mathcal M}(\llbracket t_1\rrbracket_{\mathcal M,s},\ldots,\llbracket t_n\rrbracket_{\mathcal M,s}).

$s[x\mapsto a]$ 表示只把变量 $x$ 改赋为 $a$ 的赋值。项值只依赖其中实际出现的变量；闭项不依赖 $s$ 。

直觉

变量赋值把公式中的自由变量映到结构论域中的具体元素。它与结构分工明确：结构固定解释常元、函数和关系符号，赋值只临时给变量装入论域元素；量词求值则通过修改某个变量的槽位来遍历论域。只有自由变量会让公式真假依赖赋值。

例子与边界

在整数结构中，若 $s(x)=2,s(y)=3$ ，则项 $x+y$ 的值为 5。计算 $\forall x\varphi$ 时保持其他变量不变，让 $s[x\mapsto a]$ 遍历所有整数 a。变量名本身不是论域元素； $s(x)$ 与结构中的常元 $c^{\mathcal M}$ 来源不同。对句子，任何两个赋值给出相同真值。

赋值只作用于自由出现，量词会临时覆盖同名变量。设论域为整数， $s(x)=2,s(y)=5$ ，考虑

\varphi\equiv (x<y)\land\exists x\,(x=y+1).

第一处 $x$ 是自由的，按 $s(x)=2$ 解释；量词内部的 $x$ 则遍历整数，可取 $6$ 使第二个合取式为真，因此 $\mathcal M,s\models\varphi$ 。改变 $s(x)$ 可能改变第一部分，却不会改变量词内部的绑定出现；这也是替换时必须区分自由变量与受约束变量的语义原因。

推论与应用

满足关系通过赋值让开放公式获得精确语义，替换引理把赋值更新与语法代入对应；参数定义集和量词递归也依赖它。证明中常用 coincidence lemma：若两个赋值在公式的自由变量上相同，公式真值也相同。程序语义中的环境、λ 演算中的变量解释与约束求解同样复用这一概念。

参考资料

David Marker, Model Theory: An Introduction, Springer, 2002，§1.1, variable assignments and term evaluation。
Wilfrid Hodges, Model Theory, Cambridge University Press, 1993，Ch. 1, valuations of variables and terms。

形式陈述 ​

反向链接

形式陈述