Premium
Hilbert's ϵ‐operator in intuitionistic type theories
Author(s) -
Bell John L.
Publication year - 1993
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19930390137
Subject(s) - mathematics , type theory , intuitionistic logic , adjunction , type (biology) , operator (biology) , kripke semantics , topos theory , completeness (order theory) , gödel's completeness theorem , term (time) , algebra over a field , calculus (dental) , pure mathematics , discrete mathematics , linear logic , intermediate logic , computer science , mathematical analysis , theoretical computer science , gene , art , dentistry , repressor , ecology , chemistry , literature , biology , biochemistry , quantum mechanics , transcription factor , medicine , physics , description logic
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.