Logics of involutive Stone algebras

TL;DR

This paper explores the logic IS≤ derived from involutive Stone algebras, extending it to a wide family of logics, providing axiomatizations, and analyzing its relation to super-Belnap logics, with proof-theoretic and lattice-theoretic insights.

Contribution

It introduces a method to conservatively expand super-Belnap logics to IS≤ extensions and provides finite axiomatizations for these logics.

Findings

IS≤ is a conservative expansion of Belnap-Dunn logic.

A finite Hilbert-style axiomatization for IS≤ is provided.

The lattice of super-Belnap logics embeds into the lattice of IS≤ extensions.

Abstract

An involutive Stone algebra (IS-algebra) is a structure that is simultaneously a De Morgan algebra and a Stone algebra (i.e. a pseudo-complemented distributive lattice satisfying the well-known Stone identity ~xv~~x=1). IS-algebras have been studied algebraically and topologically since the 1980's, but a corresponding logic (here denoted IS$\leq$) has been introduced only very recently. The logic IS$\leq$ is the departing point for the present study, which we then extend to a wide family of previously unknown logics defined from IS-algebras. We show that IS$\leq$ 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 so as to obtain an extension of IS$\leq$. We show that every logic thus defined can be axiomatized by adding a fixed finite set of rule schemata to the corresponding super-Belnap base logic. We also consider a few sample extensions of IS$\leq$ that cannot be obtained in the above-described way, but can nevertheless be axiomatized finitely by other methods. Most of our axiomatization results are obtained in two steps: through a multiple-conclusion calculus first, which we then reduce to a traditional one. The multiple-conclusion axiomatizations introduced in this process, being analytic, are of independent interest from a proof-theoretic standpoint. Our results entail that the lattice of super-Belnap logics (which is known to be uncountable) embeds into the lattice of extensions of IS$\leq$. Indeed, as in the super-Belnap case, we establish that the finitary extensions of IS$\leq$ are already uncountably many.