A modal logic amalgam of classical and intuitionistic propositional logic
Steffen Lewitzka · Journal of Logic and Computation · 2015
A famous result, conjectured by Gödel in 1932 and proved by McKinsey and Tarski in 1948, says that φ is a theorem of intuitionistic propositional logic IPC iff its Gödel-translation φ′ is a theorem of modal logic S4. In this article, we extend an intuitionistic version of modal logic S1 + SP, introduced in our previous paper [14], to a classical modal logic L and prove the following: a propositional formula φ is a theorem of IPC iff □φ is a theorem of L (actually, we show: Φ⊢IPCφ iff □Φ⊢L□φ, for propositional Φ,φ). Thus, the map φ↦□φ is an embedding of IPC into L, i.e. L contains a copy of IPC. Moreover, L is a conservative extension of classical propositional logic CPC. In this sense, L is an amalgam of CPC and IPC. We show that L is sound and complete w.r.t. a class of special Heyting algebras with a (non-normal) modal operator.