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.
Let A be a propositional intuitionistic formula. A modal formula T(A) is defined by induction on the complexity of A:
T(p)=\Boxp,
p
T(\bot)=\bot,
T(A\landB)=T(A)\landT(B),
T(A\lorB)=T(A)\lorT(B),
T(A\toB)=\Box(T(A)\toT(B)).
A\to\bot
T(\negA)=\Box\negT(A).
\Box
For any normal modal logic M that extends S4, we define its si-fragment ρM as
\rhoM=\{A\midM\vdashT(A)\}.
L=\rhoM
Every superintuitionistic logic has modal companions. The smallest modal companion of L is
\tauL=S4 ⊕ \{T(A)\midL\vdashA\},
⊕
\tauL\subseteqM\subseteq\sigmaL
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
\Box(\Box(A\to\BoxA)\toA)\toA
Triv=K ⊕ (A\leftrightarrow\BoxA).
L | τL | σL | other companions of L |
---|---|---|---|
IPC | S4 | Grz | S4.1, Dum, ... |
KC | S4.2 | Grz.2 | S4.1.2, ... |
LC | S4.3 | Grz.3 | S4.1.3, S4.3Dum, ... |
CPC | S5 | Triv | see below |
The set of extensions of a superintuitionistic logic L ordered by inclusion forms a complete lattice, denoted ExtL. Similarly, the set of normal extensions of a modal logic M is a complete lattice NExtM. The companion operators ρM, τL, and σL can be considered as mappings between the lattices ExtIPC and NExtS4:
\rho\colonNExtS4\toExtIPC,
\tau,\sigma\colonExtIPC\toNExtS4.
\rho\circ\tau=\rho\circ\sigma
The mappings ρ and σ are mutually inverse lattice isomorphisms of ExtIPC and NExtGrz.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,
\sigmaL=\tauL ⊕ Grz.
The Gödel translation has a frame-theoretic counterpart. Let
F=\langleF,R,V\rangle
x\simy\iffxRy\landyRx
\langle\rhoF,\le\rangle=\langleF,R\rangle/{\sim}
\sim
\rhoV=\{A/{\sim}\midA\inV,A=\BoxA\}.
\rhoF=\langle\rhoF,\le,\rhoV\rangle
A is valid in ρF if and only if T(A) is valid in F.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
\{\rhoF;F\inC\}
The largest modal companions also have a semantic description. For any intuitionistic general frame
F=\langleF,\le,V\rangle
\Box
\sigmaF=\langleF,\le,\sigmaV\rangle
\{\sigmaF;F\inC\}
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.
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,
Every intermediate logic L has an infinite number of modal companions, and moreover, the set
\rho-1(L)
\rho-1(CPC)
L(Cn)
Cn
\rho-1(L)
The Gödel translation can be applied to rules as well as formulas: the translation of a rule
R= | A1,...,An |
B |
T(R)= | T(A1),...,T(An) |
T(B) |
.