形式陈述

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

$$[[x{]]}_{\mathcal{M},s}=s(x),[[f(t_1,\dots ,t_n){]]}_{\mathcal{M},s}=f^{\mathcal{M}}([[t_1{]]}_{\mathcal{M},s},\dots ,[[t_n{]]}_{\mathcal{M},s}).$$

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

直觉

结构解释固定符号，赋值则临时给自由变量装入论域元素；改变被量化变量的槽位，就能定义量词如何遍历论域。

例子与边界

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

推论与应用

变量赋值使开放公式拥有精确语义，并用于替换引理、参数定义集和量词递归。证明中常用“赋值在自由变量上相同则公式真值相同”的 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。