If possible, the semantics should be given via a reduction
to first-order logic (see, e.g. [Hax97][Me93]).
This has the advantage
that we can re-use the theory developed
for first-order logic.
Since we are dealing with subsorted partial logic,
we reduce subsorted partial higher-order to
subsorted partial first-order logic^{3}
by using a partial application operator for application of
partial functions, and an application predicate
for application of predicates.

For the current proposal, a reduction to first-order logic is possible, but for extensions like polymorphism, this yet has to be checked.

CoFI Note: L-8 ---- 7 January 1998.

Comments to till@informatik.uni-bremen.de