满足关系

满足关系 $\mathcal{M},s\models \phi$ 把语法公式、结构解释与变量赋值连接起来。语法树从叶到根获得意义：先在结构和赋值中计算项、检查原子事实，再按真值规则组合联结词；量词则改变某个变量的赋值并遍历论域。句子没有自由变量，其真假因而只依赖结构。

量词次序决定谁可以依赖谁 ​

在通常的自然数结构中，$\mathrm{\forall }x\mathrm{\exists }y(x<y)$ 为真：每当外层选定 $x=n$，内层可以选择 $y=n+1$。反过来的 $\mathrm{\exists }y\mathrm{\forall }x(x<y)$ 为假，因为外层一旦选定 $y=m$，内层就可以取 $x=m$，使 $m<m$ 为假。

区别不在于量词的个数，而在于内层选择是否允许依赖外层选择。对有限论域也可以直接检查：令 $M=\{0,1\}$，关系 $R$ 表示不相等，则每个 $x$ 都有另一个 $y$，却不存在一个 $y$ 与所有 $x$ 都不同。

开放公式、句子与模型 ​

在整数结构中，赋值 $s(x)=2$ 满足 $x+1=3$，赋值 $s(x)=4$ 不满足它。$\mathrm{\exists }x(x+1=3)$ 则为真，且不依赖最初的 $s(x)$：量词会重新寻找允许的赋值。每次更新仅改变 $x$，其他自由变量仍保持原取值。

在自然数上 $\mathrm{\exists }x(x+x=4)$ 为真；若把论域换成只有奇数、但不适当地沿用普通加法，就甚至没有得到合法结构，因为奇数加法不封闭。先确认函数确实从论域的幂映回论域，才能讨论满足关系。

满足关系由外部元语言定义，不自动成为原语言中的真理谓词。对足够强的算术语言，不能要求一个内部谓词无条件准确描述自身所有句子的真值；这正是 Tarski 不可定义性所限制的目标。有限结构逐式求值与这个全局自指要求是不同问题。

一阶结构公理库一阶结构First-order structure · Interpretation为一阶语言中的常元、函数符号和关系符号指定集合上解释的数学结构。给解释，赋值公理库变量赋值Variable assignment把每个变量映射到结构论域元素、供项求值与量词语义使用的函数。给参数，满足关系把它们接到公式上。固定一个带一个自由变量的公式 $\phi (x)$，可取出所有满足它的元素，得到结构中的可定义集合；取多个自由变量便得到可定义关系。关系演算公理库关系演算Relational calculus · Domain relational calculus用一阶公式的满足条件定义关系查询，并以域独立性区分仅依赖数据库事实的查询与依赖外部论域的公式。将这个构造用于有限数据库查询，并进一步要求说明答案是否依赖表外论域；即使输出变量来自已有表，被量化变量也可能引入这种依赖。

语义蕴涵公理库语义蕴涵Semantic entailment所有满足前提集的结构与赋值也满足结论时成立的语义关系。又向外增加一层量化：检查每个满足前提的结构与赋值是否也满足结论。某一个模型满足 $\phi$，不等于 $\phi$ 在所有模型中有效，也不等于已有形式证明。

结构递归同时给出证明方法。在“赋值只需在自由变量上相同”这一性质的量词步骤中，让两个赋值把被量化变量更新为同一个 $a$，再对量词内部公式使用归纳假设即可。这解释了句子真值为什么与初始赋值无关。

把量词步骤中的“选择见证”放到两个结构之间，就得到Ehrenfeucht–Fraïssé 博弈公理库Ehrenfeucht–Fraïssé 博弈Ehrenfeucht–Fraïssé games · Ehrenfeucht-Fraisse games · EF games用有限轮部分同构博弈刻画有界量词秩的一阶不可区分性，并构造有限线性序的应答策略。的证明机制：一边提出见证，另一边应答，使余下的低秩公式仍真值一致。在有限关系签名下，有限轮获胜策略与相应量词秩以内的公式一致性恰好等价；反向需要有限类型的特征公式，而不只是重复满足关系的定义。