2019/07/10 by Matthias Baaz, Baaz, Matthias, Richard Zach +1
Mathematics · #03B20 #03B55 #03F05 #FOS: Mathematics #Logic (math.LO) #math.LO #msc:03B20 #msc:03B55 #msc:03F05
paper · pdf · doi:10.48550/arxiv.1907.04477
arxiv created 2021/11/30 · arxiv updated 2021/12/02
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 ε-calculus. The first and second ε-theorems for classical logic establish conservativity of the ε-calculus over its classical base logic. It is well known that the second ε-theorem fails for the intuitionistic ε-calculus, as prenexation is impossible. The paper investigates the effect of adding critical ε- and τ-formulas and using the translation of quantifiers into ε- and τ-terms to intermediate logics. It is shown that conservativity over the propositional base logic also holds for such intermediate ετ-calculi. The "extended" first ε-theorem holds if the base logic is finite-valued Gödel-Dummett logic, fails otherwise, but holds for certain provable formulas in infinite-valued Gödel logic. The second ε-theorem also holds for finite-valued first-order Gödel logics. The methods used to prove the extended first ε-theorem for infinite-valued Gödel logic suggest applications to theories of arithmetic.