In logic, a modal companion of a superintuitionistic (intermediate) logic L is a normal modal logic that interprets L by a certain canonical translation, described below. Modal companions share various properties of the original intermediate logic, which enables the study of 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 ) = ◻ p , {\displaystyle T(p)=\Box p,} for any propositional variable p {\displaystyle p} ,
T ( ⊥ ) = ⊥ , {\displaystyle T(\bot )=\bot ,}
T ( A ∧ B ) = T ( A ) ∧ T ( B ) , {\displaystyle T(A\land B)=T(A)\land T(B),}
T ( A ∨ B ) = T ( A ) ∨ T ( B ) , {\displaystyle T(A\lor B)=T(A)\lor T(B),}
T ( A → B ) = ◻ ( T ( A ) → T ( B ) ) . {\displaystyle T(A\to B)=\Box (T(A)\to T(B)).}
As negation is in intuitionistic logic defined by A → ⊥ {\displaystyle A\to \bot } , we also have
T ( ¬ A ) = ◻ ¬ T ( A ) . {\displaystyle 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 ◻ {\displaystyle \Box } before every subformula. All such variants are provably equivalent in S4.
Modal companions For any normal modal logic M that extends S4, we define its si-fragment ρM as
ρ M = { A ∣ M ⊢ T ( A ) } . {\displaystyle \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 {\displaystyle L=\rho M} . Every superintuitionistic logic has modal companions. The smallest modal companion of L is
τ L = S 4 ⊕ { T ( A ) ∣ L ⊢ A } , {\displaystyle \tau L=\mathbf {S4} \oplus \{T(A)\mid L\vdash A\},}
where ⊕ {\displaystyle \oplus } denotes normal closure. It can be shown that every superintuitionistic logic also has a largest modal companion, which is denoted by σL. A modal logic M is a companion of L if and only if τ L ⊆ M ⊆ σ L {\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 of IPC is the Grzegorczyk logic Grz, axiomatized by the axiom
◻ ( ◻ ( A → ◻ A ) → A ) → A {\displaystyle \Box (\Box (A\to \Box A)\to A)\to A}
over K. The smallest modal companion of classical logic (CPC) is Lewis' S5, whereas its largest modal companion is the logic
T r i v = K ⊕ ( A ↔ ◻ A ) . {\displaystyle \mathbf {Triv} =\mathbf {K} \oplus (A\leftrightarrow \Box A).}
More examples:
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:
ρ : N E x t S 4 → E x t I P C , {\displaystyle \rho \colon \mathrm {NExt} \,\mathbf {S4} \to \mathrm {Ext} \,\mathbf {IPC} ,}
τ , σ : E x t I P C → N E x t S 4 . {\displaystyle \tau ,\sigma \colon \mathrm {Ext} \,\mathbf {IPC} \to \mathrm {NExt} \,\mathbf {S4} .}
It is easy to see that all three are monotone, and ρ ∘ τ = ρ ∘ σ {\displaystyle \rho \circ \tau =\rho \circ \sigma } is the identity function on ExtIPC. L. Maksimova and V. Rybakov have shown that ρ, τ, and σ are actually complete, join-complete and meet-complete lattice homomorphisms respectively. The cornerstone of the theory of modal companions is the Blok–Esakia theorem, proved independently by Wim Blok and Leo Esakia. It states
… excerpt ends here. Continue reading the full article.
