 A formula \(\forall x A\) is usually defined to be well-formed in FOL even if \(A\) has no free occurrences of \(x\). Then, of course, \(\forall x A\) is equivalent to \(A\) as well as to \(\exists x A\), and such quantifiers are called vacuous. In order to show that any formula can be rewritten into an equivalent formula that contains only “nextand,” it is sufficient to inspect the following definitions for \(\lnot\), \(\lor\) and \(\forall\) (with suitable variables)—that are due to Schönfinkel.