The proof theory of Lax logic

Matt Fairtlough

(University of Sheffield)

In this work we investigate a novel intuitionistic modal logic, called Propositional Lax Logic, with promising applications to the construction of formal proofs, and in particular 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. The resulting logic is unorthodox in several respects. As a modal logic it is special since it features a single modal operator O (somehow) that has a flavour of both a modality of possibility and of necessity. As for hardware verification it is special since it is an intuitionistic rather than classical logic which so far has been the major logic of choice. Finally, its models are unusual since they feature worlds with inconsistent information and furthermore the only frame condition is that the O-frame be a subrelation of the ->-frame. In the work we will provide some motivation for Propositional Lax Logic and present several technical results. We will investigate some of its proof-theoretic properties, and prove a cut-elimination theorem for a standard Gentzen-style sequent presentation of the logic. We sketch proofs of soundness and completeness for a class of fallible two-frame Kripke models. In this framework we present a concrete and rather natural class of models from hardware verification such that the modality O models correctness up to timing constraints. This is a report on joint work with Dr. Michael Mendler of theTechnical University of Denmark, to whom any correspondence should be directed.
Tuesday 8th February 1994, 14:30
Seminar Room 322
Department of Computer Science