Inlogic, amodal companion of asuperintuitionistic (intermediate) logicL is anormalmodal logic that interpretsL by a certain canonical translation, described below. Modal companions share various properties of the originalintermediate logic, which enables to study intermediate logics using tools developed for modal logic.

LetA be apropositionalintuitionistic formula. A modal formulaT(A) is defined by induction on the complexity ofA:^[1]

${\displaystyle T(p)=◻p,}$ for anypropositional variable${\displaystyle p}$,

${\displaystyle T(\mathrm{\perp })=\mathrm{\perp },}$

${\displaystyle T(A\wedge B)=T(A)\wedge T(B),}$

${\displaystyle T(A\vee B)=T(A)\vee T(B),}$

${\displaystyle T(A\to B)=◻(T(A)\to T(B)).}$

As negation is in intuitionistic logic defined by${\displaystyle A\to \mathrm{\perp }}$, we also have

${\displaystyle T(\mathrm{\neg }A)=◻\mathrm{\neg }T(A).}$

T is called theGödel translation orGödel–McKinsey–Tarski translation. The translation is sometimes presented in slightly different ways: for example, one may insert${\displaystyle ◻}$ before every subformula. All such variants are provably equivalent inS4.

For any normal modal logicM that extendsS4, we define itssi-fragmentρM as

${\displaystyle \rho M=\{A\mid M⊢T(A)\}.}$

The si-fragment of anynormal extension ofS4 is a superintuitionistic logic. A modal logicM is amodal companion of a superintuitionistic logicL if${\displaystyle L=\rho M}$.

Every superintuitionistic logic has modal companions. Thesmallest modal companion ofL is

${\displaystyle \tau L=\mathbf{S}\mathbf{4}\oplus \{T(A)\mid L⊢A\},}$

where${\displaystyle \oplus }$ denotes normal closure. It can be shown that every superintuitionistic logic also has alargest modal companion, which is denoted byσL. A modal logicM is a companion ofL if and only if${\displaystyle \tau L\subseteq M\subseteq \sigma L}$.

For example,S4 itself is the smallest modal companion of intuitionistic logic (IPC). The largest modal companion ofIPC is theGrzegorczyk logicGrz, axiomatized by the axiom

${\displaystyle ◻(◻(A\to ◻A)\to A)\to A}$

overK. The smallest modal companion of classical logic (CPC) isLewis'S5, whereas its largest modal companion is the logic

${\displaystyle \mathbf{T}\mathbf{r}\mathbf{i}\mathbf{v}=\mathbf{K}\oplus (A\leftrightarrow ◻A).}$

More examples:

The set of extensions of a superintuitionistic logicL ordered by inclusion forms acomplete lattice, denoted ExtL. Similarly, the set of normal extensions of a modal logicM is a complete lattice NExtM. The companion operatorsρM,τL, andσL can be considered as mappings between the lattices ExtIPC and NExtS4:

${\displaystyle \rho :\mathrm{N}\mathrm{E}\mathrm{x}\mathrm{t}\mathbf{S}\mathbf{4}\to \mathrm{E}\mathrm{x}\mathrm{t}\mathbf{I}\mathbf{P}\mathbf{C},}$

${\displaystyle \tau ,\sigma :\mathrm{E}\mathrm{x}\mathrm{t}\mathbf{I}\mathbf{P}\mathbf{C}\to \mathrm{N}\mathrm{E}\mathrm{x}\mathrm{t}\mathbf{S}\mathbf{4}.}$

It is easy to see that all three aremonotone, and${\displaystyle \rho \circ \tau =\rho \circ \sigma }$ is theidentity function on ExtIPC.L. Maksimova andV. Rybakov have shown thatρ,τ, andσ are actuallycomplete, join-complete and meet-complete lattice homomorphisms respectively. The cornerstone of the theory of modal companions is theBlok–Esakia theorem, proved independently byWim Blok andLeo Esakia. It states

The mappingsρ andσ are mutuallyinverse latticeisomorphisms of ExtIPCand NExtGrz.

Accordingly,σ and therestriction ofρ to NExtGrz are called theBlok–Esakia isomorphism. An important corollary to the Blok–Esakia theorem is a simple syntactic description of largest modal companions: for every superintuitionistic logicL,

${\displaystyle \sigma L=\tau L\oplus \mathbf{G}\mathbf{r}\mathbf{z}.}$

The Gödel translation has a frame-theoretic counterpart. Let${\displaystyle \mathbf{F}=⟨F,R,V⟩}$ be atransitive andreflexive modalgeneral frame. ThepreorderR induces theequivalence relation

${\displaystyle x\sim y⟺xRy\wedge yRx}$

onF, which identifies points belonging to the same cluster. Let${\displaystyle ⟨\rho F,\le ⟩=⟨F,R⟩/\sim }$ be the inducedquotientpartial order (i.e.,ρF is the set ofequivalence classes of${\displaystyle \sim }$), and put

${\displaystyle \rho V=\{A/\sim \mid A\in V,A=◻A\}.}$

Then${\displaystyle \rho \mathbf{F}=⟨\rho F,\le ,\rho V⟩}$ is an intuitionistic general frame, called theskeleton ofF. The point of the skeleton construction is that it preserves validity modulo Gödel translation: for any intuitionistic formulaA,

A is valid inρF if and only ifT(A) is valid inF.

Therefore, the si-fragment of a modal logicM can be defined semantically: ifM is complete with respect to a classC of transitive reflexive general frames, thenρM is complete with respect to the class${\displaystyle \{\rho \mathbf{F};\mathbf{F}\in C\}}$.

The largest modal companions also have a semantic description. For any intuitionistic general frame${\displaystyle \mathbf{F}=⟨F,\le ,V⟩}$, letσV be the closure ofV under Boolean operations (binaryintersection andcomplement). It can be shown thatσV is closed under${\displaystyle ◻}$, thus${\displaystyle \sigma \mathbf{F}=⟨F,\le ,\sigma V⟩}$ is a general modal frame. The skeleton ofσF is isomorphic toF. IfL is a superintuitionistic logic complete with respect to a classC of general frames, then its largest modal companionσL is complete with respect to${\displaystyle \{\sigma \mathbf{F};\mathbf{F}\in C\}}$.

The skeleton of aKripke frame is itself a Kripke frame. On the other hand,σF is never a Kripke frame ifF 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,

• decidability is preserved byρ,τ, andσ,
• finite model property is preserved byρ,τ, andσ,
• tabularity is preserved byρ andσ,
• Kripke completeness is preserved byρ andτ,
• first-order definability on Kripke frames is preserved byρ andτ.

Every intermediate logicL has aninfinite number of modal companions, and moreover, the set${\displaystyle {\rho }^{-1}(L)}$ of modal companions ofL contains aninfinite descending chain. For example,${\displaystyle {\rho }^{-1}(\mathbf{C}\mathbf{P}\mathbf{C})}$ consists ofS5, and the logics${\displaystyle L(C_n)}$ for every positive integern, where${\displaystyle C_n}$ is then-element cluster. The set of modal companions of anyL is eithercountable, or it has thecardinality of the continuum. Rybakov has shown that the lattice ExtL can beembedded in${\displaystyle {\rho }^{-1}(L)}$; 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 belowKC). It is unknown whether the converse is also true.

The Gödel translation can be applied torules as well as formulas: the translation of a rule

${\displaystyle R=\frac{A_1,\dots ,A_n}{B}}$

is the rule

${\displaystyle T(R)=\frac{T(A_1),\dots ,T(A_n)}{T(B)}.}$

A ruleR isadmissible in a logicL if the set of theorems ofL is closed underR. It is easy to see thatR is admissible in a superintuitionistic logicL wheneverT(R) is admissible in a modal companion ofL. The converse is not true in general, but it holds for the largest modal companion ofL.

• Alexander Chagrov and Michael Zakharyaschev,Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997.

• Gödel, Kurt (1986) [1933]. "Eine Interpretation des intuitionistischen Aussagenkalkiils". InFeferman, Solomon;Dawson, Jr., John W.;Kleene, Stephen C.; Moore, Gregory H.;Solovay, Robert M.;Van Heijenoort, Jean (eds.).Publications 1929–1936(PDF). Collected Works. Vol. I. New York:Oxford University Press.ISBN 978-0-19-503964-1. / Paperback:ISBN 978-0-19-514720-9

• Vladimir V. Rybakov,Admissibility of Logical Inference Rules, vol. 136 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1997.

• Modal logic