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
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.