代替规则

设 $A$ 为一公式, 将 $A$ 中某个个体变项的所有自由出现用 $A$ 中未曾出现过的个体变项符号替代, 其他部分不变, 则 $A^{\prime }\iff A$.