The first-order axiom scheme corresponding to the elimination rule for the universal quantifier:

• • $\forall x\phi \to \phi \left[t/x\right]$

Also called universal instantiation. The law of specification is thought to be problematic by supporters of free logic, as is its contrapositive form, the law of particularization. The law of specification, however, is replaced in such contexts with the restricted law of specification:

• • $\left(\forall x\phi \wedge \exists x\left(x=t\right)\right)\to \phi \left[t/x\right]$

which permits one to instantiate a universally quantified formula only on those terms known to exist.