形式陈述

满足关系 $\mathcal M,s\models\varphi$$\mathcal{M},s\models \phi$ 按公式结构递归定义。原子关系满足当且仅当项值元组属于 $R^{\mathcal M}$$R^{\mathcal{M}}$；等式满足当且仅当两项值相等。联结词按经典真值规则解释，量词满足

$$ \mathcal M,s\models\forall x\varphi \iff \forall a\in M,\ \mathcal M,s[x\mapsto a]\models\varphi, $$$$\mathcal{M},s\models \mathrm{\forall }x\phi ⟺\mathrm{\forall }a\in M,\mathcal{M},s[x\mapsto a]\models \phi ,$$$$ \mathcal M,s\models\exists x\varphi \iff \exists a\in M,\ \mathcal M,s[x\mapsto a]\models\varphi. $$$$\mathcal{M},s\models \mathrm{\exists }x\phi ⟺\mathrm{\exists }a\in M,\mathcal{M},s[x\mapsto a]\models \phi .$$

若 $\varphi$$\phi$ 是句子，真值与 $s$$s$ 无关，写作 $\mathcal M\models\varphi$$\mathcal{M}\models \phi$；结构满足理论 $T$$T$ 表示满足其中每个句子。

直觉

语法树从叶到根获得意义：先在结构和赋值中计算项，再检查原子事实，最后按联结词和遍历论域的量词组合真值。

例子与边界

在自然数结构中，$\exists x(x+x=4)$$\mathrm{\exists }x(x+x=4)$ 为真，而 $\forall x\exists y(x<y)$$\mathrm{\forall }x\mathrm{\exists }y(x<y)$ 也为真。量词顺序不可交换：$\forall x\exists y\,x<y$$\mathrm{\forall }x\mathrm{\exists }yx<y$ 与 $\exists y\forall x\,x<y$$\mathrm{\exists }y\mathrm{\forall }xx<y$ 真值不同。满足关系由外部元语言定义，不是结构内部自动拥有的谓词；Tarski 不可定义性说明足够强结构中一般不能无条件内部定义自身全部真理。

推论与应用

满足关系定义模型、语义蕴涵、可定义集合和初等等价，是模型论所有定理的语义基础。其结构递归也使关于公式的归纳证明成为可能。

参考资料

• David Marker, Model Theory: An Introduction, Springer, 2002，§1.1, truth definition and satisfaction。
• Wilfrid Hodges, Model Theory, Cambridge University Press, 1993，Ch. 1, semantics and satisfaction relation。