The Epsilon Calculus and Herbrand Complexity

Studia Logica 82 (1):133-155 (2006)
  Copy   BIBTEX

Abstract

Hilbert's ε-calculus is based on an extension of the language of predicate logic by a term-forming operator εx. 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.

Author's Profile

Richard Zach
University of Calgary

Analytics

Added to PP
2009-01-28

Downloads
544 (#43,352)

6 months
124 (#37,060)

Historical graph of downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.
How can I increase my downloads?