We investigate the proof theory of important families of logics that are variants and generalizations of modal logics. These logics have been applied in various areas of mathematics, epistemology, philosophy, and computer science (e.g. conditional logics in hypothetical and plausible reasoning, epistemic logics in reasoning about knowledge, and bunched implication logics in separation and sharing of resources).
Several types of proof systems (calculi) have been proposed for these logics falling into two categories: internal calculi, whose basic objects can be read as formulas of the logic (e.g. hypersequent and nested calculus), and external calculi, whose basic objects are formulas of a more expressive language which partially encode the logic's semantics (e.g. labelled and display calculi). Internal and external calculi possess different properties: the former are more suitable for establishing properties such as termination, interpolation, and optimal complexity, while external calculi are easier to find and permit easier proofs of completeness, cut admissibility, and countermodel generation (from a terminating calculus).
Internal and external calculi have been introduced essentially as two independent, occasionally opposing, streams in proof theory with varying degrees of success. For certain classes of logics, no internal calculi are known, while for others, optimal external calculi are known. An integrated and systematic study of internal and external calculi has not been carried out in the 30 years of research in this area. This project will address this gap, focusing on modal and related logics, where the status of many meta-logical properties concerning various classes of logics is open. We will systematically study the interrelationships in order to facilitate the exchange of results between the two types of calculi (e.g. interpolation, semantic completeness, and countermodel generation) and to provide new tools to tackle open problems concerning decidability, conservativity and axiomatisations.