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
152 ( #32,459 of 58,485 )

Recent downloads (6 months)
10 ( #48,799 of 58,485 )

How can I increase my downloads?

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