全称实例化的可靠性

我们直接从塔斯基满足语义出发论证,该语义按公式结构递归定义了在一个结构中的真。

由 $\forall$ 的语义子句:$\mathcal{M} \models_s \forall x\, P(x) \iff \text{for every } d \in M,\ \mathcal{M} \models_{s[x \mapsto d]} P(x)$。假设前提 $\mathcal{M} \models_s \forall x\, P(x)$;由此子句,$\mathcal{M} \models_{s[x \mapsto d]} P(x)$ 对每个 $d \in M$ 都成立,毫无例外。

既然该断言对每个 $d \in M$ 都成立,它特别地对 $d = t^{\mathcal{M},s}$(项 $t$ 在赋值 $s$ 下于 $\mathcal{M}$ 中所表示的元素)也成立。代入这个特定的 $d$,得到 $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x)$。

由代入引理(一个把变量赋值与项代入联系起来的标准结果,可对 $P$ 的结构作归纳证明):$\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x) \iff \mathcal{M} \models_s P(t)$,该引理恰好在 $t$ 对 $P(x)$ 中的 $x$ 可代入时成立(即 $t$ 的自由变量不会被意外约束)。应用此引理,把 $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x)$ 转化为 $\mathcal{M} \models_s P(t)$。

由于 $\mathcal{M}$、$s$、$t$ 都是任意的,从 $\forall x\, P(x)$ 到 $P(t)$ 的推理在每个结构、每种赋值下都保真:该规则是可靠的。