We begin with a careful statement of what we will call the (X, Y, Z)definability theorem.
A relational type is a set X of constant, relation, and function symbols. An X-formula is a formula in the first-order predicate calculus with identity, whose only nonlogical symbols are in X. An X-structure consists of a nonempty domain D together with interpretations of the symbols in X on D. If 6I! is a structure and X is a relational type, then ax is the structure obtained by simply deleting, from a, the interpretations of the nonlogical symbols not in X. We write T /== #, or y /= #, to indicate that every model of T, or y, is a model of #.
The (X, Y)-definability theorem states the following. Let X, Y be disjoint finite relational types, X u Y C 2. Let $ be a Z-formula. Suppose that for all Z-structures GZ, 99 /== #, if GZ?r = g'x then 02 = .!Z?. Then for each constant symbol c E Y, each n-ary relation symbol R E Y, and each function symbol F E Y, there are X-formulas A,(+), &?(*1 ,--.7 xn), and CF(*~ ,.--, *, , x,+~ ) with only the free variables shown, such that # + (xr = c t) &(x1)) & (R(x, ,..., xn) t) B,(x, ,..., xn)) & W 1 ,**-, *,) = x,+1 f-f C&I ,*--, *, , x,+1))*
We will also consider the following weak form of the (X, Y, Z)definability theorem, which we will refer to as the weak (X, Y, Z)-* This research was partially supported by NSFP038823. Our thanks to John Isbell for interesting us in equational theories and for helpful suggestions.