Hilbert’s varepsilon -operator in intuitionistic type theories

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

John L. Bell
Western University
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

Our Archive

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

References found in this work BETA

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
24 ( #348,655 of 2,253,757 )

Recent downloads (6 months)
10 ( #126,659 of 2,253,757 )

How can I increase my downloads?


Sorry, there are not enough data points to plot this chart.

My notes

Sign in to use this feature