Algebraic semantics of the \(\left\{ \rightarrow ,\square \right\} \)-fragment of Propositional Lax Logic

In this paper, we will study a particular subvariety of Hilbert algebras with a modal operator \(\square \), called Lax Hilbert algebras. These algebras are the algebraic semantic of the \(\left\{ \square ,\rightarrow \right\} \)-fragment of a particular intuitionistic modal logic, called Propositional Lax Logic (\(\mathcal {PLL}\)), which has applications to the formal verification of computer hardware. These algebras turn to be a generalization of the variety of Heyting algebras with a modal operator studied, under different names, by Macnab (Algebra Univ 12:5–29, 1981), Goldblatt (Math Logic Q 27(31–35):495–529, 1981; J Logic Comput 21(6):1035–1063, 2010) and by Bezhanishvili and Ghilardi (Ann Pure Appl Logic 147:84–100, 2007). We shall prove that the set of fixpoints of a Lax Hilbert algebra \(\left\langle A,\square \right\rangle \) is a Hilbert algebra such that its dual space is homeomorphic to the subspace of reflexive elements of the dual space of A. We will define the notion of subframe of a Hilbert space \(\left\langle X,{\mathcal {K}}\right\rangle \), and we will prove that there is a 1–1 correspondence between subframes of \(\left\langle X,{\mathcal {K}}\right\rangle \) and binary relations \(Q\subseteq X\times X\) such that \(\left\langle X,{\mathcal {K}},Q\right\rangle \) is a Lax Hilbert space. In addition, we will define the notion of subframe variety and we will prove that any variety of Hilbert algebras is a subframe variety.