
Hilbert's Epsilon Calculus
is based on an extension of the language
of predicate logic by a termforming 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 epsilonterm.)
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 prooftheoretic point of
view is worthwhile.
As a simple example of the advantages of the epsilon calculus
note that by encoding quantifiers on the termlevel,
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 quantifierfree is provable from
the axioms of T by the quantifierfree fragment of
predicate logic. Another consequence is Herbrand's theorem,
while the converse of Herbrand's theorem follows from
the second epsilon theorem.
© 20022003 Kurt Gödel Society, Norbert Preining. 
20030713
 