Epsilon calculus

Hilbert's epsilon calculus is an extension of a formal language by the epsilon operator, where the epsilon operator substitutes for quantifiers in that language as a method leading to a proof of consistency for the extended formal language. The "epsilon operator" and "epsilon substitution method" are typically applied to a first-order predicate calculus, followed by a showing of consistency. The epsilon-extended calculus is further extended and generalized to cover those mathematical objects, classes, and categories for which there is a desire to show consistency, building on previously-shown consistency at earlier levels. [Stanford, overview paragraphs]

Epsilon operator

For any formal language L, extend L by adding the epsilon operator to redefine quantification:

*$exists\; x\; A(x)\; equiv\; A(epsilon\; x\; A)$

*$forall\; x\; A(x)\; equiv\; A(epsilon\; x\; (\; eg\; A))$

The intended interpretation of ε"x" "A" is "some x" that satisfies "A". Equality is required to be defined under L, and the only rules required for L extended by the epsilon operator are modus ponens and the substitution of "A"("t") to replace "A"("x") for any term "t". [Stanford, the epsilon calculus paragraphs]

Modern approaches

Hilbert's Program for mathematics was to justify those formal systems as consistent in relation to constructive or semi-constructive systems. While Gödel's results on incompleteness mooted Hilbert's Program to a great extent, modern researchers find the epsilon calculus to provide alternatives for approaching proofs of systemic consistency as described in the epsilon substitution method.

Epsilon substitution method

A theory to be checked for consistency is first embedded in an appropriate epsilon calculus. Second, a process is developed for re-writing quantified theorems to be expressed in terms of epsilon operations via the epsilon substitution method. Finally, the process must be shown to normalize the re-writing process, so that the re-written theorems satisfy the axioms of the theory. [Stanford, more recent developments paragraphs]

References

*cite book | last = Moser | first = G. | coauthors = R. Zach | title = The Epsilon Calculus (Tutorial) | location = Berlin | publisher = Spring-Verlag | oclc = 108629234

*Stanford Encyclopedia of Philosophy (online). [http://plato.stanford.edu/entries/epsilon-calculus/ "The Epsilon Calculus"]

Notes