Modal Companions

Origin. Gödel (1933), McKinsey-Tarski (1948), Blok-Esakia (1976). Modal logics extending S4 correspond to intermediate logics. Translation: □ for intuitionistic provability. Duality theory.

Models. Intermediate logic L has modal companion σ(L) ⊇ S4. Gödel translation embeds L into σ(L). Blok-Esakia isomorphism. Lattice correspondence.

Formalism.

Gödel translation: T(p) = □p T(⊥) = ⊥ T(φ ∧ ψ) = T(φ) ∧ T(ψ) T(φ ∨ ψ) = T(φ) ∨ T(ψ) T(φ → ψ) = □(T(φ) → T(ψ))

Embedding theorem: IPC ⊢ φ iff S4 ⊢ T(φ)

Modal companion: M ⊇ S4 is a modal companion of the intermediate logic L when L ⊢ φ iff M ⊢ T(φ). An L has many companions, and there are three maps, in two directions. Keeping them apart is the whole bookkeeping of the subject.

The three maps: ρ : NExt(S4) → Ext(Int), ρ(M) = {φ : T(φ) ∈ M}. Modal to intermediate — the intuitionistic fragment of M. A lattice epimorphism, and M is a companion of L exactly when ρ(M) = L. τ : Ext(Int) → NExt(S4), τ(L) = S4 ⊕ {T(φ) : L ⊢ φ}. The least modal companion. A lattice embedding, but not onto. σ : Ext(Int) → NExt(Grz), σ(L) = Grz ⊕ τ(L). The greatest modal companion — τ plus the Grzegorczyk axiom grz = □(□(p → □p) → p) → p.

Esakia's interval theorem: The modal companions of L are exactly the logics in the interval [τ(L), σ(L)] of NExt(S4). So companions are never unique, and "the" companion has to mean one end or the other.

Blok-Esakia theorem: σ : Ext(Int) → NExt(Grz) is a lattice isomorphism, with inverse ρ restricted to NExt(Grz). Ext(Int): intermediate logics. NExt(Grz): normal extensions of Grz. An intermediate logic has a whole interval of S4-companions but exactly one lying in NExt(Grz), and that one is σ(L) — which is why the isomorphism is stated for σ and not for τ. τ is injective but misses most of NExt(S4).

Examples: IPC: τ(IPC) = S4, σ(IPC) = Grz. The base case of the theorem — Grz is the largest extension of S4 with IPC as its intuitionistic fragment. CPC: τ(CPC) = S5, σ(CPC) = Triv. The familiar "IPC ↦ S4, CPC ↦ S5" pairing is the map τ, picking the least companion of each. LC (Gödel-Dummett): τ(LC) = S4.3

Duality: Modal algebras ↔ Heyting algebras. Esakia duality. Topological semantics.

Symbols.

Metatheory. The Gödel–McKinsey–Tarski theorem (McKinsey and Tarski 1948, proving what Gödel proposed in 1933) is the faithfulness result the subject rests on: IPC ⊢ φ iff S4 ⊢ T(φ), so the translation is an embedding and not merely sound. Maksimova and Rybakov (1974) established the three maps and their lattice behaviour — ρ is a lattice epimorphism of NExt(S4) onto Ext(Int), τ a lattice embedding that is not onto. Esakia's interval theorem places the companions of L exactly in [τ(L), σ(L)], and the Blok–Esakia theorem (Blok 1976, Esakia 1976) states that σ is an isomorphism of the complete lattice Ext(Int) onto NExt(Grz). Along σ and τ the finite model property, decidability, tabularity, and finite axiomatizability transfer in both directions, so a question about an intermediate logic and a question about its companion are literally the same question. Maksimova's interpolation theorems count the exceptions exactly: precisely eight intermediate logics have Craig interpolation (1977) and at most thirty-seven normal extensions of S4 do (1979).

Applies to. Intermediate logics. Modal logic classification. Provability interpretations. Algebraic logic.

Limitations. The theory is confined to NExt(S4): the isomorphism lands in NExt(Grz), a proper sublattice, and modal logics outside NExt(S4) — GL, the non-transitive systems, the non-normal ones — have no intuitionistic fragment the machinery can address. Companions are not unique and usually not close: since there are continuum many intermediate logics (Jankov), the interval [τ(L), σ(L)] is generally of cardinality continuum, ρ is not injective, and τ misses most of NExt(S4), so "the modal companion" is a convention picking an endpoint. Transfer is not an algorithm: whether a finitely axiomatized intermediate or transitive modal logic is decidable, has the finite model property, or is Kripke complete is itself undecidable (Chagrov), so knowing that a property crosses the isomorphism does not tell you whether either side has it. There is no predicate analogue — the Gödel translation embeds IPC into QS4, but no lattice isomorphism of the Blok–Esakia kind is available at first order.

© 2026 Lingenic LLC