id: 05989562
dt: j
an: 05989562
au: Goldblatt, Robert
ti: Cover semantics for quantified lax logic.
so: J. Log. Comput. 21, No. 6, 1035-1063 (2011).
py: 2011
pu: Oxford University Press, Oxford
la: EN
cc: 
ut: modal logic; lax modality; first-order intuitionistic logic; quantified lax
    logic
ci: 
li: doi:10.1093/logcom/exq029
ab: Lax modalities are dealt with, where a modal formula $ \bigcirc ϕ$ is read
    as “there is some constraint under which $ϕ$ is true". From the
    author’s abstract: “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 article
    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.
    [\dots] In addition, the theory is worked out for certain constructive
    versions of the classical logics ${\ssf K}$ and ${\ssf S4}$. An
    alternative 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
    article provides further evidence that there is more to intuitionistic
    modal logic than the generalization of properties of boxes and diamonds
    from Boolean modal logic."
rv: Damas Gruska (Bratislava)