[SCL] satisfaction

[Robert E. Kent]

The constraints on (abstract) vocabularies are those necessary to define
(abstract) interpretations. The constraints on (abstract) interpretations
incorporate those in column three of the interpretation table in the SCL
document from the top row up to and including the row for atoms.

For any name-set N, any vocabulary V, and any interpretation I, a name map A
on a subset of names S is a map A : S --> U. Define IA to be the
interpretation recursively defined from a base component that is A on names
in S and I otherwise.

When the (concrete) vocabulary of a text T is bounded by the vocabulary of
an interpretation I, then I is called a legal interpretation of T.
We use the notation I |= s to denote that sentence s is true in
interpretation I. We also say that I satisfies s.

-------------
Satisfaction:
-------------

For any name-set N, let I = (U, int, rel, fun, relation, function) be any
N-interpretation. Let int* denote the extension of int to sequences. We
assume that I is a legal interpretation of any text to be evaluated. We
temporarily ignore sequence variables.

Atoms:
I |= (= t1 t2) iff int(t1) = int(t2).
I |= (r seq) iff rel(r) contains int*(seq).

Boolean Sentence:
I |= (not s) iff not I |= s.
I |= (and).
I |= (and s) iff I |= s.
I |= (and s1 s2 ... sn) iff I |= s1 and I |= (s2 ... sn).
I |= (or s1 ... sn) iff I |= (not (and (not s1) ... (not sn))).
I |= (implies s1 s2) iff I |= (or (not s1) s2).
I |= (iff s1 s2) iff I |= (implies s1 s2) and I |= (implies s2 s1).

Quantified Sentence:
I |= (forall (var) body) iff IA |= body for every name map A on {var}.
I |= (exists (var) body) iff I |= (not (forall (var) (not body))).

Text:
I |= {}.
I |= {s} iff I |= s.
I |= {s1, s2, ... sn} iff I |= s1 and I |= {s2, ... sn}.


Robert E. Kent
rekent at ontologos.org