2 Reduction to first-order logic

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