Cover Semantics for Quantified Lax Logic
Lax modalities occur in intuitionistic logics concerned with hardware verification, the
computational lambda calculus, and access control in secure systems. They also encapsulate the
logic of Lawvere-Tierney-Grothendieck topologies on topoi.
This paper provides a complete semantics for quantified lax logic by combining the
Beth-Kripke-Joyal cover semantics for first-order intuitionistic logic with the classical relational semantics for a ``diamond'' modality. The main technique used is the lifting of a multiplicative closure operator (nucleus) from a Heyting algebra to its MacNeille completion, and the representation of an arbitrary locale as the lattice of ``propositions'' of a suitable cover system.
In addition, the theory is worked out for certain constructive versions of the classical logics
K and S4.
An alternative completeness proof is given for (non-modal) first-order intuitionistic logic
itself with respect to the cover semantics, using a simple and explicit Henkin-style
construction of a characteristic model whose points are principal theories rather than prime
saturated ones.
The paper provides further evidence that there is more to intuitionistic modal logic than
the generalisation of properties of boxes and diamonds from Boolean modal logic.