Displaying Modal Logic pp 87-102 | Cite as

# Strong Cut-Elimination and Labelled Modal Tableaux

## Abstract

The method used in Chapter 4 to show that every displayable logic enjoys strong cut-elimination was derived from the proof of strong normalizability of typed λ-terms. It does not only apply to display calculi. The present chapter is devoted to a proof of strong cut-elimination in a labelled tableau calculus for the (constant domain) modal predicate logic **QS5**. Modal tableau calculi which build in the accessibility relation of possible worlds models were first introduced by Kripke [93] and were later ‘linearized’ by various authors, notably Fitting [62], [63], [64] and Mints [114]. As in Gabbay’s [68] theory of labelled deductive systems, the basic declarative unit of these tableau calculi is not just a formula A, but rather a *formula plus label* (*σ*, *A*). In the case of the modal logic **S5** the label *σ* may just be a single positive integer, whereas in general it is a non-empty finite sequence of positive integers. Moreover, for **S5** the accessibility relation between labels may be universal and hence neglected. In contrast to labelled tableaux, the modal tableau systems of, for example, Rautenberg [137] and Goré [74] do not use labelled formulas. For a general survey on tableau methods for modal and tense logics, see [79]. The use of labels allows to formulate tableau calculi for certain extensions of the minimal normal modal logic **K** by imposing constraints on accessibility and on occurrences and the shape of labels on tableau branches. These constraints may be regarded as structural in the sense of not referring to any connectives. In order to emphasize the relation to sequent calculi, we shall work with a tableau calculus **TQS5** based on the ordinary notion of a sequent. By defining suitable mappings on *cut-free* closed tableaux it can easily be shown that the result of dropping cut from **TQS5** is equivalent to Fitting’s tableau calculus for first-order **S5** with respect to provable formulas (see Section 7.5). Usually modal tableau calculi are formulated without a cut rule. The admissibility of cut is, however, of interest for constructive proofs of equivalence with Hilbert-type systems; compare [93, p. 82]. Moreover, non-constructive proofs of cut-elimination are of little appeal when it comes to extending the notion of formuals-as-types to modal logic (see, for instance, [28], [106]). It is this respect in which the present chapter may be seen to have significance.

## Preview

Unable to display preview. Download preview PDF.