A modal logic amalgam of classical and intuitionistic propositional logic

作者：Lewitzka Steffen^*

来源：Journal of Logic and Computation, 2017, 27(1): 201-212.

DOI：10.1093/logcom/exv048

• Intuitionistic logic
• modal logic
• provability
• algebraic semantics
• combining classical and intuitionistic logic
• non-Fregean logic

A famous result, conjectured by Godel in 1932 and proved by McKinsey and Tarski in 1948, says that. is a theorem of intuitionistic propositional logic IPC iff its Godel-translation. psi' 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 [14], to a classical modal logic L and prove the following: a propositional formula. is a theorem of IPC iff square psi. is a theorem of L (actually, we show: Phi proves IPC. iff square proves L ., for propositional Phi,psi,.). Thus, the map. psi. proves square psi. 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.

• 出版日期2017-2