We investigate Hilbert’s varepsilon -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 varepsilon -terms. We extend the usual topos semantics for type theories to the varepsilon -operator and prove a completeness theorem. The paper also contains a discussion of the concept of “partially defined‘ varepsilon -term. MSC: 03B15, 03B20, 03G30.

The epsilon substitution method was proposed by D. Hilbert as a tool for consistency proofs. A version for first order predicate logic had been described and proved to terminate in the monograph “Grundlagen der Mathematik”. As far as the author knows, there have been no attempts to extend this approach to the second order case. We discuss possible directions for and obstacles to such extensions.