The Epsilon Calculus

Abstract

Hilbert’s ε-calculus [1,2] is based on an extension of the language of predicate logic by a term-forming operator ε _x . This operator is governed by the critical axiom

A(t) →A(εx A(x)),

where t is an arbitrary term. Within the ε-calculus, quantifiers become definable by $\exists x A(x) \Leftrightarrow A(\epsilon{x}{A(x)})$ and $\forall xA(x) \Leftrightarrow A(\epsilon{x}{\lnot A(x)})$. (The expression εx A(x) is called an ε-term.)