**Go backward to** 1.3 Sentences

**Go up to** 1 Basic Concepts

## 1.4 Satisfaction

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 *s*^{M}. 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 *p*^{M}. 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 *f*^{M}, 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).

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk