We investigate a peculiar intuitionistic modal logic, called Propositional Lax Logic (PLL), which has promising applications to the formal verification of computer hardware. The logic has emerged from an attempt to express correctness `up to' behavioural constraints - a central notion in hardware verification - as a logical modality. As a modal logic it is special since it features a single modal operator that has a flavour both of possibility and of necessity.
In the paper we provide the motivation for PLL and present several technical results. We investigate some of its proof-theoretic properties, presenting a cut-elimination theorem for a standard Gentzen-style sequent presentation of the logic. We go on to define a new class of fallible two-frame Kripke models for PLL. These models are unusual since they feature worlds with inconsistent information; furthermore, the only frame condition imposed is that the modal frame be a subrelation of the implication frame. We give a natural translation of these models into Goldblatt's J-space models of PLL. Our completeness theorem for these models yields a Goedel-style embedding of PLL into a classical bimodal theory of type S4/S4 and underpins a simple proof of the finite model property. We proceed to prove soundness and completeness of several theories for specialized classes of models.
We conclude with a brief exploration of two concrete and rather natural types of model from hardware verification for which the modality models correctness up to timing constraints. We obtain decidability of modal-free fragment of the logic of the first type of model, which coincides with the stable form of Maksimova's intermediate logic LP.