全称例化の健全性

構造における真理性を論理式の構造に関する帰納で定義するタルスキの充足意味論から直接論じる。

$\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)$ への推論はすべての構造・すべての付値において真理性を保存する。すなわちこの規則は健全である。