3.4 Expansions to an underlying logic

The choice of the notion of higher-order signatures is almost fixed by the choice taken for the syntax of declarations (see e.g. appendix 4.1), and it should be obvious how CASL declarative constructs determine fragments of a higher-order signature.

Hence, the major questions are:

1. what are the notions of higher-order sentences and models,
2. how are CASL formulas expanded to higher-order sentences

One possibility could be to do the following:

1. Generalise the subsorted logic used so far to a generalised subsorted logic using two subsort relations, one which is a subrelation of the other, to distinguish between embeddings that are required to be injective (and have inverse projections) and those that are not (and do not have inverse projections). For details, see appendix 4.2.
2. Define higher-order Sigma sentences as generalised subsorted Sigma ^-> sentences, where Sigma ^->
   1. uses the set S ^-> of types as the set of sorts
   2. uses < ^-> and < ^=> as the two subsort relations
   3. has a total constant function with coarity t for each value symbol with type t in Sigma
   4. has an apply function for each function type in S ^->
   Sigma models are Sigma ^-> models satisfying a collection of extensionality axioms (ensuring that carrier sets of functional types become isomorphic to subsets of the corresponding function space). For details, see appendix 4.1.