View article

The expansive use of logic in various domains, from areas of computer science and artificial intelligence, to philosophy and epistemology, has resulted in the development of many new logics. Along with the introduction of each new logic, it has proven crucial to design an analytic calculus for the logic. A calculus is said to be analytic when every formula occurring in a proof of the calculus is a subformula of the formula to be proved. Due to this property, such a calculus allows for the stepwise decomposition of formulae, which has proven useful in decidability and automated deduction procedures. The sequent calculus, introduced by Gerhard Gentzen in the 1930’s, has since been the preferred formalism for constructing analytic calculi due to its simplicity and ease of use. Nevertheless, for many modal and related logics the sequent calculus formalism proves itself too simple, and so, many new extensions of the sequent calculus have been proposed over the last 30 years. Such extensions are achieved by augmenting Gentzen’s sequent calculus with additional structure, thus increasing the complexity of the formalism but allowing for the construction of analytic calculi for a broader range of logics.

The multitude of new calculi were found to largely fall into two different camps:(i) internal calculi, where each object can be read as a formula of the logic and (ii) external calculi, where each object is a formula in a more expressive language partially encoding the semantics of the logic. Internal calculi have proven themselves useful in proving certain properties of logics such as interpolation and optimal complexity, whereas external calculi have proven useful …