  In this paper we define intensional models for the classical theory of types,
thus arriving at an intensional type logic ITL. Intensional models generalize
Henkin's general models and have a natural definition. As a class they do not
validate the axiom of Extensionality. We give a cut-free sequent calculus for
type theory and show completeness of this calculus with respect to the class of
intensional models via a model existence theorem. After this we turn our
attention to applications. Firstly, it is argued that, since ITL is truly
intensional, it can be used to model ascriptions of propositional attitude
without predicting logical omniscience. In order to illustrate this a small
fragment of English is defined and provided with an ITL semantics. Secondly, it
is shown that ITL models contain certain objects that can be identified with
possible worlds. Essential elements of modal logic become available within
classical type theory once the axiom of Extensionality is given up.
