Hilbert's ϵ-operator in intuitionistic type theories

We investigate Hilbert's ?-calculus in the context of intuitionistic type theories, that is, within certain systems of intuitionistic higher-order logic. We determine the additional deductive strength conferred on an intuitionistic type theory by the adjunction of closed ?-terms. We extend the usual topos semantics for type theories to the ?-operator and prove a completeness theorem. The paper also contains a discussion of the concept of “partially defined” ?-term. MSC: 03B15, 03B20, 03G30.