Epsilon Theorems in Intermediate Logics

TL;DR

This paper extends epsilon-calculus to intermediate logics, demonstrating conservativity and the conditions under which epsilon-theorems hold, with implications for arithmetic theories.

Contribution

It generalizes epsilon-theorems to intermediate logics, including G"odel-Dummett logic, and explores their applicability beyond classical logic.

Findings

Conservativity holds for intermediate epsilon-tau calculi.

Extended epsilon-theorem holds in finite-valued G"odel logic.

Second epsilon-theorem holds in finite-valued G"odel first-order logic.

Abstract

Any intermediate propositional logic (i.e., a logic including intuitionistic logic and contained in classical logic) can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert's $\varepsilon$-calculus. The first and second $\varepsilon$-theorems for classical logic establish conservativity of the $\varepsilon$-calculus over its classical base logic. It is well known that the second $\varepsilon$-theorem fails for the intuitionistic $\varepsilon$-calculus, as prenexation is impossible. The paper investigates the effect of adding critical $\varepsilon$- and $\tau$-formulas and using the translation of quantifiers into $\varepsilon$- and $\tau$-terms to intermediate logics. It is shown that conservativity over the propositional base logic also holds for such intermediate $\varepsilon\tau$-calculi. The "extended" first $\varepsilon$-theorem holds if the base logic is finite-valued G\"odel-Dummett logic, fails otherwise, but holds for certain provable formulas in infinite-valued G\"odel logic. The second $\varepsilon$-theorem also holds for finite-valued first-order G\"odel logics. The methods used to prove the extended first $\varepsilon$-theorem for infinite-valued G\"odel logic suggest applications to theories of arithmetic.