Logics of involutive Stone algebras

An involutive Stone algebra (IS-algebra) is simultaneously a De Morgan algebra and a Stone algebra (i.e., a pseudo-complemented distributive lattice satisfying the Stone identity \(\mathop {\sim }x \vee \mathop {\sim }\mathop {\sim }x \approx 1\)). IS-algebras have been studied algebraically and topologically since the 1980s, but a corresponding logic (here denoted \(\mathcal {IS}_{\le }\)) has been introduced only very recently. This logic is the departing point of the present study, which we then extend to a wide family of previously unknown logics defined from IS-algebras. We show that \(\mathcal {IS}_{\le }\) is a conservative expansion of the Belnap-Dunn four-valued logic (i.e., the order-preserving logic of the variety of De Morgan algebras), and we give a finite Hilbert-style axiomatization for it. More generally, we introduce a method for expanding conservatively every super-Belnap logic (i.e., every strengthening of the Belnap-Dunn logic) so as to obtain an extension of \(\mathcal {IS}_{\le }\). We show that every logic thus defined can be axiomatized by adding a fixed finite set of multiple-conclusion rule schemata to the corresponding super-Belnap base logic. Our results entail that the lattice of super-Belnap logics (which is known to be uncountable) embeds into the lattice of extensions of \(\mathcal {IS}_{\le }\). In fact, as in the super-Belnap case, we establish that the finitary extensions of \(\mathcal {IS}_{\le }\) are already uncountably many. When the base super-Belnap logic possesses a disjunction, we show that we can reduce the multiple-conclusion calculus to a traditional one; some of the multiple-conclusion axiomatizations so introduced are analytic and are thus of independent interest from a proof-theoretic standpoint. We also consider a few extensions of \(\mathcal {IS}_{\le }\) that cannot be obtained in the above-described way, but can nevertheless be axiomatized finitely by other methods.