A short proof of Glivenko theorems for intermediate predicate logics
2013 (English)In: Archive for mathematical logic, ISSN 0933-5846, E-ISSN 1432-0665, Vol. 52, no 7-8, 823-826 p.Article in journal (Refereed) Published
We give a simple proof-theoretic argument showing that Glivenko’s theorem for propositional logic and its version for predicate logic follow as an easy consequence of the deduction theorem, which also proves some Glivenko type theorems relating intermediate predicate logics between intuitionistic and classical logic. We consider two schemata, the double negation shift (DNS) and the one consisting of instances of the principle of excluded middle for sentences (REM). We prove that both schemata combined derive classical logic, while each one of them provides a strictly weaker intermediate logic, and neither of them is derivable from the other. We show that over every intermediate logic there exists a maximal intermediate logic for which Glivenko’s theorem holds. We deduce as well a characterization of DNS, as the weakest (with respect to derivability) scheme that added to REM derives classical logic.
Place, publisher, year, edition, pages
2013. Vol. 52, no 7-8, 823-826 p.
Glivenko’s theorem, Negative translations, Double negation shift, Proof-theoretic methods
Algebra and Logic
Research subject Mathematics
IdentifiersURN: urn:nbn:se:su:diva-94966DOI: 10.1007/s00153-013-0346-7ISI: 000328257800009OAI: oai:DiVA.org:su-94966DiVA: diva2:657374
FunderSwedish Research Council