-
Unified Correspondence. Correspondence and completeness theory have a
long history in modal logic, and they are referred to as the “three pillars of
wisdom supporting the edifice of modal logic” [22, page 331] together with duality
theory. Dating back to [
20,21
], the Sahlqvist theorem gives a syntactic definition
of a class of modal formulas, the Sahlqvist class, each member of which defines
an elementary (i.e. first-order definable) class of Kripke frames and is canonical.
Since modal logic on the frame level is essentially second-order, computing the
first-order correspondence of a modal formula is a kind of second-order quantifier
elimination.
Recently, a uniform and modular theory which subsumes the above results
and extends them to logics with a non-classical propositional base has emerged,
and has been dubbed unified correspondence [
5
]. It is built on duality-theoretic
insights [
9
] and uniformly exports the state-of-the-art in Sahlqvist theory from
normal modal logic to a wide range of logics which include, among others,
intuitionistic and distributive and general (non-distributive) lattice-based (modal)
logics [
6,8
], non-normal (regular) modal logics based on distributive lattices of
arbitrary modal signature [
19
], hybrid logics [
12
], many valued logics [
16
] and
bi-intuitionistic and lattice-based modal mu-calculus [
1,3,2
]. Unified
correspondence theory has two components: the first one is a very general syntactic
definition of Sahlqvist and inductive formulas, which applies uniformly to each logical
signature and is given purely in terms of the order-theoretic properties of the
algebraic interpretations of the logical connectives; the second one is the
Ackermann lemma based algorithm ALBA, which is a generalization of SQEMA based
on order-theoretic and algebraic insights, which effectively computes first-order
correspondents of input formulas/inequalities, and is guaranteed to succeed on
the Sahlqvist and inductive classes of formulas/inequalities. The algorithm aims
at eliminating all propositional variables, which are, on the relational
semantics side, second-order variables, and rewrite the formula into a quasi-inequality
which contains only nominals and co-nominals, which are, on the relational
semantics side, essentially first-order. In this sense, unified correspondence theory
is essentially second-order quantifier elimination on the algebraic side.
The breadth of this work has stimulated many and varied applications. Some
are closely related to the core concerns of the theory itself, such as understanding
the relationship between different methodologies for obtaining canonicity results
[
18,7
], the phenomenon of pseudocorrespondence [
10
], and the investigation of
the extent to which the Sahlqvist theory of classes of normal distributive lattice
expansions can be reduced to the Sahlqvist theory of normal Boolean algebra
expansions, by means of G¨odel-type translations [
11
]. Other, possibly
surprising applications include the dual characterizations of classes of finite lattices
[
13
], the identification of the syntactic shape of axioms which can be translated
into structural rules of a proper display calculus [
14
] and of internal Gentzen
calculi for the logics of strict implication [
17
], and the epistemic interpretation
of lattice-based modal logic in terms of categorization theory in management
science [
4
]. These and other results (cf. [
9
]) form the body of a theory called
unified correspondence [
5
], a framework within which correspondence results can
be formulated and proved abstracting away from specific logical signatures,
using only the order-theoretic properties of the algebraic interpretations of logical
connectives.
Possibility Semantics. Possibility semantics for modal logic is a
generalization of standard Kripke semantics. In this semantics, a possibility frame has a
refinement relation which is a partial order between states, in addition to the
accessibility relation for modalities. From an algebraic perspective, full possibility
frames are dually equivalent to complete Boolean algebras with complete
operators which are not necessarily atomic, while filter-descriptive possibility frames
are dually equivalent to Boolean algebras with operators.
In recent years, the theoretic study of possibility semantics has received more
attention. In [
23
], Yamamoto investigates the correspondence theory in
possibility semantics in a frame-theoretic way and prove a Sahlqvist-type
correspondence theorem over full possibility frames, which are the possibility semantic
counterpart of Kripke frames, using insights from the algebraic understanding
of possibility semantics. In [15, Theorem 7.20], it is shown that all inductive
formulas are filter-canonical and hence every normal modal logic axiomatized
by inductive formulas is sound and complete with respect to its canonical full
possibility frame. However, the correspondence result for inductive formulas is
still missing, as well as the correspondence result over filter-descriptive
possibility frames (see [15, page 103]) and soundness and completeness with respect to
the corresponding elementary class of full possibility frames. The present paper
aims at giving a closer look at the aforementioned unsolved problems using the
algebraic and order-theoretic insights from a current ongoing research project,
namely unified correspondence.
Methodology. Our contribution is methodological: we analyze the
correspondence phenomenon in possibility semantics using the dual algebraic structures,
namely complete (not necessarily atomic) Boolean algebras with complete
operators, where the atoms are not always available. For the correspondence over
full possibility frames, our strategy is to identify two different Boolean algebras
with operators as the dual algebraic structures of the possibility frame, namely
the Boolean algebra of regular open subsets BRO (when viewing the possibility
frame as a possibility frame itself) and the Boolean algebra of arbitrary subsets
BFull (when viewing the possibility frame as a bimodal Kripke frame), where a
canonical order-embedding map e : BRO → BFull can be defined. The embedding
e preserves arbitrary meets, therefore a left adjoint c : BFull → BRO of e can be
defined, which sends a subset X of the domain W of possibilities to the smallest
regular open subset containing X. This left adjoint c plays an important role in
the dual characterization of the interpretations of the expanded language, which
form the ground of the regular open translation, i.e. the counterpart of standard
translation in possibility semantics. When it comes to canonicity, we use the fact
that filter-canonicity is equivalent to constructive canonicity [15, Theorem 5.46,
7.20], and prove a topological Ackermann lemma, which justifies the soundness
of propositional variable elimination rules and forms the basis of the
correspondence result with respect to the class of filter-descriptive frames as well as the
canonicity and completeness result with respect to the corresponding class of
full possibility frames.