Christian Espíndola: On Glivenko theorems for intermediate predicate logics

We will expose 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, from which we will show with the same elementary arguments some Glivenko-type theorems relating intermediate logics between intuitionistic and classical logic. We will consider two schemata, the double negation shift (DNS) and the one consisting of instances of the principle of excluded middle for sentences (REM). We will prove that both schematas 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 will show that over every intermediate logic there exists a maximal intermediate logic for which Glivenko's theorem holds, and also deduce two characterizations of DNS, as the weaker (with respect to derivability) schema that added to REM derives classical logic and as the strongest (with respect to derivability) schema among the ¬¬-stable ones.