> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/600-toc/620-formal-language-theory/epsilon-calculus.md).

# 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.