   Go backward to 1.2 Models
Go up to 1 Basic Concepts
Go forward to 1.4 Satisfaction

## 1.3 Sentences

The  many-sorted terms on a signature Sigma=(S,TF,PF,P) and a set of sorted, non-overloaded variables X are built from:

• variables from X;
• applications of qualified function symbols in TF u PF to argument terms of appropriate sorts.
We refer to such terms as  fully-qualified terms, to avoid confusion with the terms of the language considered in Chapter 2, which allow the omission of qualifications and explicit sorts when these are unambiguously determined by the context.

For a many-sorted signature Sigma= (S,TF,PF,P) the  many-sorted sentences in Sen(Sigma) are the usual closed many-sorted first-order logic formulae, built from atomic formulae using quantification (over sorted variables) and logical connectives. An inner quantification over a variable makes a hole in the scope of an outer quantification over the same variable, regardless of the sorts of the variables. Implication may be taken as primitive [CHANGED:] (in the presence of an always-false formula), [] the other connectives being regarded as derived.

The  atomic formulae are:

• applications of qualified predicate symbols p e P to argument terms of appropriate sorts;
• assertions about the definedness of fully-qualified terms;
• existential and strong equations between fully-qualified terms of the same sort.
Definedness assertions may be derived from existential equations using conjunction, or regarded as applications of fixed predicates. Strong equations may be derived from existential equations, using [CHANGED:] implication and conjunction; existential equations may be derived from conjunctions of [] strong equations and definedness assertions, or regarded as applications of fixed predicates.

The sentences Sen(Sigma) also include  sort-generation constraints. Let Sigma=(S,TF,PF, P). A sort-generation constraint consists of (S',F') with S' c S and F' c TF u PF. 4

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