(例) ∀xP(x) → P(t) (tは自由な項)

∀xP(x)からP(t)を得る規則は、任意の対象について成り立つ全称命題を、項tで具体化する全称除去である。tが自由変数を捕獲せず、議論領域の要素を指すことが前提になる。

仕組みと確認

量化子のスコープと項の自由変数を構文木で確認し、具体例を一つ選んで代入後の式を示す。クエリや汎用関数でも、全体の契約から具体的な入力へ特殊化する操作として対応付けられる。

限界と注意点

逆向きに一例から全称を導けるわけではない。型、スコープ、代入可能性を無視した文字列置換は、変数捕獲や誤った仕様を生む。