Power and Weakness of the Modal Display Calculus

Abstract

The present paper explores applications of Display Logic as defined in [1] to modal logic. Acquaintance with that paper is presupposed, although we will give all necessary definitions. Display Logic is a rather elegant proof-theoretic system that was developed to explore in depth the possibility of total Gentzenization of various propositional logics. By Gentzenization I understand the strategy to replace connectives by structures. Gentzenization is something of an ingenious optical trick because it uses a single symbol to mean different things depending on the place it occupies in the sequent. In the original Gentzen system it was the comma that had to be interpreted as and when to the left of the turnstile and as or when to the right. The interpretation of the structures oscillates between two logical symbols depending on whether it is in the antecedent or in the consequent. This is why we call symbols like comma Gentzen toggles. These two symbols between which this toggle switches are the Gentzen duals of each other. So, and and or are Gentzen duals. The strength of Display logic lies in a rather general cut-elimination theorem. In [10] and [9], Heinrich Wansing has refined these methods for modal logics; he showed that contrary to Belnap’s own Gentzenization of modal operators as binary structure operators, a unary one is more appropriate (not only from an esthetical point of view) and makes perfect sense semantically as well. The Gentzen dual of the modal operator □ is actually not — as one might expect — the. possibility operator ◇, but the backward looking possibility operator, denoted here by ◇. (To be consistent with that we write □ instead of □ and ◇ instead of ◇.) The corresponding toggle is denoted by •. The reason why this is so natural lies in the fact that it is the exact Display or Gentzen dual, for we have that the sequent •B ⊢ A and the sequent B ⊢ • A are equivalent if • is read as if in the antecedent and if it is read as 0 if in the consequent. Wansing uses this fact to display various modal and tense logics à la Belnap by providing some formula introduction rules and basic structural rules for K and Kt and then Gentzenizing the additional axioms. The benefit lies not only in the homogeneity with which all these systems are now handled and the rather clear intuitive background. The benefit lies in the possibility to use the general cut-elimination theorem of [1].