Semantics and proof theory of the epsilon calculus

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.

Continue reading