 The axioms of classical quantificational logic with identity include axioms for quantification and axioms for identity. The axioms for quantification include a suitably modified variant of \((\forall 1)\) in addition to \((\forall 2)\) and \((\forall 3)\). The minimal adjustment in \((\forall 1)\) is meant to accommodate the presence of function symbols and individual constants. We call a term \(t\) free for a variable \(x\) if, and only if, no free occurrence of \(x\) lies within the scope of a quantifier \(\forall y\) or \(\exists y\), where \(y\) is a variable which occurs in \(t\). The axiom of universal instantiation, \((\forall 1)\), now reads: