We examine second order intuitionistic propositional logic, IPC². Let $F_\exists $ be the set of formulas with no universal quantification. We prove Glivenko's theorem for formulas in $F_\exists $ that is, for φ € $F_\exists $ φ is a classical tautology if and only if ¬¬φ is a tautology of IPC². We show that for each sentence φ € $F_\exists $ (without free variables), φ is a classical tautology if and only if φ is an intuitionistic tautology. As a corollary (...) we obtain a semantic argument that the quantifier V is not definable in IPC² from ⊥, V, ^, →. (shrink)

A natural deduction formulation is given for the intermediate logic called MH by Gabbay in [4]. Proof-theoretic methods are used to show that every deduction can be normalized, that MH is the weakest intermediate logic for which the Glivenko theorem holds, and that the Craig-Lyndon interpolation theorem holds for it.

A normalization procedure is given for classical natural deduction with the standard rule of indirect proof applied to arbitrary formulas. For normal derivability and the subformula property, it is sufficient to permute down instances of indirect proof whenever they have been used for concluding a major premiss of an elimination rule. The result applies even to natural deduction for classical modal logic.

The usual rule used to obtain natural deduction formulations of classical logic from intuitionistic logic, namely.

It is well known that classical propositional logic can be interpreted in intuitionistic propositional logic. In particular Glivenko's theorem states that a formula is provable in the former iff its double negation is provable in the latter. We extend Glivenko's theorem and show that for every involutive substructural logic there exists a minimum substructural logic that contains the first via a double negation interpretation. Our presentation is algebraic and is formulated in the context of residuated lattices. In the last part (...) of the paper, we also discuss some extended forms of the Kolmogorov translation and we compare it to the Glivenko translation. (shrink)

Along the same line as that in Ono (Ann Pure Appl Logic 161:246–250, 2009), a proof-theoretic approach to Glivenko theorems is developed here for substructural predicate logics relative not only to classical predicate logic but also to arbitrary involutive substructural predicate logics over intuitionistic linear predicate logic without exponentials QFLe. It is shown that there exists the weakest logic over QFLe among substructural predicate logics for which the Glivenko theorem holds. Negative translations of substructural predicate logics are studied by using (...) the same approach. First, a negative translation, called extended Kuroda translation is introduced. Then a translation result of an arbitrary involutive substructural predicate logics over QFLe is shown, and the existence of the weakest logic is proved among such logics for which the extended Kuroda translation works. They are obtained by a slight modification of the proof of the Glivenko theorem. Relations of our extended Kuroda translation with other standard negative translations will be discussed. Lastly, algebraic aspects of these results will be mentioned briefly. In this way, a clear and comprehensive understanding of Glivenko theorems and negative translations will be obtained from a substructural viewpoint. (shrink)

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. (shrink)

n this paper we investigate the implication-less fragment of Johansson's minimal logic. We call it subminimal logic and we study its associated algebras, which we call weak algebras. We prove the algebraic Glivenko theorem, soundness and completeness for this logic.