Semisimplicity, Glivenko theorems, and the excluded middle

TL;DR

This paper establishes a general connection between semisimplicity of logics, the law of the excluded middle, and Glivenko theorems, providing new syntactic and model-theoretic characterizations and extending classical results to various algebraic frameworks.

Contribution

It introduces a signature-independent law of the excluded middle, links semisimplicity to this law, and extends Glivenko theorems to a broad class of algebraic and substructural logics.

Findings

Semisimple logics satisfy a general law of the excluded middle.

Syntactic proofs of algebraic characterizations are provided.

A Glivenko-like correspondence is established for various logic extensions.

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.