---
tag: CGHFRWC8B3
kind: statement
role: theorem
name: Modal substitution theorem
sources:
  - wikipedia: en:51072@r1371231120
    locator: Natural deduction, section Classical and modal logics > Modal substitution theorem
    note: adopted
    mention: wikipedia://en/51072#3SS5
    sections: [Statement]
inventory: [RNXYF4WQM6]
---

## Statement

*If* Ω;⋅ ⊢ π<sub>1</sub> : *A* *and* Ω, *u*: (*A valid*) ; Γ ⊢ π<sub>2</sub> : *C*, *then* Ω;Γ ⊢ \[π<sub>1</sub>/*u*\] π<sub>2</sub> : *C*.

This framework of separating judgments into distinct collections of hypotheses, also known as *multi-zoned* or *polyadic* contexts, is very powerful and extensible; it has been applied for many different modal logics, and also for linear and other substructural logics, to give a few examples. However, relatively few systems of modal logic can be formalised directly in natural deduction. To give proof-theoretic characterisations of these systems, extensions such as labelling or systems of deep inference.

The addition of labels to formulae permits much finer control of the conditions under which rules apply, allowing the more flexible techniques of analytic tableaux to be applied, as has been done in the case of labelled deduction. Labels also allow the naming of worlds in Kripke semantics; (Simpson 1994) presents an influential technique for converting frame conditions of modal logics in Kripke semantics into inference rules in a natural deduction formalisation of hybrid logic. (Stouppa 2004) surveys the application of many proof theories, such as Avron and Pottinger's hypersequents and Belnap's display logic to such modal logics as S5 and B.