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.
For any formal language L, extend L by adding the epsilon operator to redefine quantification:
The intended interpretation of εx A is some x that satisfies A, if it exists. In other words, εx A returns some term t such that A(t) is true, otherwise it returns some default or arbitrary term. If more than one term can satisfy A, then any one of these terms (which make A true) can be chosen, non-deterministically. 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.
In tau-square notation from N. Bourbaki's Theory of Sets, the quantifiers are defined as follows:
where A is a relation in L, x is a variable, and juxtaposes a at the front of A, replaces all instances of x with , and links them back to . Then let Y be an assembly, (Y|x)A denotes the replacement of all variables x in A with Y.
Defining quantifiers in this way leads to great inefficiencies. For instance, the expansion of Bourbaki's original definition of the number one, using this notation, has length approximately 4.5 × 1012, and for a later edition of Bourbaki that combined this notation with the Kuratowski definition of ordered pairs, this number grows to approximately 2.4 × 1054.
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.
- "Epsilon Calculi". Internet Encyclopedia of Philosophy.
- Moser, Georg; Richard Zach. The Epsilon Calculus (Tutorial). Berlin: Springer-Verlag. OCLC 108629234.
- Avigad, Jeremy; Zach, Richard (November 27, 2013). "The epsilon calculus". In Zalta, Edward N. Stanford Encyclopedia of Philosophy.
- Bourbaki, N. Theory of Sets. Berlin: Springer-Verlag. ISBN 3-540-22525-0.