Epsilon calculus

Epsilon calculus, also known as epsilon substitution or epsilon calculus of constructions, is a formal system and a framework within mathematical logic and particularly in the foundation of mathematics. It extends first-order logic by incorporating a special operator, usually denoted by the Greek letter epsilon (ε), which is used to express the idea of "the witness" or "the choice" in logical statements. The central idea in epsilon calculus is to allow assertions involving existence to be represented in a more constructive way.