The satisfaction of a sentence in a structure M is determined as usual by the holding of its atomic formulae w.r.t. assignments of (defined) values to all the variables that occur in them, the values assigned to variables of sort s being in sM. The value of a term w.r.t. a variable assignment may be undefined, due to the application of a partial function during the evaluation of the term. Note, however, that the satisfaction of sentences is 2-valued [CHANGED:] (as is the holding of open formulae with respect to variable assignments). []
The application of a predicate symbol p to a sequence of argument terms holds in M iff the values of all the terms are defined and give a tuple belonging to pM. A definedness assertion concerning a term holds iff the value of the term is defined (thus it corresponds to the application of a constantly-true unary predicate to the term). An existential equation holds iff the values of both terms are defined and identical, whereas a strong equation holds also when the values of both terms are undefined.
The value of an occurrence of a variable in a term is that provided by the given variable assignment. The value of the application of a function symbol f to a sequence of argument terms is defined only if the values of all the argument terms are defined and give a tuple in the domain of definedness of fM, and then it is the associated result value.
A sort-generation constraint (S',F') is satisfied in a Sigma-model M if the carriers of the sorts in S' are generated by the function symbols in F'. I.e., every element of each sort in S' is the value of a term built from just these symbols (possibly using variables of sorts not in S', with appropriate assignments of values to them).