Introduction

Abstract

This monograph deals with various selected aspects of proof systems for intensional logics, that is, modal logics in the broad sense, including, for instance, also subintuitionistic and constructive propositional logics with strong negation. But also certain variants of classical first-order logic will be considered from a modal perspective. The principal formalism to be developed and investigated is a certain refinement of Gentzen’s sequent calculus, namely Nuel Belnap’s display logic, DL, [16]. However, Dov Gabbay’s [67] related general framework of structured consequence relations, higher-level sequent systems for structured consequence relations, higher-arity display sequents, and a labelled modal tableau calculus for (constant domain) first-order S5 will also be examined. The common idea behind these proof-theoretic approaches is that many logical connectives can be introduced by natural operations on structures not as meagre as finite sets. Wheras Belnap considers terms in a natural extension of the structural language of Gentzen’s sequent calculus, Gabbay deals with complex datastructures, which essentially are assignments of formulas to individuals of first-order structures. These datastructures exemplify the general idea of Gabbay’s theory of labelled deductive systems, LDSs [68]. More specific and familiar examples of LDSs are provided by modal tableaux systems for labelled formulas and by typed lambda calculi.

Hilbert-style systems are easy to define ... but they are difficult to use. Gentzen systems reverse this situation by emphasizing the importance of inference rules ... .

J. Barwise [14, p. 37]