The Epsilon Calculus with Equality and Herbrand Complexity

Kenji Miyamoto, Georg Moser

Hilbert's epsilon calculus is an extension of elementary or predicate calculus by a term-forming operator $\epsilon$ and initial formulas involving such terms. The fundamental r…