Print this page

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