A higher-order signature Sigma is a tuple (S, F, P, < ), where S is a set of sorts, < is a preorder on S, F is a family of S -> typed value symbols and P is a family of (S -> )+ typed predicate symbols.
S -> is the least set for which
The associated generalised subsorted signature is Sigma -> = (S -> , TF -> , PF -> , P, < -> , < => ) where the only possibly non-empty sets in TF -> and PF -> are TF\, s = Fs for s e S -> , TF(w -> s)w,s = { apply} and PF(w+s)w,s = { apply} for s e S -> , w e (S -> )+
Sigma sentences are Sigma -> sentences.
Sigma models are Sigma -> models satisfying a collection of extensionality axioms.