In this paper we re-examine the semantics of classical higher-order
logic with the purpose of clarifying the role of extensionality. To
reach this goal, we distinguish nine classes of higher-order models
with respect to various combinations of Boolean extensionality and
three forms of functional extensionality. Furthermore, we develop a
methodology of abstract consistency methods (by providing the
necessary model existence theorems) needed to analyze completeness of
(machine-oriented) higher-order calculi with respect to these model
classes.