Canonical Formulas for the Lax Logic
Sebastian David Melzer
Abstract:
We develop the method of canonical formulas for the lax logic. This is an intuitionistic modal logic that formalises nuclei of pointless topology and has applications in formal hardware verification. We show that all extensions of the lax logic can be axiomatised by lax canonical formulas. We give a dual description of lax canonical formulas by extending generalised Esakia duality for nuclear implicative semilattice homomorphisms. We go on to generalise lax canonical formulas to introduce steady logics, a class of lax logics that is structurally very similar to subframe logics for intermediate logics, for example, they all have the finite model property and are generated by classes closed under subframes. We look at translations of intermediate logics into lax logic and show a number of preservation results. In particular, we prove a lax analogue for the Dummett-Lemmon conjecture that the least modal companion of each Kripke-complete intermediate logic is Kripke-complete.