3 What is a function space?

Design proposal: Allow any (set isomorphic to a) function space that is closed under definability (i.e. it contains any definable function, and also any function that may defined using other functions in the function space). This is the approach of Henkin [And86].

The advantage is that the model theory can be defined by a reduction to the first-order case, by introducing higher-order types, application operators and stating a family of extensionality axioms. As a consequence, we get the Henkin completeness theorem, i.e. there is a sound and complete calculus.
Alternatives:

1. Always require the full function space. This follows the set-theoretic intuition, but has the disadvantage that we loose completeness of entailment systems/theorem provers, and we have no reduction to first-order logic.
2. Allow arbitrary function spaces that satisfy extensionality. As a consequence, functional terms (even without partial operation symbols) may not denote, because the corresponding function is not available in the model. For example, enriching ordered natural numbers, it would be consistent to write down an axiom stating that all functions are monotone. Since \x.3-x is a non-monotone function, this term does not denote (while the monotonicity axiom would be inconsistent with the current design, which we find more natural).
3. Allow arbitrary function spaces, but the top-level function always stem from the full, unrestricted function space. This exploits the difference of choice 2 in section 1. So we can state that all functions are monotone and still have non-monotone top-level functions. This seemed to be too confusing for us.
4. Allow even function spaces that are not extensional. The advantage is that positive conditional specifications have initial models (note that the extensionality axiom is not positive conditional). But even with the current design proposal, we can get initial models if we additionally add axioms stating that all carriers are term-generated, because the class of reachable extensional models of positive conditional specifications admits initial models [Hax97].