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: σ(L) = smallest S4-extension validating L under T. L ⊢ φ iff σ(L) ⊢ T(φ)

ρ-companion (largest): ρ(L) = {φ | T⁻¹(φ) ⊆ L} Largest modal logic translating into L.

Blok-Esakia theorem: σ: Int → NExt(S4) isomorphism. Int: intermediate logics. NExt(S4): normal extensions of S4.

Examples: IPC → S4 CPC → S5 LC (Gödel-Dummett) → 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+03C3	Sigma	Modal companion
ρ	U+03C1	Rho	Largest companion

Metatheory. Blok-Esakia isomorphism. Faithfulness. Preservation of properties. Duality.

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

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