The Epsilon Calculus

摘要

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(ε_xA(x)), where t is an arbitrary term. Within the ε-calculus, quantifiers become definable by xA(x) <=> A(ε_xA(x)) and xA(x) <=> A(ε_x A(x)). (The expression ε_xA(x) is called an ε-term.)