Computer Science Logic and 8th Kurt Gödel Colloquium
Georg Moser, Richard Zach: The Epsilon Calculus
Welcome and News
Host Institutions
Calls and Deadlines
Social Program
Location and Venue
Colocated Events
Authors' instructions
Print current pagePrint this page
Hilbert's Epsilon Calculus is based on an extension of the language of predicate logic by a term-forming operator e_x. This operator is governed by the critical axiom
A(t) -> A(e_x (A(x)))
where t is an arbitrary term. Within the epsilon calculus, quantifiers become definable by \exists x A(x) iff A(e_x(A(x))) and \forall x A(x) iff A(e_x (A(x))). (The expression e_x(A(x)) is called an epsilon-term.)

The epsilon calculus was developed in the context of Hilbert's program of consistency proofs. It is of independent interest, however, and a study from a computational and proof-theoretic point of view is worthwhile. As a simple example of the advantages of the epsilon calculus note that by encoding quantifiers on the term-level, formalizing (informal) proofs is sometimes easier in the epsilon calculus, compared to formalizing proofs in, e.g., sequent calculi.

In this tutorial we will restrict our attention to predicate logic. After formally introducing the relevant concepts we present some conservativity results for the epsilon calculus. In particular we will prove the first and second epsilon theorem. As an easy consequence of the first epsilon theorem one obtains: Any consequence F of a finitely axiomatized open theory T, where F is quantifier-free is provable from the axioms of T by the quantifier-free fragment of predicate logic. Another consequence is Herbrand's theorem, while the converse of Herbrand's theorem follows from the second epsilon theorem.

© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-07-13 Valid HTML 4.01! Valid CSS! Debian