The Epsilon Calculus and Herbrand Complexity

Georg Moser and Richard Zach

Studia Logica 82(1), pp. 133 – 155, 2006.


Hilbert’s ε-calculus is based on an extension of the language of predicate logic by a term-forming operator ex. Two fundamental results about the ε-calculus, the first and second epsilon theorem, play a rôle similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand’s Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential theorems obtained by this elimination procedure.


  PDF |    doi:10.1007/s11225-006-6610-7  |  © Springer


author = "Georg Moser and Richard Zach",
title = "The Epsilon Calculus and Herbrand Complexity",
journal = "Studia Logica",
volume = 82,
number = 1,
year = 2006,
pages = "133--155"
Nach oben scrollen