 IF first-order logic is an extension of first-order logic. Now, any first-order formula is equivalent to a first-order formula in which no variable occurs both free and bound, and in which no two nested quantifiers carry the same variable. Formulas meeting these two syntactic conditions will be termed regular. Henceforth we systematically restrict attention to regular first-order  formulas.[17]  A vocabulary (signature, non-logical terminology) is any countable set \(\tau\) of relation symbols (each of which carries a fixed arity), function symbols (again each with a fixed arity), and constant symbols. The first-order logic of vocabulary \(\tau\) will be referred to as \(\mathbf{FO}[\tau]\). It is assumed here that among the logical symbols of first-order logic there is the identity symbol (=). The identity symbol is syntactically a binary relation symbol, but its semantic interpretation is fixed in a way that the interpretations of the items in the non-logical terminology are not.