Semisimplicity, Glivenko theorems, and the excluded middle

Abstract

We formulate a general, signature-independent form of the law of the excluded middle and prove that a logic is semisimple if and only if it enjoys this law, provided that it satisfies a weak form of the so-called inconsistency lemma of Raftery. We then show that this equivalence can be used to provide simple syntactic proofs of the theorems of Kowalski and Kracht characterizing the semisimple varieties of FLew-algebras and Boolean algebras with operators, and to extend them to FLe-algebras and Heyting algebras with operators. Moreover, under stronger assumptions this correspondence works at the level of individual models: the semisimple models of such a logic are precisely those which satisfy an axiomatic form of the law of the excluded middle, and a Glivenko-like connection obtains between the logic and its extension by the axiom of the excluded middle. This in particular subsumes the well-known Glivenko theorems relating intuitionistic and classical logic and the modal logics S4 and S5. As a consequence, we also obtain a description of the subclassical substructural logics which are Glivenko related to classical logic.