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) = Triv. S5 is a companion of CPC, but neither endpoint of the interval; the familiar "IPC ↦ S4, CPC ↦ S5" pairing picks a convenient member, not the canonical one. LC (Gödel-Dummett): τ(LC) = S4.3

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

Symbols.

Symbol	Unicode	Name	Meaning
T	—	Translation	Gödel translation
□	U+25A1	Box	Provability/necessity
τ	U+03C4	Tau	Least modal companion, into NExt(S4)
σ	U+03C3	Sigma	Greatest modal companion, into NExt(Grz)
ρ	U+03C1	Rho	Modal to intermediate: intuitionistic fragment
Grz	—	Grzegorczyk logic	S4 ⊕ □(□(p → □p) → p) → p

Metatheory. Blok-Esakia isomorphism. Faithfulness. Preservation of properties along the interval. Duality.

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

Limitations. Only S4 extensions. Translation overhead. Not all properties transfer.