Glivenko theorems for substructural logics over FL

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.

• Type: Journal
• Year: 2006
• Where: JSYML
• Authors: Nikolaos Galatos, Hiroakira Ono
• Keywords: Double Negation, JSYML 2006, Propositional Logic, Substructural Logic