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

Journal of Logic and Computation


Theoretical Computer Science / Hardware and Architecture / Logic / Software


[10:21 17/7/2015 exv048.tex] LogCom: Journal of Logic and Computation Page: 1 1–12

A modal logic amalgam of classical and intuitionistic propositional logic

STEFFEN LEWITZKA, Universidade Federal da Bahia – UFBA, Instituto de

Matemática, Departamento de Ciência da Computação, Campus de Ondina, 40170-110 Salvador – BA, Brazil. E-mail: steffen@dcc.ufba.br


A famous result, conjectured by Gödel in 1932 and proved by McKinsey and Tarski in 1948, says that ϕ is a theorem of intuitionistic propositional logic IPC iff its Gödel-translation ϕ′ 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ϕ is a theorem of L (actually, we show: IPC ϕ iffLϕ, 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 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.

Keywords: Intuitionistic logic, modal logic, provability, algebraic semantics, combining classical and intuitionistic logic, non-Fregean logic. 1 Introduction

According to the informal Brouwer–Heyting–Kolmogorov semantics (BHK) of intuitionistic propositional logic (IPC), intuitionistic truth is provability: a formula is true if there is a proof for it. Logical connectives then have a constructive meaning. For instance, a proof of ϕ∨ψ is given by a proof of ϕ or by a proof of ψ . In an attempt to formalize BHK, Gödel [11] interprets IPC in a modal extension of classical propositional logic (namely Lewis system S4) by defining a translation ϕ →ϕ′ that maps any propositional formula ϕ to a modal formula ϕ′ such that the following holds: if ϕ is a theorem of IPC, then ϕ′ is a theorem of S4. Gödel also conjectured the converse, i.e. IPC ϕ ⇔ S4 ϕ′ (1.1) for any propositional ϕ. This conjecture was later proved by McKinsey and Tarski [16].1 Thus,

Brouwer’s intuitionistic logic, as axiomatized by Heyting, can be recovered from modal system S4 by the equivalence (1.1) above. However, since the Gödel translation ϕ →ϕ′ is not trivial, S4 contains

IPC only in indirect, codified form. In particular, the modal operator of system S=S4 cannot be seen as a predicate for intuitionistic truth in the following sense: ϕ is true in S iff ϕ belongs to a given prime theory of IPC (1.2) for any propositional ϕ.2 1For much more details and historical background, we refer the reader to [1, 17]. 2Of course, truth is a semantic notion which is defined relative to a given model. Recall that the set of formulas which are true at a given world of a Kripke model of intuitionistic logic forms a prime theory, and each prime theory corresponds to a world of a Kripke model. Hence, in intuitionistic logic, ‘ϕ is true’ means that ϕ belongs to a given prime theory of IPC. © The Author, 2015. Published by Oxford University Press. All rights reserved.

For Permissions, please email: journals.permissions@oup.com doi:10.1093/logcom/exv048

Journal of Logic and Computation Advance Access published July 20, 2015 at U niversity of Sussex on July 28, 2015 http://logcom .oxfordjournals.org/

D ow nloaded from [10:21 17/7/2015 exv048.tex] LogCom: Journal of Logic and Computation Page: 2 1–12 2 Classical and intuitionistic propositional logic

In this article, we present a modal logic L such that (1.2) above holds with S=L. Soundness of L then implies the right-to-left direction of the following equivalence (1.3). The left-to-right direction can easily be shown by an induction on the length of a derivation. For any propositional ϕ: IPC ϕ ⇔ Lϕ (1.3)

Actually, we will show the following stronger result: IPC ϕ ⇔ Lϕ, (1.4) for any set of propositional formulas ∪{ϕ}. Thus, derivations in IPC are mirrored by corresponding derivations in L by means of the modal operator. In particular, the mapping ϕ →ϕ defines an embedding of IPC into L. That is, L contains a copy of IPC and behaves in a similar way as a conservative extension. Moreover, L is a conservative extension of classical propositional logic CPC.

In this sense, L can be viewed as an amalgam or a combination of IPC and CPC. In the combined logic L, IPC is separated from CPC by means of the modal operator, which avoids the collapsing of both logics. Combinations of logics in a much more general context have been studied extensively over the last years (see [4] for an excellent overview). Known combining techniques largely rely on the concept of fibring originally introduced by Gabbay (see [8–10]). These techniques generally assume that the object logics are defined over different languages. The so-called collapsing problem was first identified in [8, 9] for the special case of combining intuitionistic and classical propositional logic: in the semantics of the combined logic, the logical connectives of the composed language have classical behaviour. That is, the combination results in a collapsing of intuitionistic logic into classical logic. A logical system that combines classical and intuitionistic logic avoiding the problem is found in [6]. A first general solution to the collapsing problem, based on modulated fibring, is presented in [5]. In [3], the authors propose cryptofibring semantics as a generalization of fibring semantics and show that this provides a solution to the collapsing problem. Other solutions to the problem are given by graph-theoretic fibring [18, 19] and, more recently, by a new method called meet combination of logics [20, 21].

The present article is not in the tradition of fibring or related techniques of combining logics, neither it pretends to compete with the sophisticated techniques developed in that research line. In fact, our approach relies on different assumptions and motivations, which makes a direct comparison to complex fibring techniques a difficult task. One of the main differences is the fact that our object logics IPC and CPC are given in exactly the same propositional language. In the combined system, the object logics then are distinguished by a modal operator. Semantically, the intuitionistic part of the amalgam is, roughly speaking, given by special Heyting algebras whereas the classical part is given by ultrafilters contained in those Heyting algebras. This represents a very compact semantical solution which, together with the mentioned syntactical simplifications, ensures that, in our view, the approach is technically simpler and less complex than known fibring techniques. We believe that the proposed solution can be adapted to similar cases of combining logics. To what extent this can be done and which are the limitations in comparison to fibring techniques, remains to be further investigated. The original motivation for the present approach was not to develop new combining techniques but rather to find a classical modal logic L with the properties (1.2)–(1.4) above. Of course, it would be nice to have a minimal logic with those properties. Lewis modal system S1 turns out to be a promising base. In our previous paper [14], we found an algebraic semantics for the slightly stronger system S1+SP. The semantics essentially relies on principles of non-Fregean logic [2] paired with the idea to identify strict equivalence (ϕ↔ψ) with propositional identity ϕ≡ψ . That is, we at U niversity of Sussex on July 28, 2015 http://logcom .oxfordjournals.org/