Propositional lax logic

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 circle 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 circle-frame be a subrelation of the superset of-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 Godel-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 circle models correctness up to timing constraints. We obtain decidability of circle-free fragment of the logic of the first type of model, which coincides with the stable form of Maksimova's intermediate logic L box with bottom missing. (C) 1997 Academic Press