d by an expression, we say that
the expression holds for the tuple or that the tuple satisfies the
expression. The IFF has a lax notion of satisfaction for tuples. For a
tuple to satisfy an expression, or that expression to hold for or
classify that tuple, we only require that the arity of the expression
be a subset of the arity of the tuple and that the restriction of the
tuple to that subset satisfy the expression in the usual sense.
Satisfaction is defined recursively. A model satisfies an expression of
