Zach, Richard. 2017. “Semantics and Proof Theory of the Epsilon Calculus.” In Logic and Its Applications. ICLA 2017, edited by Sujata Ghosh and Sanjiva Prasad, 27–47. LNCS 10119. Berlin, Heidelberg: Springer. DOI :10.1007/978-3-662-54069-5_4.

The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. The application of this undervalued formalism has been hampered by the absence of well-behaved proof systems on the one hand, and accessible presentations of its theory on the other. One significant early result for the original axiomatic proof system for the 𝜀-calculus is the first epsilon theorem, for which a proof is sketched. The system itself is discussed, also relative to possible semantic interpretations. The problems facing the development of proof-theoretically well-behaved systems are outlined.