A modal logic amalgam of classical and intuitionistic propositional logic
Steffen Lewitzka

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 is a theorem of intuitionistic propositional logic IPC iff its G\"odel-translation 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 is a theorem of IPC iff is a theorem of L (actually, we show: iff , 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
