Epsilon calculus

https://en.wikipedia.org/wiki/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.