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.
[1] 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.
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.[2] 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
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.
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.
A theory to be checked for consistency is first embedded in an appropriate epsilon calculus.