S-1 -- 1.3 Sentences

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 variables X

[TM,DTS,AT] May variables be overloaded, i.e. can X contain x:s and x:s' with s /= s'? (Probably no, because things like forall x:s. forall x:s'. f(x)=x for f : s -> s' might be confusing. But see later comments about variables below.)

Discharged: Variables may not be overloaded.

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 a later section, which allow the omission of qualifications and explicit sorts when these are unambiguously determined by the context.

An explicitly-sorted term is formed by attaching a sort to a fully-qualified term of that sort.¹

[AH,DTS] I don't see the point of explicitly-sorted terms, as the sort of a fully-qualified term can always be derived. ([TM] This is correct: one can always infer the sort of a fully-qualified term by looking at the (result) sort of the outermost function symbol or variable. Transitivity of equality does not fail provided one always works with fully-qualified terms rather than unqualified terms. Therefore it is redundant to use explicitly-sorted terms. It is not necessary to annotate the equality sign with the sort either.)

Discharged: Explicitly-sorted terms are eliminated.

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 using quantification (over sorted variables) and logical connectives from the following atomic formulae:

applications of qualified predicate symbols p e P to argument terms of appropriate sorts;
assertions about the definedness of explicitly-sorted terms;
existential and strong equations between explicitly-sorted terms of the same sort.

[DTS] Assuming that overloading of variables is forbidden (see above): when forall x':s'.phi is a Sigma-formula over X, x' cannot appear in X with any sort other than s', since phi has to be a Sigma-formula over X u {x':s'}! Is this really what we want? And should we additionally require that x':s' / e X? Similarly for other quantifiers.

Discharged: Overloading isn't allowed, but overriding is allowed in quantifications. An inner quantification makes a hole in the scope of an outer quantification of a variable with the same or different sort.

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.

[AT] Translations of sentences along signature morphisms are not defined. I would not attempt this here: first, there would be troubles with constraints; second, we do not need this for the semantics of the language.

Discharged: No change required.

CoFI Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk