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. 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. Let A be a propositional intuitionistic formula. A modal formula T(A) is defined by induction on the complexity of A: As negation is in intuitionistic logic defined by A → ⊥ {displaystyle A o ot } , we also have 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. For any normal modal logic M which extends S4, we define its si-fragment ρM as 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= ho M} . Every superintuitionistic logic has modal companions. The smallest modal companion of L is where ⊕ {displaystyle 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 τ L ⊆ M ⊆ σ L {displaystyle au Lsubseteq Msubseteq 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