Semisimplicity, Glivenko theorems, and the excluded middle

Abstract: There are at least three different ways to obtain classical propositional logic from intuitionistic propositional logic. Firstly, it is the extension of intuitionistic logic by the law of the excluded middle (LEM). Secondly, it is related to intuitionistic logic by the double-negation translation of Glivenko. Finally, the algebraic models of classical logic are precisely the semisimple algebraic models of intuitionistic logic (i.e. Boolean algebras are precisely the semisimple Heyting algebras). We show how to formulate the equivalence between the LEM and semisimplicity, and between what we might call the Glivenko companion and the semisimple companion of a logic, at an appropriate level of generality. This equivalence will subsume several existing Glivenko-like theorems, as well as some new ones. It also provides a useful technique for describing the semisimple subvarieties of a given variety of algebras. This is joint work with Tomáš Lávička, building on previous work by James Raftery.

logic

Audience: researchers in the topic

Online logic seminar

Series comments: Description: Seminar on all areas of logic