Epsilon Theorems in Intermediate Logics

DOI10.1017/JSL.2021.103MaRDI QIDQ6321846arXivWikidataFDO

Authors Matthias Baaz, Richard Zach

Publication date 9 July 2019

Published in arXiv

Full work available at URL https://doi.org/10.1017/JSL.2021.103

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Intermediate logics (03B55) Cut-elimination and normal-form theorems (03F05)

arXiv classification

math.LO

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 $au$-formulas and using the translation of quantifiers into $varepsilon$- and $au$-terms to intermediate logics. It is shown that conservativity over the propositional base logic also holds for such intermediate $varepsilonau$-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.

This page was built for publication: Epsilon Theorems in Intermediate Logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6321846)