Modal companion

Modal companion

In logic, a modal companion of a superintuitionistic (intermediate) logic L is a normal modal logic which 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:

T(p)=\Box p for any propositional variable p,
T(A\land B)=T(A)\land T(B),
T(A\lor B)=T(A)\lor T(B),
T(A\to B)=\Box(T(A)\to T(B)).

As negation is in intuitionistic logic defined by A\to\bot, we also have

T(\neg A)=\Box\neg T(A).

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 \Box before every subformula. All such variants are provably equivalent in S4.

Modal companions

For any normal modal logic M which extends S4, we define its si-fragment ρM as

\rho M=\{A\mid M\vdash T(A)\}.

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 L = ρM.

Every superintuitionistic logic has modal companions. The smallest modal companion of L is

\tau L=\mathbf{S4}\oplus\{T(A)\mid L\vdash A\},

where \oplus denotes normal closure. It can be shown that every superintuitionistic logic also has the largest modal companion, which is denoted by σL. A modal logic M is a companion of L if and only if \tau L\subseteq M\subseteq\sigma L.

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

\Box(\Box(A\to\Box A)\to A)\to A

over K. The smallest modal companion of the classical logic (CPC) is Lewis' S5, whereas its largest modal companion is the logic

\mathbf{Triv}=\mathbf K\oplus(A\leftrightarrow\Box A).

More examples:

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

Blok–Esakia isomorphism

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:


It is easy to see that all three are monotone, and \rho\circ\tau=\rho\circ\sigma is the identity function on ExtIPC. L. Maksimova and V. Rybakov have shown that ρ, τ, and σ are actually complete lattice homomorphisms. The cornerstone of the theory of modal companions is the Blok–Esakia theorem, proved independently by Wim Blok and Leo Esakia. It states

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,

\sigma L=\tau L+\mathbf{Grz}.

Semantic description

The Gödel translation has a frame-theoretic counterpart. Let \mathbf F=\langle F,R,V\rangle be a transitive and reflexive modal general frame. The preorder R induces the equivalence relation

x\sim y \iff x\,R\,y \land y\,R\,x

on F, which identifies points belonging to the same cluster. Let \langle\rho F,\le\rangle=\langle F,R\rangle/{\sim} be the induced quotient partial order (i.e., ρF is the set of equivalence classes of ), and put

\rho V=\{A/{\sim}\mid A\in V,A=\Box A\}.

Then \rho\mathbf F=\langle\rho F,\le,\rho V\rangle 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,

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 \{\rho\mathbf F;\,\mathbf F\in C\}.

The largest modal companions also have a semantic description. For any intuitionistic general frame \mathbf F=\langle F,\le,V\rangle, let σV be the closure of V under Boolean operations (binary intersection and complement). It can be shown that σV is closed under \Box, thus \sigma\mathbf F=\langle F,\le,\sigma V\rangle 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 \{\sigma\mathbf F;\,\mathbf F\in C\}.

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 ρ − 1(L) of modal companions of L contains an infinite descending chain. For example, \rho^{-1}(\mathbf{CPC}) consists of S5, and the logics L(Cn) for every positive integer n, where Cn 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 ExtL can be embedded in ρ − 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 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.


  • Alexander Chagrov and Michael Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997.
  • Vladimir V. Rybakov, Admissibility of Logical Inference Rules, vol. 136 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1997.

Wikimedia Foundation. 2010.

Look at other dictionaries:

  • General frame — In logic, general frames (or simply frames) are Kripke frames with an additional structure, which are used to model modal and intermediate logics. The general frame semantics combines the main virtues of Kripke semantics and algebraic semantics:… …   Wikipedia

  • Intermediate logic — In mathematical logic, a superintuitionistic logic is a propositional logic extending intuitionistic logic. Classical logic is the strongest consistent superintuitionistic logic. Thus consistent superintuitionistic logics are called intermediate… …   Wikipedia

  • List of mathematics articles (M) — NOTOC M M estimator M group M matrix M separation M set M. C. Escher s legacy M. Riesz extension theorem M/M/1 model Maass wave form Mac Lane s planarity criterion Macaulay brackets Macbeath surface MacCormack method Macdonald polynomial Machin… …   Wikipedia

  • History of logic — Philosophy ( …   Wikipedia

  • Jazz — For other uses, see Jazz (disambiguation). Jazz Stylistic origins: Blues • Folk • March • Ragtime …   Wikipedia

  • Entailment — For other uses, see Entail (disambiguation). In logic, entailment is a relation between a set of sentences (e.g.,[1] meaningfully declarative sentences or truthbearers) and a sentence. Let Γ be a set of one or more sentences; let S1 be the… …   Wikipedia

  • Modern Scots — Not to be confused with Scottish people. Scots language History …   Wikipedia

  • Logic — For other uses, see Logic (disambiguation). Philosophy …   Wikipedia

  • HEBREW LANGUAGE — This entry is arranged according to the following scheme: pre biblical biblical the dead sea scrolls mishnaic medieval modern period A detailed table of contents precedes each section. PRE BIBLICAL nature of the evidence the sources phonology… …   Encyclopedia of Judaism

  • Musical mode — This article is about modes as used in music. For other uses, see Mode (disambiguation). Modern Dorian mode on C  Play …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.