Remark

One can go further in this direction and use quantification inside other terms. To formalize this idea, the notion of terms can be redefined as follows:

• A variable v is a term.
• If f is an r-ary function name and are terms, then f() is a term. The new term is Boolean if f is a relation name.
• Boolean terms are closed under the Boolean operations and quantification, and every Boolean term is a term.