A short proof of Glivenko theorems for intermediate predicate logics (Q377463)

This short paper deals with Glivenko-type theorems for intermediate logics, which are, among other things, shown to follow from the deduction theorem. In the terminology adopted by the author, the original Glivenko theorem shows that the Glivenko theorem holds for (propositional) classical logic over intuitionistic logic (IL). So the paper contains a short proof that for any set \(S\) of sentences, valid in classical logic, the Glivenko theorem holds for (a) IL + law of the excluded middle for sentences (REM) + \(S\) over (b) IL + \(S\). From this proposition, the well known original version of Glivenko theorem and its version for first-order logic (with additional double negation shift scheme) as well as infinitely many other variants of Glivenko-type theorems can be obtained as corollaries. Moreover, (a) is the biggest logic with this property for (b). Further, if \(S\) only contains \(\neg\neg\)-stable (in intuitionistic logic) sentences, then (b) is the least logic for the given (a) with this property. The paper also contains a proposition characterizing the double negation shift (DNS) axiom scheme in the domain of intermediate logics. DNS is shown to be the weakest scheme deriving classical logic in IL + REM, and the strongest one among the \(\neg\neg\)-stable sentences valid in classical logic. It is shown to be independent from REM, and the latter is shown to be unable to derive any new \(\neg\neg\)-stable sentences in intuitionistic logic.