# zbMATH — the first resource for mathematics

A modal logic amalgam of classical and intuitionistic propositional logic. (English) Zbl 1444.03066
Summary: A famous result, conjectured by Gödel in 1932 and proved by J. C. C. McKinsey and A. Tarski [J. Symb. Log. 13, 1–15 (1948; Zbl 0037.29409)], says that $$\varphi$$ is a theorem of intuitionistic propositional logic IPC iff its Gödel-translation $$\varphi^\prime$$ 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 [the author, J. Log. Comput. 26, No. 5, 1769–1783 (2016; Zbl 1396.03032)], 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_{I P C} \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.

##### MSC:
 03B45 Modal logic (including the logic of norms) 03B05 Classical propositional logic 03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: