Glivenko theorems and negative translations in substructural predicate logics (Q1938390)

The Glivenko theorem holds for a logic \(\mathbf L\) relative to a logic \(\mathbf K\) if, for any formula \(\alpha\), \(\alpha\) is provable in \(\mathbf K\) iff \(\neg\neg\alpha\) is provable in \(\mathbf L\). For instance, the Glivenko theorem holds for intuitionistic propositional logic relative to classical propositional logic, and also for the extension of intuitionistic predicate logic by the double negation shift scheme \(\forall x\neg\neg\varphi(x)\to\neg\neg\forall x\varphi(x)\) relative to classical predicate logic. In this paper, following the same line as the one of [the second author, Ann. Pure Appl. Logic 161, No. 2, 246--250 (2009; Zbl 1181.03021)], a proof-theoretic approach to Glivenko theorems is developed 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. The authors show that among the substructural predicate logics there exists a unique weakest system over intuitionistic linear predicate logic without exponentials for which the Glivenko theorem holds. A negative translation of logical systems, called extended Kuroda translation, is defined, and then it is also shown that among the involutive substructural predicate logics there exists a unique weakest system over intuitionistic linear predicate logic without exponentials for which the extended Kuroda translation works. The paper includes algebraic aspects of these results as well, and contributes to a better understanding of the role of Glivenko theorems and negative translations in the context of substructural logics.