The Epsilon Calculus

In Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy. The Metaphysics Research Lab, Center for the Study of Language and Information, Stanford University (2008)

Authors
Richard Zach
University of Calgary
Jeremy Avigad
Carnegie Mellon University
Abstract
The epsilon calculus is a logical formalism developed by David Hilbert in the service of his program in the foundations of mathematics. The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. Specifically, in the calculus, a term εx A denotes some x satisfying A(x), if there is one. In Hilbert's Program, the epsilon terms play the role of ideal elements; the aim of Hilbert's finitistic consistency proofs is to give a procedure which removes such terms from a formal proof. The procedures by which this is to be carried out are based on Hilbert's epsilon substitution method. The epsilon calculus, however, has applications in other contexts as well. The first general application of the epsilon calculus was in Hilbert's epsilon theorems, which in turn provide the basis for the first correct proof of Herbrand's theorem. More recently, variants of the epsilon operator have been applied in linguistics and linguistic philosophy to deal with anaphoric pronouns.
Keywords epsilon calculus  indefinite description  proof theory
Categories (categorize this paper)
Reprint years 2013
Options
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: 46,330
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Epsilon Substitution Method for ID1.Toshiyasu Arai - 2003 - Annals of Pure and Applied Logic 121 (2-3):163-208.
Mathematical Logic and Hilbert's & Symbol.A. C. Leisenring - 1969 - London: Macdonald Technical & Scientific.
Update Procedures and the 1-Consistency of Arithmetic.Jeremy Avigad - 2002 - Mathematical Logic Quarterly 48 (1):3-13.

View all 10 references / Add more references

Citations of this work BETA

Notions of Invariance for Abstraction Principles.G. A. Antonelli - 2010 - Philosophia Mathematica 18 (3):276-292.
Hilbert’s Program.Richard Zach - 2003 - In Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy. The Metaphysics Research Lab, Center for the Study of Language and Information, Stanford University.

View all 8 citations / Add more citations

Similar books and articles

Epsilon Calculi.Barry Slater - 2006 - Logic Journal of the IGPL 14 (4):535-590.
Cut Elimination for a Simple Formulation of Epsilon Calculus.Grigori Mints - 2008 - Annals of Pure and Applied Logic 152 (1):148-160.
The Epsilon Calculus and its Applications.B. H. Slater - 1991 - Grazer Philosophische Studien 41:175-205.
Epsilon Calculi.Hartley Slater - 2001 - Internet Encyclopedia of Philosophy.
Creature Forcing and Large Continuum: The Joy of Halving.Jakob Kellner & Saharon Shelah - 2012 - Archive for Mathematical Logic 51 (1-2):49-70.
The Epsilon Calculus' Problematic.B. H. Slater - 1994 - Philosophical Papers 23 (3):217-242.
Exact Bounds on Epsilon Processes.Toshiyasu Arai - 2011 - Archive for Mathematical Logic 50 (3-4):445-458.
Heyting Predicate Calculus with Epsilon Symbol.Grigori Efroimovich Mints - 1977 - Journal of Soviet Mathematics 8 (3):317--323.
Intuitionistic Predicate Calculus with ^|^Epsilon;-Symbol.Kokio Shirai - 1971 - Annals of the Japan Association for Philosophy of Science 4 (1):49-67.
Epsilon Substitution for Transfinite Induction.Henry Towsner - 2004 - Archive for Mathematical Logic 44 (4):397-412.

Analytics

Added to PP index
2009-01-28

Total views
60 ( #146,659 of 2,285,999 )

Recent downloads (6 months)
6 ( #196,884 of 2,285,999 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature