代入不可能

φ中のxにtは代入不可能であるとは以下の2条件を満たす変数記号yが存在すること

条件

φは(…∀y(…x…)…)または(…∃y(…x…)…)という形をしている

xはφ中の自由出現

y ∈ Var(t)

φは論理式

xは変数記号

tは項