变元

定义 在公式 $\forall xA$ 与 $\exists xA$ 中, 称 $x$ 为指导变元, $A$ 为相应量词的辖域.

在 $\forall x$ 和 $\exists x$ 的辖域中, $x$ 的所有出现都称为约束出现; $A$ 中不是约束出现的所有变项都称为自由出现.