Algebraic semantics of the { → , □ } -fragment of Propositional Lax Logic

Abstract

In this paper, we will study a particular subvariety of Hilbert algebras with a modal operator □ , called Lax Hilbert algebras. These algebras are the algebraic semantic of the { □ , → } -fragment of a particular intuitionistic modal logic, called Propositional Lax Logic (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 〈 A, □ 〉 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 〈 X, K〉 , and we will prove that there is a 1–1 correspondence between subframes of 〈 X, K〉 and binary relations Q⊆ X× X such that 〈 X, K, Q〉 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.