Mathematical Logic Quarterly 39 (1):323--337 (1993)

John L. Bell
University of Western Ontario
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.
Keywords ψ -calculus   Intuitionistic type theories
Categories (categorize this paper)
DOI 10.1002/malq.19930390137
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 59,058
Through your library

References found in this work BETA

Mathematical Logic and Hilbert's & Symbol.A. C. Leisenring - 1969 - London: Macdonald Technical & Scientific.
Toposes and Local Set Theories. An Introduction.J. L. Bell - 1990 - Journal of Symbolic Logic 55 (2):886-887.
Topos Theory.P. T. Johnstone - 1982 - Journal of Symbolic Logic 47 (2):448-450.

Add more references

Citations of this work BETA

Hilberts Logik. Von der Axiomatik zur Beweistheorie.Volker Peckhaus - 1995 - NTM Zeitschrift für Geschichte der Wissenschaften, Technik und Medizin 3 (1):65-86.

Add more citations

Similar books and articles

An Overview of Type Theories.Nino Guallart - 2015 - Axiomathes 25 (1):61-77.
An Intuitionistic Version of Cantor's Theorem.Dario Maguolo & Silvio Valentini - 1996 - Mathematical Logic Quarterly 42 (1):446-448.
Intuitionistic Completeness of First-Order Logic.Robert Constable & Mark Bickford - 2014 - Annals of Pure and Applied Logic 165 (1):164-198.
Intuitionistic Ε- and Τ-Calculi.David Devidi - 1995 - Mathematical Logic Quarterly 41 (4):523-546.
Axiomatizations of Intuitionistic Double Negation.Milan Bozic & Kosta Došen - 1983 - Bulletin of the Section of Logic 12 (2):99-102.
Opérateurs de Mise En Mémoire Et Traduction de Gödel.Jean-Louis Krivine - 1990 - Archive for Mathematical Logic 30 (4):241-267.
A General Type for Storage Operators.Karim Nour - 1995 - Mathematical Logic Quarterly 41 (4):505-514.
Intuitionistic Completeness for First Order Classical Logic.Stefano Berardi - 1999 - Journal of Symbolic Logic 64 (1):304-312.


Added to PP index

Total views
32 ( #328,651 of 2,427,679 )

Recent downloads (6 months)
2 ( #329,204 of 2,427,679 )

How can I increase my downloads?


My notes