代入補題

$\mathcal{M}$ を構造、$s$ を割り当て、$w$ を項とし、$a=w^{\mathcal{M}}[s]$ とおく。

1. 任意の項 $u$ について、$(u[w/x])^{\mathcal{M}}[s]=u^{\mathcal{M}}[s(x\mapsto a)]$。
2. $w$ が論理式 $\varphi$ の中で $x$ に代入可能ならば、$\mathcal{M}\models\varphi[w/x]\,[s]\iff\mathcal{M}\models\varphi[s(x\mapsto a)]$。