**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.

Comments to cofi-language@brics.dk