# A modal logic amalgam of classical and intuitionistic propositional logic

arXiv: https://arxiv.org/abs/1306.2068 · HTML: https://mlsanity.com/paper/1306.2068/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Jun 2013.

## Built on by (most cited first, 2 of 2)

- [From Knowledge to Conjectures: A Modal Framework for Reasoning about Hypotheses](https://mlsanity.com/paper/2508.07304/) (2025)
- [Belief, knowledge and evidence](https://mlsanity.com/paper/2304.01283/) (2023)

## Abstract (arXiv)

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 squarevarphi is a theorem of L (actually, we show: PhivdashIPCvarphi iff squarePhivdashLsquarevarphi, for propositional Phi,varphi). Thus, the map varphimapstosquarevarphi 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.