A modal logic amalgam of classical and intuitionistic propositional logic

Abstract

A famous result, conjectured by Gödel in 1932 and proved by McKinsey and Tarski in 1948, says that $\phi$ is a theorem of intuitionistic propositional logic IPC iff its Gödel-translation ${\phi }^{\prime }$ 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 $\phi$ is a theorem of IPC iff $\square \phi$ is a theorem of L (actually, we show: $\Phi {⊢}_{IPC}\phi$ iff $\square \Phi {⊢}_L\square \phi$, for propositional $\Phi ,\phi$). Thus, the map $\phi \mapsto \square \phi$ 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.

18 pages

References in corpus (2)

• Denotational semantics for modal systems S3--S5 extended by axioms for propositional quantifiers and identity
• Algebraic semantics for a modal logic close to S1

Cited by in corpus (5)

• Another Combination of Classical and Intuitionistic Conditionals
• Epistemic extensions of combined classical and intuitionistic propositional logic
• Reasoning about proof and knowledge
• Access-based Intuitionistic Knowledge
• Combining intermediate propositional logics with classical logic