The First Epsilon Theorem in Pure Intuitionistic and Intermediate Logics

Matthias Baaz, Richard Zach

Published 2019-07-10Version 1

By adding a $\tau$ operator, versions of Hilbert's $\varepsilon$-calculus can be obtained for intermediate propositional logics including intuitionistic logic. It is well known that such calculi, in contrast to the $\varepsilon$-calculus for classical logic, are not conservative. In particular, any $\varepsilon$-$\tau$ calculus for an intermediate logic proves all classically valid quantifier shift principles. The resulting calculi are however conservative over their propositional fragments. One important result pertaining to the $\varepsilon$-calculus is the first epsilon theorem, which is closely related to Herbrand's theorem for existential formulas. It is shown that finite-valued G\"odel logics have the first epsilon theorem, and no other intermediate logic does. However, there are partial results for other intermediate logics including G\"odel-Dummett logic, the logic of weak excluded middle, and intuitionistic logic.