A modal logic amalgam of classical and intuitionistic propositional logic

TL;DR

This paper introduces a new modal logic L that embeds intuitionistic propositional logic (IPC) within a classical modal framework, extending previous results and demonstrating L's soundness, completeness, and its role as an amalgam of classical and intuitionistic logic.

Contribution

The paper extends an intuitionistic modal logic to a classical modal logic L that embeds IPC, showing L's conservativity over classical propositional logic and its algebraic semantics.

Findings

L is a conservative extension of CPC.

IPC can be embedded into L via the map φ ↦ □φ.

L is sound and complete with respect to special Heyting algebras.

Abstract

A famous result, conjectured by G\"odel in 1932 and proved by McKinsey and Tarski in 1948, says that $\varphi$ is a theorem of intuitionistic propositional logic IPC iff its G\"odel-translation $\varphi'$ is a theorem of modal logic S4. In this paper, we extend an intuitionistic version of modal logic S1+SP, introduced in our previous paper (S. Lewitzka, Algebraic semantics for a modal logic close to S1, J. Logic and Comp., doi:10.1093/logcom/exu067) to a classical modal logic L and prove the following: a propositional formula $\varphi$ is a theorem of IPC iff $\square\varphi$ is a theorem of L (actually, we show: $\Phi\vdash_{IPC}\varphi$ iff $\square\Phi\vdash_L\square\varphi$, for propositional $\Phi,\varphi$). Thus, the map $\varphi\mapsto\square\varphi$ 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.