新しい定数の変数化

$L'$ を言語 $L$ に定数記号の集合 $C$ を加えた言語とする。

1. $\Gamma$ を $L$ の文の集合、$\varphi$ を $L$ の論理式とする。$\Gamma$ から $L'$ で $\varphi$ が導出できるならば、$L$ で導出できる。特に、$\Gamma$ が $L$ で無矛盾ならば $L'$ でも無矛盾。
2. $\Gamma$ を $L'$ の文の集合、$\varphi$ を $L'$ の論理式、$c$ を $L'$ の定数記号とし、$c$ は $\Gamma$ にも $\varphi$ にも現れないとする。$\Gamma\vdash\varphi[c/x]$ ならば $\Gamma\vdash\forall x\,\varphi$。