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.

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 ${\displaystyle \tau _{x}(A)}$ juxtaposes a ${\displaystyle \tau }$ at the front of A, replaces all instances of x with ${\displaystyle \square }$, and links them back to ${\displaystyle \tau }$. Then let Y be an assembly, (Y|x)A denotes the replacement of all variables x in A with Y.

...
Wikipedia