Roy Dyckhoff
A cut-free sequent calculus for distributive
lattices with adjoint pairs of modal operators.
Abstract:
We present a cut-free sequent calculus for
validity of inequations m <= m' in an arbitrary
distributive lattice with a family of adjoint
pairs (f,g) of operators, where each f is both
the left adjoint of the corresponding g and
join-preserving. Such lattices are natural
generalisations of Boolean algebras with
(provided a symmetry axiom, i.e. B: <>[]phi
implies phi, holds) the traditional operators of
<> and [] from classical modal logic; we have in
mind future work to quantales with such operators
and applications in epistemic logic. Sequents in
such a calculus are formed not from sets,
multisets or lists but from more complex
structures, here called ''contexts'', but
variously known as ``nested sequents'' and``deep
sequents''; we will try and trace some of their
history.
This is joint work with Mehrnoosh Sadrzadeh.