The Epsilon Calculus and Herbrand Complexity

Studia Logica 82 (1):133-155 (2006)
Download Edit this record How to cite View on PhilPapers
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.
PhilPapers/Archive ID
MOSTEC-3
Upload history
Archival date: 2017-08-13
View other versions
Added to PP index
2009-01-28

Total views
128 ( #30,844 of 52,683 )

Recent downloads (6 months)
19 ( #31,009 of 52,683 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.