Modal companion

In logic, a modal companion of a superintuitionistic (intermediate) logic "L" is a normal modal logic that interprets "L" by a certain canonical translation, described below. Modal companions share various properties of the original intermediate logic, which enables to study intermediate logics using tools developed for modal logic.
Gödel–McKinsey–Tarski translation.
Let "A" be a propositional intuitionistic formula. A modal formula "T"("A") is defined by induction on the complexity of "A":
As negation is in intuitionistic logic defined by formula_7, we also have
"T" is called the Gödel translation or Gödel–McKinsey–Tarski translation. The translation is sometimes presented in slightly different ways: for example, one may insert formula_9 before every subformula. All such variants are provably equivalent in S4.
Modal companions.
For any normal modal logic "M" that extends S4, we define its si-fragment "ρM" as
The si-fragment of any normal extension of S4 is a superintuitionistic logic. A modal logic "M" is a modal companion of a superintuitionistic logic "L" if formula_11.
Every superintuitionistic logic has modal companions. The smallest modal companion of "L" is
where formula_13 denotes normal closure. It can be shown that every superintuitionistic logic also has a largest modal companion, which is denoted by "σL". A modal logic "M" is a companion of "L" if and only if formula_14.
For example, S4 itself is the smallest modal companion of intuitionistic logic (IPC). The largest modal companion of IPC is the Grzegorczyk logic Grz, axiomatized by the axiom
over K. The smallest modal companion of classical logic (CPC) is Lewis' S5, whereas its largest modal companion is the logic
More examples:
Blok–Esakia isomorphism.
The set of extensions of a superintuitionistic logic "L" ordered by inclusion forms a complete lattice, denoted Ext"L". Similarly, the set of normal extensions of a modal logic "M" is a complete lattice NExt"M". The companion operators "ρM", "τL", and "σL" can be considered as mappings between the lattices ExtIPC and NExtS4:
It is easy to see that all three are monotone, and formula_19 is the identity function on ExtIPC. L. Maksimova and V. Rybakov have shown that "ρ", "τ", and "σ" are actually complete, join-complete and meet-complete lattice homomorphisms respectively. The cornerstone of the theory of modal companions is the Blok–Esakia theorem, proved independently by Wim Blok and Leo Esakia. It states
Accordingly, "σ" and the restriction of "ρ" to NExtGrz are called the Blok–Esakia isomorphism. An important corollary to the Blok–Esakia theorem is a simple syntactic description of largest modal companions: for every superintuitionistic logic "L",
Semantic description.
The Gödel translation has a frame-theoretic counterpart. Let formula_21 be a transitive and reflexive modal general frame. The preorder "R" induces the equivalence relation
on "F", which identifies points belonging to the same cluster. Let formula_23 be the induced quotient partial order (i.e., "ρF" is the set of equivalence classes of formula_24), and put
Then formula_26 is an intuitionistic general frame, called the skeleton of F. The point of the skeleton construction is that it preserves validity modulo Gödel translation: for any intuitionistic formula "A",
Therefore, the si-fragment of a modal logic "M" can be defined semantically: if "M" is complete with respect to a class "C" of transitive reflexive general frames, then "ρM" is complete with respect to the class formula_27.
The largest modal companions also have a semantic description. For any intuitionistic general frame formula_28, let "σV" be the closure of "V" under Boolean operations (binary intersection and complement). It can be shown that "σV" is closed under formula_9, thus formula_30 is a general modal frame. The skeleton of "σ"F is isomorphic to F. If "L" is a superintuitionistic logic complete with respect to a class "C" of general frames, then its largest modal companion "σL" is complete with respect to formula_31.
The skeleton of a Kripke frame is itself a Kripke frame. On the other hand, "σ"F is never a Kripke frame if F is a Kripke frame of infinite depth.
Preservation theorems.
The value of modal companions and the Blok–Esakia theorem as a tool for investigation of intermediate logics comes from the fact that many interesting properties of logics are preserved by some or all of the mappings "ρ", "σ", and "τ". For example,
Other properties.
Every intermediate logic "L" has an infinite number of modal companions, and moreover, the set formula_32 of modal companions of "L" contains an infinite descending chain. For example, formula_33 consists of S5, and the logics formula_34 for every positive integer "n", where formula_35 is the "n"-element cluster. The set of modal companions of any "L" is either countable, or it has the cardinality of the continuum. Rybakov has shown that the lattice Ext"L" can be embedded in formula_32; in particular, a logic has a continuum of modal companions if it has a continuum of extensions (this holds, for instance, for all intermediate logics below KC). It is unknown whether the converse is also true.
The Gödel translation can be applied to rules as well as formulas: the translation of a rule
is the rule
A rule "R" is admissible in a logic "L" if the set of theorems of "L" is closed under "R". It is easy to see that "R" is admissible in a superintuitionistic logic "L" whenever "T"("R") is admissible in a modal companion of "L". The converse is not true in general, but it holds for the largest modal companion of "L".