[a] [b] [c] [c] [c] [d] [e]

# Internal and External Calculi: Ordering the Jungle without Being Lost in
Translations

Tim S. Lyon0000-0003-3214-0828  ,  Agata Ciabattoni  ,  Didier Galmiche  ,
Dominique Larchey-Wendling  ,  Daniel Méry  ,  Nicola Olivetti  and  Revantha
Ramanayake  Technische Universität Dresden, Germany  timothy_stephen.lyon@tu-
dresden.de Vienna University of Technology, Austria<EMAIL_ADDRESS>Université
de Lorraine, CNRS, LORIA, France<EMAIL_ADDRESS>dominique.larchey-
<EMAIL_ADDRESS><EMAIL_ADDRESS>Aix-Marseille University, France
<EMAIL_ADDRESS>University of Groningen, The Netherlands
<EMAIL_ADDRESS>
###### Abstract.

This paper gives a broad account of the various sequent-based proof formalisms
in the proof-theoretic literature. We consider formalisms for various modal
and tense logics, intuitionistic logic, conditional logics, and bunched
logics. After providing an overview of the logics and proof formalisms under
consideration, we show how these sequent-based formalisms can be placed in a
hierarchy in terms of the underlying data structure of the sequents. We then
discuss how this hierarchy can be traversed using translations. Translating
proofs up this hierarchy is found to be relatively easy while translating
proofs down the hierarchy is substantially more difficult. Finally, we inspect
the prevalent distinction in structural proof theory between ‘internal
calculi’ and ‘external calculi’. It is observed that these classes resist a
rigorous separation, and we critically assess the properties that (calculi
from) these classes are purported to possess.

###### Key words and phrases:

Bunched implication, Conditional logic, Display, External calculus,
Hypersequent, Internal calculus, Intuitionistic logic, Labeled, Modal logic,
Nested, Proof theory, Sequent, Tense logic

## Introduction

The widespread application of logical methods in computer science,
epistemology, and artificial intelligence has resulted in an explosion of new
logics. These logics are more expressive than classical logic, allowing finer
distinctions and a direct representation of notions that cannot be well stated
in classical logic. For instance, they are used to express different modes of
truth (e.g. modal logics [BdRV01]) and to study different types of reasoning,
e.g. hypothetical/plausible reasoning (e.g. conditional logics [Lew73]) or
reasoning about the separation and sharing of resources (e.g. bunched
implication logics [Pym02]). Apart from formalizing reasoning, these logics
are also used to model systems and to prove properties about them, leading,
for example, to applications in software verification [McM18].

These applications require the existence of analytic calculi. Analytic calculi
consist solely of rules that compose (decompose, in the case of tableau
calculi) the formulae to be proved in a stepwise manner, and in particular,
the key rule of cut—used to simulate modus ponens—is not needed. As a result,
the proofs from an analytic calculus possess the subformula property: every
formula that appears (anywhere) in the proof is a subformula of the formulae
proved. This is a powerful restriction on the form of proofs, which can be
exploited to develop automated reasoning methods [Sla97] as well as prove
important (meta-)logical properties of the formalized logics such as
consistency [Gen35a, Gen35b], decidability [Dyc92], and interpolation [Mae60].

Since its introduction by Gentzen in the 1930’s and his seminal proof of the
Hauptsatz (see [Gen35a, Gen35b]), the sequent calculus has become the
preferred formalism for constructing analytic calculi. This is because the
sequent calculus is relatively simple and it does not require much technical
machinery (i.e. ‘bureaucracy’) to enable analyticity. The downside of this
simplicity is that the sequent calculus is not expressive enough to construct
analytic calculi for many logics of interest, thus necessitating the discovery
of new formalisms. In response, many proof-theoretic formalisms extending the
sequent calculus have been proposed over the last 50 years to define analytic
calculi for families of logics; these include hypersequent calculi [Avr96,
Min68], nested sequent calculi [Bul92, Kas94], bunched sequent calculi
[Pym02], display calculi [Bel82, Wan94], and labeled sequent calculi [Sim94,
Vig00]. Each of these proof-theoretic formalisms (or, _formalisms_ for short)
is characterized in terms of the standard notation it uses, the data
structures employed in sequents, the types of inference rules that normally
appear, and the types of properties ordinarily shared by the proof calculi
thereof (which serve as _instances_ of a formalism). As the notion is central
to this paper, we further remark that a proof-theoretic formalism is a
_paradigm_ in which calculi are built or defined, i.e. a formalism constitutes
the _way_ in which calculi are constructed, giving rise to a family
resemblance shared by systems within the same formalism.

In the literature, proof-theoretic formalisms and calculi have often been
classified into _internal_ or _external_. There is no formal definition of
these properties and the proof-theoretic community lacks consensus on how each
term should be precisely defined. Nevertheless, the literature abounds with
informal definitions of internal and external calculi. Typically, internal
calculi are described along multiple (sometimes intersecting, sometimes
conflicting) lines; e.g. internal calculi have been qualified as proof systems
omitting semantic elements from their syntax, or proof systems where every
sequent is translatable into an equivalent logical formula. Often times,
external calculi are defined as the opposite of internal calculi, and
therefore, have also been qualified in multiple ways. It has been claimed that
distinguishing internal and external calculi is useful because each type of
calculus has distinct properties making one type better suited for certain
applications than the other. For example, it has been claimed that internal
calculi are better suited for establishing properties such as termination,
interpolation, and optimal complexity, while external calculi are better
suited for counter-model generation and permit easier proofs of cut
admissibility and completeness [Vig00, Neg05].

Due to the diverse number of proof-theoretic formalisms and the categorization
of calculi into internal and external, a large body of work has been dedicated
to investigating the relationships between calculi within distinct formalisms
by means of _translations_. A translation is a function from one proof
formalism into another which extends in a natural way to yield structure-
preserving maps between derivations in the concrete calculi instantiating the
formalisms. The goal of this paper is twofold: (1) we map out the
relationships between various proof-theoretic formalisms by means of
translations and (2) we investigate the internal and external distinction in
light of these relationships.111We consider sequent-based formalisms in this
paper for generality as other types of proof systems, e.g. tableaux and
natural deduction systems, can be transformed into sequent calculi. Moreover,
sequent-based systems are easier to mechanize, meaning the systems we consider
have a higher degree of practical use. What we find is that proof-theoretic
formalisms sit within a hierarchy that increases in complexity from Gentzen-
style sequents up to labeled sequents, and is based upon the underlying data
structure of the sequents used in the system. We will argue that it is
‘easier’ to translate proofs up this hierarchy than down this hierarchy.
Furthermore, we will dispel myths about internal and external calculi,
explaining that the terms ‘internal’ and ‘external’ resist rigorous
definition, and clarifying what properties can actually be expected of proof
systems that are often qualified as ‘internal’ or ‘external’. To provide a
broad account of sequent-based formalisms and internal/external calculi we
consider a large number of formalisms and systems constructed for a wide array
of logics, including modal and tense logics, intuitionistic logic, conditional
logics, and bunched implication logic.

We identify five desiderata for proof-theoretic formalisms (see e.g., [Wan94,
Avr96]): (1) Generality: the formalism covers a sizable class of logics with
proof systems sharing desirable properties, (2) Uniformity: the formalism need
not be enriched to obtain a system for a logic within a given class, (3)
Modularity: a system for one logic within the considered class can be
transformed into a system for another, with properties preserved, by
adding/deleting rules or modifying the functionality of rules, (4)
Constructibility: a method is known for constructing a calculus for a given
logic in the considered class, and (5) Syntactic Parsimony: the data
structures used are as simple as required by the logic or purpose of the proof
systems.

When the desiderata (1)-(4) are satisfied, a proof formalism is expected to
generate large classes of proof calculi for logics on demand without requiring
substantial work on the side of the logician. The fifth desideratum is meant
to enforce that a formalism should produce calculi which are as simple as
required to improve their interpretability and the ease with which they may be
applied. However, the _purpose_ of a proof system, i.e. its use in a
particular application, may require the data structure of the sequent to be
enriched, and so, we note that it is sensible at times to trade syntactic
parsimony for complexity so the proof system is better adapted for a
particular application. For example, although nested sequents employ trees of
Gentzen-style sequents, they are better suited for counter-model extraction
than Gentzen-style sequent calculi, and so, if we aim to use our systems to
extract counter-models of formulae, then it is sensible to trade the simple
structure of Gentzen-style sequents for nested sequents.

It is not to be taken for granted that a single proof formalism can fulfill
all of the above requirements, which justifies the study of alternative proof
systems and formalisms with different properties, used for different purposes.
We will, throughout the course of the paper, discuss which formalisms satisfy
which desiderata to pinpoint distinctions between formalisms and motivate the
usage of one formalism relative to another.

This paper is organized as follows: In Section 1, we introduce the various
families of logics we will consider and their semantics, including modal and
tense logics, intuitionistic logic, conditional logics, and bunched logics. In
Section 2, we will explain the various sequent-based formalisms and specific
systems that have been introduced for these logics, giving a broad account of
the types of sequent systems that appear in the literature. In the subsequent
section (Section 3), we organize these proof-theoretic formalisms and systems
into a hierarchy and explain how to traverse this hierarchy by means of
translations. Lastly, in Section 4, we consider the internal and external
distinction, discuss the issues with defining these terms, and set the record
straight regarding what properties calculi deemed ‘internal’ or ‘external’ can
be expected to satisfy.

##  1\. Logical Preliminaries

To keep the paper self contained, we introduce the various logics whose proof
systems will be considered throughout the paper. In particular, we define the
languages and model-theoretic semantics for modal and tense logics,
intuitionistic logic, conditional logics, and bunched implication logics.

###  1.1. Modal Logics

The origin of modal logic is often attributed to the work of C.I. Lewis
[Lew18], who formulated a notion of strict implication in an attempt to
resolve certain paradoxes of material implication. Since then various modal
logics have been defined by expanding a base logic (e.g. classical or
intuitionistic logic) with _modalities_ , that is, logical operators that
qualify the truth of a proposition. _Normal modal logics_ extend classical
propositional logic through the incorporation of _alethic_ modalities, namely,
“it is possible that” (denoted by $\Diamond$) and “it is necessary that”
(denoted by $\Box$). For an in-depth treatment and presentation of such
logics, see Blackburn et al. [BdRV01].

Let us formally define the normal modal logics we consider. We let
$\mathsf{Prop}:=\\{p,q,r,\ldots\\}$ be a set of _propositional atoms_ (which
are occasionally annotated), and note that normal modal logics are extensions
of classical propositional logic, which makes use of formulae generated by the
following grammar in BNF:

$A::=p\ |\ \neg A\ |\ A\lor A\ |\ A\land A\ |\ A\rightarrow A$

where $p$ ranges over $\mathsf{Prop}$. We mention this language as classical
propositional logic will be discussed later on. It is well known that
disjunction and conjunction are definable in terms of $\neg$ and
$\rightarrow$, i.e. $A\lor B:=\neg A\rightarrow B$ and $A\land
B:=\neg(A\rightarrow\neg B)$. We mention this because the modal logics we
consider in this paper omit the use of $\lor$ and $\land$ as such connectives
are definable in terms of the others, and therefore, extraneous. To obtain
modal logics, we define the language $\mathcal{L}_{M}$ to be the set of
formulae generated via the following grammar in BNF:

$A::=p\ |\ \neg A\ |\ A\rightarrow A\ |\ \Box A$

where $p$ ranges over $\mathsf{Prop}$. Such formulae are interpreted over
_modal Kripke models_. We define such models below, and afterward, define how
formulae are interpreted over them.

[Modal Kripke Model] A _Kripke frame_ is defined to be an ordered pair
$F:=(W,R)$ such that $W$ is a non-empty set of points, called _worlds_ , and
$R\subseteq W\times W$ is the _accessibility relation_. A _modal Kripke model_
is defined to be a tuple $M=(F,V)$ such that $F$ is a Kripke frame and
$V:\mathsf{Prop}\to 2^{W}$ is a _valuation function_ mapping propositions to
sets of worlds.

[Semantic Clauses] Let $M=(W,R,V)$ be a modal Kripke model. We define a
forcing relation $\models$ such that

  * •

$M,w\models p$ iff $w\in V(p)$;

  * •

$M,w\models\neg A$ iff $M,w\not\models A$;

  * •

$M,w\models A\rightarrow B$ iff if $M,w\models A$, then $M,w\models B$;

  * •

$M,w\models\Box A$ iff for every $u\in W$, if $wRu$, then $M,u\models A$;

  * •

$M\models A$ iff for every $w\in W$, $M,w\models A$.

We define a formula $A\in\mathcal{L}_{M}$ to be _$\mathcal{L}_{M}$ -valid_ iff
for all modal Kripke models $M$, $M\models A$. We define the minimal normal
modal logic $\mathsf{K}$ to be the set of $\mathcal{L}_{M}$-valid formulae.

As is well-known in the domain of modal logics, certain formulae are valid on
a class of modal Kripke frames if and only if the accessibility relation of
those frames satisfies a certain property. This discovery led to the
formulation of _correspondence theory_ [BdRV01], which investigates
relationships between modal axioms and the properties possessed by modal
Kripke frames. In Figure 1, we display a few popular and well-studied
correspondences, and define two prominent modal logics based on such
properties as follows:

[$\mathsf{S4}$ and $\mathsf{S5}$] The modal logic $\mathsf{S4}$ is defined to
be the set of $\mathcal{L}_{M}$-valid formula over modal Kripke frames whose
relation is reflexive and transitive. The modal logic $\mathsf{S5}$ is defined
to be the set of $\mathcal{L}_{M}$-valid formula over modal Kripke frames
whose relation is reflexive and Euclidean.

Name | Frame Property | Modal Axiom
---|---|---
Reflexivity | $\forall wwRw$ | $\Box A\rightarrow A$
Symmetry | $\forall w,u(wRu\rightarrow uRw)$ | $A\rightarrow\Box\neg\Box\neg A$
Transitivity | $\forall w,v,u(wRv\land vRu\rightarrow wRu)$ | $\Box\Box A\rightarrow\Box A$
Euclideanity | $\forall w,v,u(wRv\land wRu\rightarrow vRu)$ | $\neg\Box A\rightarrow\Box\neg\Box A$
Figure 1. Frame properties and corresponding axioms.

We note that although $\mathsf{S5}$ is characterizable in terms of reflexive
and Euclidean Kripke models, i.e. Kripke models where the accessibility
relation forms an equivalence relation, the logic also admits a simplified
Kripke semantics that disregards the accessibility relation.

[Alternative $\mathsf{S5}$ Semantics] We define a _simplified modal Kripke
model_ to be a pair $M=(W,V)$ such that $W$ is a non-empty set of worlds and
$V:\mathsf{Prop}\to 2^{W}$ is a valuation function. We interpret modal
formulae over such models as follows:

  * •

$M,w\models\Diamond A$ iff there exists $u\in W$ such that $M,u\models A$;

  * •

$M,w\models\Box A$ iff for every $u\in W$, $M,u\models A$.

and note that (negated) propositional atoms, disjunctions, and conjunctions
are interpreted as in Definition 1.2 above.

It is straightforward to establish the following correspondence, which
demonstrates the equivalence between the two different semantic presentations
of $\mathsf{S5}$.

######  Proposition 1.

A formula $A$ is valid over the class of reflexive and Euclidean modal Kripke
frames iff $A$ is valid over the class of simplified modal Kripke models
(according to the alternative $\mathsf{S5}$ semantics).

###  1.2. Tense Logics

Tense logics were invented by Prior in the 1950’s [Pri57], and are types of
normal modal logics that not only include the $\Diamond$ and $\Box$
modalities, but the _converse modalities_ $\blacklozenge$ and $\blacksquare$.
These modalities are interpreted in a temporal manner, that is, $\Diamond$ is
read as “in some future moment,” $\Box$ is read as “in every future moment,”
$\blacklozenge$ is read as “in some past moment,” and $\blacksquare$ is read
as “in every past moment.” In this paper, we consider the _minimal tense logic
$\mathsf{Kt}$_ [BdRV01], whose language $\mathcal{L}_{T}$ is defined via the
following grammar in BNF:

$A::=p\ |\ \neg p\ |\ A\lor A\ |\ A\land A\ |\ \langle?\rangle A\ |\ [?]A$

where $p$ ranges over $\mathsf{Prop}$,
$\langle?\rangle\in\\{\Diamond,\blacklozenge\\}$, and
$[?]\in\\{\Box,\blacksquare\\}$. Formulae from $\mathcal{L}_{T}$ are in
negation normal form as this will simplify the sequent systems we consider
later on. Note that negation $\neg$ and implication $\rightarrow$ can be
defined as usual; see e.g. [CLRT21]. Like formulae in $\mathcal{L}_{M}$, we
interpret formulae from $\mathcal{L}_{T}$ over modal Kripke models (Definition
1.1).

[Semantic Clauses] Let $M=(W,R,V)$ be a modal Kripke model. We define a
forcing relation $\models$ such that

  * •

$M,w\models p$ iff $w\in V(p)$;

  * •

$M,w\models\neg p$ iff $w\not\in V(p)$;

  * •

$M,w\models A\lor B$ iff $M,w\models A$ or $M,w\models B$;

  * •

$M,w\models A\land B$ iff $M,w\models A$ and $M,w\models B$;

  * •

$M,w\models\Diamond A$ iff there exists a $u\in W$ such that $wRu$ and
$M,u\models A$;

  * •

$M,w\models\blacklozenge A$ iff there exists a $u\in W$ such that $uRw$ and
$M,u\models A$;

  * •

$M,w\models\Box A$ iff for every $u\in W$, if $wRu$, then $M,u\models A$;

  * •

$M,w\models\blacksquare A$ iff for every $u\in W$, if $uRw$, then $M,u\models
A$;

  * •

$M\models A$ iff for every $w\in W$, $M,w\models A$.

We define a formula $A\in\mathcal{L}_{T}$ to be _$\mathcal{L}_{T}$ -valid_ iff
for all modal Kripke models $M$, $M\models A$. We define the minimal tense
logic $\mathsf{Kt}$ to be the set of $\mathcal{L}_{T}$-valid formulae.

###  1.3. Intuitionistic Logic

Intuitionistic logic aims to capture the notion of constructive proof,
something which classical logic fails to do [Hey30]. For this reason
intuitionistic logic does not contain familiar classical axioms such as the
law of the excluded middle ($p\lor\lnot p$) and double negation elimination
($\lnot\lnot p\supset p$).

The language of intuitionistic logic $\mathcal{L}_{I}$ is the same as for
classical propositional logic, with the exception that implication $\supset$
must be included in the language as it is not definable in terms of the other
connectives. We define $\mathcal{L}_{I}$ by means of the following grammar in
BNF:

$A::=p\ |\ \bot\ |\ A\lor A\ |\ A\land A\ |\ A\supset A$

where $p$ ranges over $\mathsf{Prop}$. As usual, we define $\lnot
A:=A\supset\bot$. Intuitionistic formulae are interpreted over _intuitionistic
Kripke models_ , defined accordingly.

[Intuitionistic Kripke Model] An _intuitionistic Kripke frame_ is defined to
be an ordered pair $F:=(W,\leq)$ such that $W$ is a non-empty set of points,
called _worlds_ , and the _accessibility relation_ $\leq\ \subseteq W\times W$
is reflexive and transitive. A _intuitionistic Kripke model_ is defined to be
a tuple $M=(F,V)$ such that $F$ is an intuitionistic Kripke frame and
$V:\mathsf{Prop}\to 2^{W}$ is a _valuation function_ satisfying the
_persistence_ condition, that is, if $w\in V(p)$ and $wRu$, then $u\in V(p)$.

[Semantic Clauses] Given an intuitionistic Kripke model $M=(W,\leq,V)$, we
define a forcing relation $\models$ such that

  * •

$M,w\not\models\bot$;

  * •

$M,w\models p$ iff $w\in V(p)$;

  * •

$M,w\models A\lor B$ iff $M,w\models A$ or $M,w\models B$;

  * •

$M,w\models A\land B$ iff $M,w\models A$ and $M,w\models B$;

  * •

$M,w\models A\supset B$ iff for every $u\in W$, if $w\leq u$ and $M,u\models
A$, then $M,u\models B$;

  * •

$M\models A$ iff for every $w\in W$, $M,w\models A$.

We define a formula $A\in\mathcal{L}_{I}$ to be _intuitionistically-valid_ iff
for all intuitionistic Kripke models $M$, $M\models A$. We define
_intuitionistic logic_ $\mathsf{IL}$ to be the set of intuitionistically-valid
formulas.

A basic fact of intuitionistic logic is that it forms a proper subset of
classical logic. Conversely, via the double negation translation, classical
logic can be embedded into $\mathsf{IL}$ [Bus98]. Moreover, there is also a
natural embedding of (axiomatic extensions of) intuitionistic logic (called
_intermediate logics_) into (axiomatic extensions of) the modal logic
$\mathsf{S4}$ [Kri65].

###  1.4. Conditional Logics

Conditional logic deals with a hypothetical notion of implication that cannot
be represented by classical/material implication or by intuitionistic/strict
(modal) implication. Rather, implication is interpreted either
_counterfactually_ , e.g. “if A were the case, then B would be the case,” or
_typically_ , e.g. “Normally, if A then B.” Although the family of conditional
logics contains over 50 systems, we concentrate on the conditional logic of
counterfactual reasoning V defined by Lewis [Lew73]. We choose to focus our
attention on this conditional logic as its proof-theoretical treatment
requires and illustrates special techniques.

In Lewis’s account, the conditional operator is defined in terms of another
operator, referred to as _comparative plausibility_ and denoted $\preceq$. The
formula $A\preceq B$ states that “$A$ is at least as plausible as $B$.” The
conditional operator $A>B$ may then be defined as $(\bot\preceq
A)\lor\neg(A\land\neg B\preceq(A\land B))$, and is interpreted as, “$A$ is
impossible or $A\land\neg B$ is less plausible than $A\land B$.” We note that
this definition of $A>B$ can be simplified by replacing $A\land B$ by $A$ in
the second disjunct, yielding the official definition:

$A>B:=(\bot\preceq A)\lor\neg(A\land\neg B\preceq A)$

Conversely, we note that $\preceq$ can be defined in terms of the conditional
operator $>$. Our full language is defined via the following grammar in BNF:

$A::=p\ |\ \neg A\ |\ A\lor A\ |\ A\land A\ |\ A\rightarrow B\ |\ A\preceq A$

where $p$ ranges over $\mathsf{Prop}$.

An axiomatization of V in terms of $\preceq$ is given by extending an
axiomatization of classical propositional logic including _modus ponens_ (MP)
with the following set of axioms and rules:

  * •

(TR) $(A\preceq B)\land(B\preceq C)\rightarrow(A\preceq C)$

  * •

(CO) $(A\preceq B)\lor(B\preceq A)$

  * •

(CPA) $(A\preceq A\lor B)\lor(B\preceq A\lor B)$

  * •

(CPR) the rule

$\frac{A\rightarrow B}{B\preceq A}$

From a semantic point of view, V is characterized by special kinds of
neighborhood models, introduced by Lewis and called _sphere models_. In this
semantics, each world is assigned a system of spheres, i.e. a set of nested
neighborhoods. The intuition is that spheres represent degrees of
plausibility, so that worlds in smaller spheres are considered more plausible
than worlds contained solely in larger spheres.

[Sphere Model] A sphere model $M=(W,S,V)$ is a triple such that $W$ is a non-
empty set of worlds, $S:W\to 2^{2^{W}}$, $V:\mathsf{Prop}\to 2^{W}$ is a
valuation function, and the following conditions are satisfied, for every
$w\in W$:

  * •

for every $\alpha\in S(w)$, $\alpha\not=\emptyset$

  * •

for every $\alpha,\beta\in S(w)$, either $\alpha\subseteq\beta$ or
$\beta\subseteq\alpha$.

The elements of $S(w)$ are called _spheres_ and we use $\alpha,\beta,\ldots$
to denote them.

[Semantic Clauses] Given a sphere model $M=(W,S,V)$, we define a forcing
relation $\models$ such that

  * •

$M,w\models p$ iff $w\in V(p)$;

  * •

$M,w\models\neg A$ iff $M,w\not\models A$;

  * •

$M,w\models A\lor B$ iff $M,w\models A$ or $M,w\models B$;

  * •

$M,w\models A\land B$ iff $M,w\models A$ and $M,w\models B$;

  * •

$M,w\models A\rightarrow B$ iff if $M,w\models A$, then $M,w\models B$;

  * •

$M,w\models A\preceq B$ iff for all $\alpha\in S(w)$, if there exists
$u\in\alpha$ such that $M,u\models B$, then there exists $v\in\alpha$ such
that $M,v\models A$.

  * •

$M\models A$ iff for all $w\in W$, $M,w\models A$.

We define a formula $A$ to be _valid_ iff for any sphere model $M$, $M\models
A$, and we define the conditional logic V to be the set of all validities over
the class of sphere models.

Given a sphere model $M=(W,S,V)$, we find it useful to introduce the following
notation for a sphere $\alpha\in S(w)$:

  * •

$\alpha\models^{\exists}A$ iff $\exists w\in\alpha.M,w\models A$;

  * •

$\alpha\models^{\forall}A$ iff $\forall w\in\alpha.M,w\models A$.

With this notation, the semantic clauses for the comparative plausibility
operator and the conditional operator are equivalent to the clauses shown
below top and below bottom, respectively.

  * •

$M,w\models A\preceq B$ iff for all $\alpha\in S(w)$, if
$\alpha\models^{\exists}B$, then $\alpha\models^{\exists}A$;

  * •

$M,w\models A>B$ iff either for all $\alpha\in S(w)$,
$\alpha\not\models^{\exists}A$, or there is an $\alpha\in S(w)$ such that
$\alpha\models^{\exists}A$ and $\alpha\models^{\forall}A\to B$.

By imposing additional properties on sphere models, we obtain a family of
conditional logics. Later on, we will define calculi for conditional logics
that incorporate inference rules for the plausibility operator, taking the
conditional operator as defined.

###  1.5. Bunched Logics

Bunched logics are substructural logics222Logics that include connectives for
which at least one of the usual structural rules (weakening, contraction,
exchange, associativity) does not hold. that arised from mixing different
kinds of connectives associated with a resource aware interpretation. In this
paper we focus on the logic of bunched implications ($\mathsf{BI}$) [OP99,
Pym02], which combines propositional intuitionistic logic with intuitionistic
multiplicative linear logic. More formally, the set of formulae of
$\mathsf{BI}$, denoted $\mathsf{Fm}$, is given by the following grammar in
BNF:

$A::=p\mid\underbrace{\makebox[10.76385pt]{$\top{\scriptscriptstyle\mathfrak{m}}$}\mid
A\mathbin{\makebox[6.45831pt]{$\ast$}}A\mid
A\mathbin{\makebox[9.68747pt]{$-\ast$}}A}_{\text{multiplicatives}}\mid\underbrace{\makebox[10.76385pt]{$\top{\scriptscriptstyle\mathfrak{a}}$}\mid\bot\mid
A\mathbin{\makebox[6.45831pt]{$\wedge$}}A\mid
A\mathbin{\makebox[6.45831pt]{$\vee$}}A\mid
A\mathbin{\makebox[9.68747pt]{$\supset$}}A}_{\text{additives}}$

where $p$ ranges over $\mathsf{Prop}$.

$\mathsf{BI}$ admits various forcing semantics [Pym02], called _resource
semantics_ , that are more elaborated than Kripke models for intuitionistic
logic or for the modal logics $\mathsf{K}$, $\mathsf{S4}$, or $\mathsf{S5}$.
The most intuitive and widespread resource semantics for $\mathsf{BI}$ is the
monoid based Kripke semantics that arises from the definition of a
(multiplicative) resource composition $\otimes$ on worlds, viewed as
resources. The monoid based Kripke semantics can be generalized to a
relational semantics [GMP05] replacing both the accessibility $\sqsubseteq$
and the monoidal composition $\otimes$ with a ternary relation $R$ on worlds à
la Routley-Meyer (thus reading
$w\mathbin{\otimes}w^{\prime}\mathrel{\sqsubseteq}u$ as a particular case of
$Rww^{\prime}u$).

The standard monoid based Kripke semantics [GMP05] requires only one resource
composition reflecting the properties of the multiplicative connectives. The
specifics of the additive connectives are implicitly reflected in their
forcing clauses using the properties of the accessibility relation. However,
in this paper, we follow [GMM19] and use a monoid based Kripke semantics in
which we add a second (additive) resource composition $\oplus$ that explicitly
reflects the syntactic behaviour of $\mathbin{\makebox[6.45831pt]{$\wedge$}}$
into the semantics.

[Resource Monoid] A _resource monoid (RM)_ is a structure
$M=(M,\otimes,1,\oplus,0,\infty,\sqsubseteq)$ where $(M,\otimes,1)$,
$(M,\oplus,0)$ are commutative monoids and $\sqsubseteq$ is a preordering
relation on $M$ such that:

  * •

for all $w\in M$, $w\mathrel{\sqsubseteq}\infty$ and
$\infty\mathrel{\sqsubseteq}\infty\mathbin{\otimes}w$;

  * •

for all $w,u\in M$, $w\mathrel{\sqsubseteq}w\mathbin{\oplus}u$ and
$w\mathbin{\oplus}w\mathrel{\sqsubseteq}w$;

  * •

$\text{if }w\mathrel{\sqsubseteq}u\text{ and
}w^{\prime}\mathrel{\sqsubseteq}u^{\prime}\text{, then
}w\mathbin{\otimes}w^{\prime}\mathrel{\sqsubseteq}u\mathbin{\otimes}u^{\prime}\text{
and
}w\mathbin{\oplus}w^{\prime}\mathrel{\sqsubseteq}u\mathbin{\oplus}u^{\prime}$.

Let us remark that the conditions of Definition 1.5 imply that $\infty$ and
$0$ respectively are greatest and least elements and that $\oplus$ is
idempotent.

[Resource Interpretation] Given a resource monoid $M$, a _resource
interpretation (RI) for $M$_, is a function
$\mathop{[}-\mathop{]}:\mathsf{Fm}\longrightarrow 2^{M}$ satisfying
$\forall\,p\in\mathsf{Prop}$, $\infty\in\mathop{[}p\mathop{]}$ and
$\forall\,w,u\in M$, if $w\in\mathop{[}p\mathop{]}$ and
$w\mathrel{\sqsubseteq}u$, then $u\in\mathop{[}p\mathop{]}$.

[Kripke Resource Model] A _Kripke resource model (KRM)_ is a structure
$\mathcal{K}=(M,\models,\mathop{[}-\mathop{]})$ where $M$ is a resource
monoid, $\mathop{[}-\mathop{]}$ is a resource interpretation and $\models$ is
a forcing relation such that:

  * •

${M,w\models p}$ iff $w\in\mathop{[}p\mathop{]}$;

  * •

${M,w\models\bot}$ iff $\infty\mathrel{\sqsubseteq}w$;
${M,w\models\makebox[10.76385pt]{$\top{\scriptscriptstyle\mathfrak{a}}$}}$ iff
$0\mathrel{\sqsubseteq}w$;
${M,w\models\makebox[10.76385pt]{$\top{\scriptscriptstyle\mathfrak{m}}$}}$ iff
$1\mathrel{\sqsubseteq}w$;

  * •

${M,w\models A\mathbin{\makebox[6.45831pt]{$\ast$}}B}$ iff for some
$u,u^{\prime}$ in $M$ such that
$u\mathbin{\otimes}u^{\prime}\mathrel{\sqsubseteq}w$, ${M,u\models A}$ and
${M,u^{\prime}\models B}$;

  * •

${M,w\models A\mathbin{\makebox[6.45831pt]{$\wedge$}}B}$ iff for some
$u,u^{\prime}$ in $M$ such that
$u\mathbin{\oplus}u^{\prime}\mathrel{\sqsubseteq}w$, ${M,u\models A}$ and
${M,u^{\prime}\models B}$;

  * •

${M,w\models A\mathbin{\makebox[9.68747pt]{$-\ast$}}B}$ iff for all
$u,u^{\prime}$ in $M$ such that ${M,u\models A}$ and
$w\mathbin{\otimes}u\mathrel{\sqsubseteq}u^{\prime}$, ${M,u^{\prime}\models
B}$;

  * •

${M,w\models A\mathbin{\makebox[9.68747pt]{$\supset$}}B}$ iff for all
$u,u^{\prime}$ in $M$ such that ${M,u\models A}$ and
$w\mathbin{\oplus}u\mathrel{\sqsubseteq}u^{\prime}$, ${M,u^{\prime}\models
B}$;

  * •

${M,w\models A\mathbin{\makebox[6.45831pt]{$\vee$}}B}$ iff ${M,w\models A}$ or
${M,w\models B}$.

A formula $A$ is valid in the Kripke resource semantics iff ${M,1\models A}$
in all Kripke resource models.

Let us call $\mathsf{dmKRS}$ the Kripke resource semantics based on double
monoids as defined in this section (and first introduced in [GMM19]) and call
$\mathsf{smKRS}$ the standard one based on single monoids (as defined in
[GMP05]). The $\mathsf{smKRS}$ is recovered from the $\mathsf{dmKRS}$ by
erasing all references to $\oplus$ in Definition 1.5 and replacing the forcing
clauses for the additive connectives in Definition 1.5 with the following
ones:

  * •

${M,w\models\makebox[10.76385pt]{$\top{\scriptscriptstyle\mathfrak{a}}$}}$ iff
always;

  * •

${M,w\models A\mathbin{\makebox[6.45831pt]{$\wedge$}}B}$ iff ${M,w\models A}$
and ${M,w\models B}$;

  * •

${M,w\models A\mathbin{\makebox[9.68747pt]{$\supset$}}B}$ iff for all $u$ in
$M$ such that $w\mathrel{\sqsubseteq}u$, if ${M,u\models A}$ then ${M,u\models
B}$;

The forcing clauses for the additive connectives might seem more natural in
the $\mathsf{smKRS}$ as they convey their intuitive interpretation in terms of
resource sharing (see [Pym02] for details). Indeed, it is immediately seen
that $A\mathbin{\makebox[6.45831pt]{$\wedge$}}B$ is about $A$ and $B$ sharing
the same resource (namely, the resource $w$ in ${M,w\models
A\mathbin{\makebox[6.45831pt]{$\wedge$}}B})$. Let us remark that the
interpretation of the multiplicative connectives in terms of resource
separation ($A\mathbin{\makebox[6.45831pt]{$\ast$}}B$ holds for resource $w$
if it can be split into two resources $u$ and $u^{\prime}$, one satisfying $A$
and the other satisfying $B$) remains the same in both semantics. Let us also
mention that the interpretation of $\mathsf{BI}$ formulas in terms of resource
sharing and separation is one of the key differences with Linear Logic [Gir87]
and its interpretation of formulas in terms of resource accounting
(consumption and production).

Although (arguably) less intuitive, the $\mathsf{dmKRS}$ clearly makes the
presentation of the semantics more uniform as the differences between the
additive and multiplicative connectives are captured at the level of the
algebraic properties that the corresponding monoidal operators should satisfy
(e.g., idempotence for $\oplus$ but not for $\otimes$) and not at the level of
the forcing clauses which can therefore be formulated in a similar way. As we
shall see later in Section 2.4 it also makes the $\mathsf{dmKRS}$ more in tune
with the bunched sequent calculus of $\mathsf{BI}$ in which the differences
between the additive and multiplicative connectives are handled at the level
of the structural rules that the connectives should satisfy and not at the
level of the logical rules (which share a similar form).

##  2\. An Overview of the Proof-Theoretic Jungle

System Type | Data Structure of Sequent
---|---
Labeled Sequents | Graph of Gentzen Sequents
Display Sequents | (Pairs of)(Poly-)Tree(s) of
| Gentzen Sequents
Nested, Tree-hypersequents, | Tree of Gentzen Sequents
& Bunched Sequents |
2-Sequents | Linear Graph of Gentzen Sequents
& Linear Nested Sequents |
Hypersequents | (Multi-)Set of Gentzen Sequents
Gentzen Sequents | (Pairs of)(Multi-)Set(s)
Figure 2. Common Sequent Systems and Data Structure of Sequents.

We give a broad overview of the various sequent-based formalisms that have
come to prominence as generalizations of Gentzen’s sequent calculi [Gen35a,
Gen35b]. Each formalism extends Gentzen-style sequent systems in some way by
enriching the data structure employed in sequents. In particular, starting
with (1) standard Gentzen-style sequent systems (which are the least complex),
we describe (2) the formalism of hypersequents, which are multisets of
Gentzen-style sequents [Avr96, Min68], (3) 2-sequents and linear nested
sequents, which are sequences of Gentzen-style sequents [Mas92, Lel15], (4)
bunched sequents, which use treelike structures called “bunches” [Pym02], (5)
nested sequents, which are trees of Gentzen-style sequents [Bul92, Kas94], (6)
display sequents, which are (pairs of) polytrees of Gentzen-style sequents
[Bel82, Wan94], and (6) labeled sequents, which are graphs of Gentzen-style
sequents [Sim94, Vig00]. Based on the types of sequents employed, such systems
form a hierarchy of increasing complexity, which is presented in Figure 2.
Throughout the section, we detail which of the five desiderata (mentioned in
Section Introduction) each formalism tends to satisfy as well as the typical
properties systems within each formalism typically possess.

###  2.1. Gentzen Sequent Systems

The sequent calculi by Gentzen [Gen35a, Gen35b] for classical and
intuitionistic logic are fundamental to the domain of proof theory. We begin
by recalling the sequent calculus for classical logic. A sequent is an object
of the form $\Gamma\Rightarrow\Delta$ where $\Gamma$ and $\Delta$ are
(possibly empty) sequences of formulae. We call $\Gamma$ the _antecedent_ and
$\Delta$ the _consequent_ of the sequent. Each sequent
$\Gamma\Rightarrow\Delta$ with $\Gamma=\\{A_{1},\ldots,A_{m}\\}$ and
$\Delta=\\{B_{1},\ldots,B_{n}\\}$ can be interpreted as a formula of the
following form:

$\tau(\Gamma\Rightarrow\Delta):=(A_{1}\land\cdots\land
A_{m})\rightarrow(B_{1}\lor\cdots\lor B_{n})$

When $m=0$, the empty conjunction is interpreted as $\top$, and when $n=0$,
the empty disjunction is interpreted as $\bot$.

A sequent calculus contains axioms, also called _initial sequents_ , and rules
to derive sequents from sequents. The latter are divided into _logical_ rules
that introduce complex formulae in either the antecedent or consequent of a
sequent, and _structural_ rules which modify the structure of the
antecedent/consequent, without changing the formulae themselves. Figure 3
contains the axiom $(id)$ and the logical rules for the sequent calculus
$\mathsf{S(CP)}$ for classical propositional logic.

$(id)$ $\Gamma,p\Rightarrow p,\Delta$ |  $\Gamma,A\Rightarrow\Delta$ $(\neg_{r})$ $\Gamma\Rightarrow\neg A,\Delta$
---|---

$\Gamma,A\Rightarrow\Delta$ $\Gamma,B\Rightarrow\Delta$ $(\lor_{l})$ $\Gamma,A\lor B\Rightarrow\Delta$ |  $\Gamma\Rightarrow A,\Delta$ $\Gamma\Rightarrow B,\Delta$ $(\land_{r})$ $\Gamma\Rightarrow A\land B,\Delta$
---|---

$\Gamma\Rightarrow A,B,\Delta$ $(\lor_{r})$ $\Gamma\Rightarrow A\lor B,\Delta$ |  $\Gamma,A\Rightarrow B,\Delta$ ($\rightarrow_{r}$) $\Gamma\Rightarrow A\rightarrow B,\Delta$
---|---

Figure 3. Axioms and logical rules for the sequent calculus $\mathsf{S(CP)}$.

The structural rules for $\mathsf{S(CP)}$ are displayed in Figure 4. The
_exchange_ rules ($e_{l}$) and ($e_{r}$) re-order the formulae on each side of
a sequent, which has the effect that the order of formulae is irrelevant and
the antecedent and consequent of a sequent can be interpreted as multisets.
The _weakening_ rules ($wk_{l}$) and ($wk_{r}$) introduce formulae into the
antedecdent and consequent of a sequent, while the _contraction_ rules
($cr_{l}$) and ($cr_{r}$) remove additional copies of formulae. The $(cut)$
rule can be seen as a generalization of modus ponens and has a special status,
namely, it encodes the transitivity of deduction. Observe that the $(cut)$
rule is not analytic, as the premises contain an arbitrary formula that
disappears in the conclusion. It is important to notice that all structural
rules, and in particular the $(cut)$ rule, are _admissible_ in the calculus
$\mathsf{S(CP)}$, meaning that if the premises are derivable in the calculus,
then so is the conclusion. By this fact, structural rules are recognized to be
unnecessary for deduction as they only capture properties of sequents.

Let us now fix some terminology that will be used throughout the remainder of
the paper. We define a _derivation_ $\mathcal{D}$ of a sequent $S$ to be a
(finite, upward) tree whose nodes are sequents satisfying the following
conditions: (1) the root of $\mathcal{D}$ is the sequent $S$, and (2) for
every node $S^{\prime}$ with children nodes $S_{1},\ldots,S_{n}$, there is an
instance of a rule $(r)$ of the following form:

$S_{1}$ $\cdots$ $S_{n}$ $(r)$ $S^{\prime}$

Moreover, we say that a derivation $\mathcal{D}$ of $S$ is a _proof_ of $S$ if
all the leaves of $\mathcal{D}$ are axioms. The _height_ of a derivation is
equal to be the number of sequents along a maximal path from the root to a
leaf. In a rule, we define the _principal formulae_ to be those explicitly
displayed in the conclusion, and the _auxiliary formulae_ to be those
explicitly mentioned in the premise(s). For example, $A\rightarrow B$ is the
principal formula in $(\rightarrow_{l})$ and $A$ and $B$ are the auxiliary
formulae. By _proof-search_ we usually mean an algorithm that proceeds by
applying inference rules bottom-up with the goal of constructing a proof.

$\Gamma_{1},A,B,\Gamma_{2}\Rightarrow\Delta$ ($e_{l}$) $\Gamma_{1},B,A,\Gamma_{2}\Rightarrow\Delta$ |  $\Gamma\Rightarrow\Delta$ ($wk_{r}$) $\Gamma\Rightarrow\Delta,A$
---|---

$\Gamma,A,A\Rightarrow\Delta$ ($cr_{l}$) $\Gamma,A\Rightarrow\Delta$ |  $\Gamma\Rightarrow A,\Delta$ $\Gamma,A\Rightarrow\Delta$ $(cut)$ $\Gamma\Rightarrow\Delta$
---|---

Figure 4. Structural rules for the sequent calculus $\mathsf{S(CP)}$.

The calculus $\mathsf{S(CP)}$ has some important properties that set it as an
“ideal” proof system, which we enumerate and elaborate on below. We note that
the following terminology will also be applied to the other kinds of sequent-
style systems we consider later on.

  * •

_Analyticity_ : the premises of each rule only contain subformulae of the
conclusion. Thus, if we do not consider multiple occurrences of the same
formulae (i.e. we consider a sequent as a pair of sets), given a sequent $S$
at the root of a derivation $\mathcal{D}$, there are only finitely many
different sequents that can occur in $\mathcal{D}$. This follow from the
redundancy of the cut rule, i.e. _cut-elimination_ , meaning every proof
containing applications of $(cut)$ can be transformed into a $(cut)$-free
proof of the same conclusion [Gen35a, Gen35b].

  * •

_Termination_ : the premises of each rule are less complex than the
conclusion. We can see that this property holds in $\mathsf{S(CP)}$ (without
structural rules) since the auxiliary formulae are always less complex than
the principal formulae. This property together with analyticity ensures that
proof-search always terminates, that is, every branch of a derivation
$\mathcal{D}$ terminates with an axiom or an unprovable sequent (usually
containing only atoms).

  * •

_Invertibility_ : if the conclusion of a rule is derivable, then its premises
are derivable. By this property, the order of bottom-up applications of rules
during proof-search does not matter: either we obtain a proof of the root
sequent, or we get a (finite) derivation containing an unprovable sequent as a
leaf. When this property is present, backtracking (i.e. searching for
alternative proofs) is unnecessary during proof-search.

  * •

_Counter-model generation_ : if proof-search yields a derivation $\mathcal{D}$
that is not a proof of the conclusion, then there exists an unprovable sequent
as a leaf which can be used to define a counter-model of the conclusion. In
the case of $\mathsf{S(CP)}$, if $\Gamma\Rightarrow\Delta$ is such a leaf in a
derivation $\mathcal{D}$, then $\Gamma\cap\Delta=\emptyset$, and one can
define a propositional evaluation ‘$V(p)=\textbf{t}$ iff $p\in\Gamma$’ that
serves as a counter-model of the conclusion of $\mathcal{D}$.

The calculus $\mathsf{S(CP)}$ is ideal in the sense that it satisfies the
above four properties; as a consequence, the calculus provides a decision
procedure for classical propositional logic. Proof-search is carried out by
building _just one_ derivation that will either be a proof, or from which a
counter-model may be extracted, of the formula/sequent to check (i.e. the
conclusion). Furthermore, the decision procedure based on the calculus has an
optimal complexity ($\mathrm{CoNP}$).

$(id)$ $\Gamma,p\Rightarrow p,\Delta$ |  $(\bot_{l})$ $\Gamma,\bot\Rightarrow\Delta$
---|---

$\Gamma,A\Rightarrow\Delta$ $\Gamma,B\Rightarrow\Delta$ $(\lor_{l})$ $\Gamma,A\lor B\Rightarrow\Delta$ |  $\Gamma\Rightarrow A,B,\Delta$ $(\lor_{r})$ $\Gamma\Rightarrow A\lor B,\Delta$
---|---

$\Gamma,A,B\Rightarrow\Delta$ $(\land_{l})$ $\Gamma,A\land B\Rightarrow\Delta$ |  $\Gamma,A\Rightarrow B$ $(\supset_{r})$ $\Gamma\Rightarrow A\supset B,\Delta$
---|---

$\Gamma,A\supset B,B\Rightarrow\Delta$ $\Gamma,A\supset B\Rightarrow A,\Delta$
$(\supset_{l})$ $\Gamma,A\supset B\Rightarrow\Delta$
---

Figure 5. The Gentzen-style sequent system $\mathsf{S(IL)}$ for intuitionistic
logic.

Gentzen’s sequent systems are also flexible enough to capture other logics.
For example, intuitionistic logic can be provided a sequent calculus by making
simple modifications to $\mathsf{S(CP)}$. The calculus $\mathsf{S(IL)}$, shown
in Figure 5, is a sequent calculus for intuitionistic logic. Originally,
Gentzen obtained a sequent calculus for intuitionistic logic by imposing a
restriction on the sequent calculus for classical logic, namely, only sequents
with at most one formula in the consequent (viz. sequents
$\Gamma\Rightarrow\Delta$ such that $|\Delta|\leq 1$) could be used in
derivations. However, Gentzen’s restriction invalidates certain admissibility
and invertibility properties, which can be regained by swapping the
$(\rightarrow_{l})$ and $(\rightarrow_{l})$ rules with the $(\supset_{l})$ and
$(\supset_{r})$ rules shown in Figure 5. The calculus $\mathsf{S(IL)}$ is a
variant of Gentzen’s sequent calculus for intuitionistic logic that has all
structural rules, including $(cut)$, admissible.

The calculus $\mathsf{S(IL)}$ is analytic, though not terminating as the
premises of a rule may be as complex as the conclusion as witnessed by the
premises of ($\supset_{l}$). Additionally, the ($\supset_{r}$) rule is not
invertible, which is an impediment to proof-search. In particular, if proof-
search constructs a derivation that is not a proof, then a proof may still
exist and the constructed derivation may not provide a counter-model of the
conclusion. Due to analyticity a decision procedure can still be obtained in
principle, however, the procedure will also require loop checking which
diminishes its efficiency. We find that although Gentzen’s sequent formalism
satisfies syntactic parsimony to a high degree, the formalism lacks uniformity
and modularity since simple modifications to a calculus can nullify important
properties. In addition, although Gentzen-style sequent calculi have been
provided for many logics, the formalism is not general enough to yield cut-
free systems for many logics of interest (e.g. $\mathsf{S5}$ and bi-
intuitionistic logics [BG07]). These facts motivate the search for more
expressive formalisms that satisfy our important desiderata.

###  2.2. Hypersequents

Introduced independently by Mints [Min68], Pottinger [Pot83], and Avron
[Avr87], hypersequent systems are a simple generalization of Gentzen’s sequent
formalism. A hypersequent is a set of “$\mid$”- separated sequents, usually
interpreted as a disjunction at the meta-level, that is, a _hypersequent_ is a
multiset of the form:

$\Gamma_{1}\Rightarrow\Delta_{1}\;\mid\;\dots\;\mid\;\Gamma_{n}\Rightarrow\Delta_{n}$

where, for each $1\leq i\leq n$, $\Gamma_{i}\Rightarrow\Delta_{i}$ is a
Gentzen-style sequent, called a _component_ of the hypersequent.

As with ordinary sequent calculi, the inference rules of hypersequent calculi
consist of initial hypersequents (i.e. axioms), logical rules, and structural
rules, which includes a cut rule. These inference rules are usually presented
as rule schemata. A concrete instance of a rule is obtained by instantiating
the schematic variables with concrete formulae. In the case of hypersequents,
the rule schema may also contain schematic context variables for side
hypersequents, denoted by $G$ or $H$, representing (possibly empty)
hypersequents. The logical and structural rules are divided into internal and
external rules. The internal rules deal with formulae within one component of
the conclusion. Examples of internal structural rules are the ordinary rules
of weakening and contraction of the sequent calculus (augmented with the side
hypersequents). Examples of external structural rules are external weakening
($ew$), and external contraction ($ec$), which can be seen in Figure 6. These
behave like weakening and contraction over whole components of hypersequents.
The hypersequent structure opens the possibility to define new external
structural rules that allow for the “exchange of information” between
different sequents. It is this possibility which increases the expressive
power of hypersequent calculi compared to ordinary, Gentzen-style sequent
calculi.

One such rule, is the ($s5^{\prime}$) rule, shown in Figure 6, that when added
to the hypersequent version of the sequent calculus for $\mathsf{S4}$ (i.e.
adding a hypersequent context to all rules) allows the Euclidean axiom
$\mathsf{5}$ of the logic $\mathsf{S5}$ to be derived:

tensy  $\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
13.88872pt\hbox{$\displaystyle\penalty 1\Box A\Rightarrow\Box\neg\Box A,\Box
A$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=111.38847pt\hbox{\kern
3.00003pt${(s5^{\prime})}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Box
A\Rightarrow\;\mid\;\Rightarrow\Box\neg\Box A,\Box A$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=164.61261pt\hbox{\kern
3.00003pt${(\neg_{r})}$}}}\hbox{\kern
22.44542pt\hbox{$\displaystyle\Rightarrow\neg\Box
A\;\mid\;\Rightarrow\Box\neg\Box A,\Box A$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=215.95796pt\hbox{\kern
3.00003pt${(\Box_{r})}$}}}\hbox{\kern
33.53476pt\hbox{$\displaystyle\Rightarrow\Box\neg\Box A,\Box
A\;\mid\;\Rightarrow\Box\neg\Box A,\Box A$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=268.41443pt\hbox{\kern
3.00003pt${(ec)}$}}}\hbox{\kern
101.42946pt\hbox{$\displaystyle\Rightarrow\Box\neg\Box A,\Box A$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=319.39488pt\hbox{\kern
3.00003pt${(\neg_{l})}$}}}\hbox{\kern 122.75307pt\hbox{$\displaystyle\neg\Box
A\Rightarrow\Box\neg\Box A$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$
${(\rightarrow_{l})}$ $\displaystyle\Rightarrow\neg\Box A\to\Box\neg\Box A$

The hypersequent framework allowed the introduction of cut-free calculi for
logics not having a cut-free sequent calculus, e.g. $\mathsf{S5}$ [Pog08].
Moreover, the framework supported the systematic and algorithmic
transformation of large classes Hilbert axioms and frame properties into cut-
free hypersequent calculi for substructural and intermediate logics [CGT08,
CST09] and modal logics [Lah13, Lel16]. Therefore, the hypersequent formalism
can be seen to satisfy our five desiderata to a large degree: with only a
basic increase in syntactic complexity from that of Gentzen-style sequents,
hypersequent systems with favorable properties (e.g. analyticity) can be
algorithmically generated for wide classes of logics, thus demonstrating
generality, uniformity, modularity, and constructibility. Nevertheless, there
are logics for which the hypersequent formalism is ill-suited (e.g. the tense
logic $\mathsf{Kt}$ and some modal logics characterized by geometric frame
conditions [Sim94]), showing that the generality of the formalism is limited
in scope.

$G$ $(ew)$ $G\;\mid\;\Gamma\Rightarrow\Delta$
---

$G\;\mid\;\Gamma\Rightarrow\Delta\;\mid\;\Gamma\Rightarrow\Delta$ $(ec)$
$G\;\mid\;\Gamma\Rightarrow\Delta$
---

$G\;\mid\;\square\Gamma,\Gamma^{\prime}\Rightarrow\Delta$ $(s5^{\prime})$
$G\;\mid\;\square\Gamma\Rightarrow\;\mid\;\Gamma^{\prime}\Rightarrow\Delta$
---

Figure 6. Rules in hypersequent calculi.

###  2.3. 2-Sequents and Linear Nested Sequents

The 2-sequent formalism was introduced by Masini [Mas92, Mas93] as a
generalization of Gentzen’s sequent formalism whereby an _infinite list_ of
multisets of formulae implies another infinite list. For instance, an example
of a 2-sequent is shown below left and an another example is shown below
right:

$\textstyle{A,B}$$\textstyle{D}$$\textstyle{C}$$\textstyle{\Rightarrow}$$\textstyle{E,F}$$\textstyle{G}$ |  $\textstyle{\leadsto}$ | $\textstyle{A,B}$$\textstyle{D}$$\textstyle{C}$$\textstyle{\Rightarrow}$$\textstyle{E,F,\Box G}$
---|---|---

In the 2-sequent above left, the antecedent consists of the list whose first
element is the multiset $A,B$, second element is the singleton $C$, and where
every other element is the empty multiset. By contrast, the consequent
consists of a list beginning with the three multisets (1) $D$, (2) $E,F$, and
(3) $G$, and where every other element is the empty multiset. The 2-sequent
shown above right is derivable from the 2-sequent shown above left by
‘shifting’ the $G$ formula up one level and introducing a $\Box$ modality,
thus demonstrating how modal formulae may be derived in the formalism. Systems
built with such sequents have been provided for various logics—e.g. modal
logics [Mas92], intuitionistic logic [Mas93], and tense logics [BM04]—and tend
to exhibit desirable proof-theoretic properties such as generalized forms of
cut-elimination and the subformula property.

More recently, a refined but equivalent re-formulation of 2-sequents was
provided by Lellmann [Lel15]. Rather than employing sequents with infinite
lists for antecedents and consequents, the formalism employs _linear nested
sequents_ , which are finite lists of Gentzen-style sequents. For example, the
2-sequents shown above left and right may be re-written as the linear nested
sequents shown below left and right respectively with the ‘$\sslash$’
constructor separating the components (i.e. each Gentzen-style sequent) in
each list:

$A,B\Rightarrow D\sslash C\Rightarrow E,F\sslash\emptyset\Rightarrow G\qquad
A,B\Rightarrow D\sslash C\Rightarrow E,F,\Box G$

Linear nested sequent systems have been provided for a diverse selection of
logics; e.g., modal logics [Lel15], propositional and first-order Gödel-
Dummett logic [KL18, Lyo20b], and the tense logic $\mathsf{Kt}$ [GL19].
Moreover, such calculi have been used to write constructive interpolation
proofs [KL18] and decision procedures [GL19].

As discussed by Lellmann [Lel15], there is a close connection between Gentzen-
style sequent calculi, nested sequent calculi (discussed in Section 2.5
below), and linear nested sequent calculi. In particular, certain linear
nested sequent systems have been found to encode _branches_ within sequent
calculus proofs as well as branches within nested sequents. For example, the
standard $(\Box)$ rule that occurs in the sequent calculus for the modal logic
$\mathsf{K}$ (shown below left) corresponds to $|\Gamma|$ many applications of
the $(\Box_{l})$ rule followed by an application of the $(\Box_{r})$ rule in
the linear nested sequent calculus for $\mathsf{K}$ (cf. [Lel15]).

$\Gamma\Rightarrow A$ $(\Box)$ $\Box\Gamma\Rightarrow\Box A$ | $\leadsto$ |  $\Box\Gamma\Rightarrow\Box A\sslash\Gamma\Rightarrow A$ $(\Box_{l})\times|\Gamma|$ $\Box\Gamma\Rightarrow\Box A\sslash\emptyset\Rightarrow A$ $(\Box_{r})$ $\Box\Gamma\Rightarrow\Box A$
---|---|---

Observe that the top linear nested sequent in the inferences shown above right
stores the conclusion and premise of the $(\Box)$ rule, thus demonstrating how
linear nested sequents can encode branches (i.e. sequences of inferences) in
sequent calculus proofs.

Due to the fact that linear nested sequents employ a relatively simple data
structure, the formalism typically allows for complexity-optimal proof-search
algorithms, similar to (depth-first) algorithms written within sequent and
nested sequent systems. As such, the linear nested sequent formalism strikes a
balance between complexity-optimality on the one hand, and expressivity on the
other, since the formalism allows for many logics to be captured in a cut-free
manner while exhibiting desirable invertibility and admissibility properties.
Note that if we let the ‘$\sslash$’ constructor be commutative, then it can be
seen as the hypersequent ‘$\;\mid\;$’ constructor, showing that every
hypersequent calculus is technically a linear nested sequent calculus, i.e.
and the latter formalism generalizes the former [Lel15]. It can be seen that
the linear nested sequent formalism satisfies the same desiderata as the
hypersequent formalism, though improves upon generality as the formalism is
known to capture logics lacking a cut-free hypersequent calculus, e.g. the
tense logic $\mathsf{Kt}$ [GL19].

###  2.4. Bunched Sequents

As recalled in Section 2.1, a standard Gentzen sequent is an object of the
form ${\Gamma\Rightarrow\Delta}$ where the contexts $\Gamma$ and $\Delta$
usually are sets or multisets, sometimes (but less often333This is the case
for logics lacking all structural rules.) lists. Those data structures are one
dimensional and built from a single context forming operator usually written
as a comma or a semi-colon. An interesting extension of Gentzen sequents are
_bunched sequents_ , which arise when the contexts are built from more than
one context forming operators. For example, in [CGS11] two context forming
operators, “;” and ‘,‘ are used to split the contexts into several zones the
formulas of which are handled differently by a focused sequent calculus.
Nevertheless, inside a zone, the formulas are arranged as a one dimensional
structure (usually a multiset) and the inference rules can be applied to any
formula in that shallow structure (thus making the inference rules shallow).
Let us remark that bunched structures can also be used to extend the
hypersequent framework to bunched hypersequents (forests of sequents) as
illustrated in a recent work [CR17]. However, in the remaining of the section,
we shall focus on the most representative witness of a bunched sequent
calculus, which is undoubtedly the one given for Bunched Implications logic
($\mathsf{BI}$) in [Pym02].

In $\mathsf{BI}$, formulas are arranged as “bunches” which can be viewed as
trees whose leaves are labeled with formulas and whose internal nodes are
labeled with either “$\mathop{;}$” or “$\mathop{,}$”. More formally, bunches
are trees given by the following grammar:

$\Gamma::=A\mid\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{a}}}\mid\Gamma\mathop{;}\Gamma\mid\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{m}}}\mid\Gamma\mathop{,}\Gamma$

The notation $\Gamma(\Delta)$ denotes a bunch $\Gamma$ that contains the bunch
$\Delta$ as a subtree.

Bunches are considered up to a structural equivalence $\mathbin{\equiv}$ given
by commutative monoid equations for “$\mathop{;}$” and “$\mathop{,}$” with
units $\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{a}}}$ and
$\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{m}}}$ respectively, together
with the substitution congruence for subbunches. From a logical point of view,
bunches relate to formulas as follows: let $\Gamma$ be a bunch, the
corresponding formula is $\mathrm{\Phi}_{\Gamma}$ which is obtained from
$\Gamma$ by replacing each
$\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{m}}}$ with
$\top{\scriptscriptstyle\mathfrak{m}}$, each
$\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{a}}}$ with
$\top{\scriptscriptstyle\mathfrak{a}}$, each “$\mathop{,}$” with
$\mathbin{\makebox[6.45831pt]{$\ast$}}$ and each “$\mathop{;}$” with
$\mathbin{\makebox[6.45831pt]{$\wedge$}}$.

The standard internal calculus for $\mathsf{BI}$ is a single conclusion
bunched sequent calculus called $\mathsf{LBI}$. In $\mathsf{LBI}$, bunches
arise (on the left-hand side only) from the two kinds of implications
$\mathbin{\makebox[9.68747pt]{$\supset$}}$ and
$\mathbin{\makebox[9.68747pt]{$-\ast$}}$, that respectively give rise to two
distinct context forming operators “$\mathop{;}$” and “$\mathop{,}$” as
follows:

($\mathrm{\mathbin{\makebox[7.74998pt]{$\supset$}}_{\mathit{r}}}$)
${\Gamma\mathop{;}A\Rightarrow B}$${\Gamma\Rightarrow
A\mathbin{\makebox[9.68747pt]{$\supset$}}B}$
($\mathrm{\mathbin{\makebox[7.74998pt]{$-\ast$}}_{\mathit{r}}}$)
${\Gamma\mathop{,}A\Rightarrow B}$${\Gamma\Rightarrow
A\mathbin{\makebox[9.68747pt]{$-\ast$}}B}$

From a syntactic point of view, the main distinction between “$\mathop{;}$”
(associated with $\mathbin{\makebox[6.45831pt]{$\wedge$}}$) and “$\mathop{,}$”
(associated with $\mathbin{\makebox[6.45831pt]{$\ast$}}$) is that
“$\mathop{;}$” admits both weakening and contraction while “$\mathop{,}$” does
not.

($\mathrm{id}$) ${A\Rightarrow A}$

($\mathrm{\makebox[8.6111pt]{$\top{\scriptscriptstyle\mathfrak{m}}$}_{\mathit{r}}}$)
${\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{m}}}\Rightarrow\makebox[10.76385pt]{$\top{\scriptscriptstyle\mathfrak{m}}$}}$

($\mathrm{\makebox[8.6111pt]{$\top{\scriptscriptstyle\mathfrak{a}}$}_{\mathit{r}}}$)
${\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{a}}}\Rightarrow\makebox[10.76385pt]{$\top{\scriptscriptstyle\mathfrak{a}}$}}$

($\mathrm{\bot_{\mathit{l}}}$) ${\Gamma(\bot)\Rightarrow A}$

($\mathrm{\makebox[8.6111pt]{$\top{\scriptscriptstyle\mathfrak{m}}$}_{\mathit{l}}}$)
${\Gamma(\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{m}}})\Rightarrow
A}$${\Gamma(\makebox[10.76385pt]{$\top{\scriptscriptstyle\mathfrak{m}}$})\Rightarrow
A}$

($\mathrm{\makebox[8.6111pt]{$\top{\scriptscriptstyle\mathfrak{a}}$}_{\mathit{l}}}$)
${\Gamma(\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{a}}})\Rightarrow
A}$${\Gamma(\makebox[10.76385pt]{$\top{\scriptscriptstyle\mathfrak{a}}$})\Rightarrow
A}$

($\mathrm{\mathbin{\makebox[5.16666pt]{$\vee$}}_{\mathit{l}}}$)
${\Gamma(B)\Rightarrow A}$${\Gamma(C)\Rightarrow
A}$${\Gamma(B\mathbin{\makebox[6.45831pt]{$\vee$}}C)\Rightarrow A}$

($\mathrm{\mathbin{\makebox[5.16666pt]{$\vee$}}^{\mathrm{i}}_{\mathit{r}}}$)
${\Gamma\Rightarrow A_{\mathrm{i}\,\in\,\\{\,1,2\/\,\\}}}$${\Gamma\Rightarrow
A_{1}\mathbin{\makebox[6.45831pt]{$\vee$}}A_{2}}$

($\mathrm{\mathbin{\makebox[7.74998pt]{$-\ast$}}_{\mathit{l}}}$)
${\Delta\Rightarrow B}$${\Gamma(C)\Rightarrow
A}$${\Gamma(B\mathbin{\makebox[9.68747pt]{$-\ast$}}C\mathop{,}\Delta)\Rightarrow
A}$

($\mathrm{\mathbin{\makebox[7.74998pt]{$-\ast$}}_{\mathit{r}}}$)
${\Gamma\mathop{,}A\Rightarrow B}$${\Gamma\Rightarrow
A\mathbin{\makebox[9.68747pt]{$-\ast$}}B}$

($\mathrm{\mathbin{\makebox[5.16666pt]{$\ast$}}_{\mathit{l}}}$)
${\Gamma(B\mathop{,}C)\Rightarrow
A}$${\Gamma(B\mathbin{\makebox[6.45831pt]{$\ast$}}C)\Rightarrow A}$

($\mathrm{\mathbin{\makebox[5.16666pt]{$\ast$}}_{\mathit{r}}}$)
${\Gamma\Rightarrow A}$${\Delta\Rightarrow
B}$${\Gamma\mathop{,}\Delta\Rightarrow
A\mathbin{\makebox[6.45831pt]{$\ast$}}B}$

($\mathrm{\mathbin{\makebox[7.74998pt]{$\supset$}}_{\mathit{l}}}$)
${\Delta\Rightarrow B}$${\Gamma(C)\Rightarrow
A}$${\Gamma(B\mathbin{\makebox[9.68747pt]{$\supset$}}C\mathop{;}\Delta)\Rightarrow
A}$

($\mathrm{\mathbin{\makebox[7.74998pt]{$\supset$}}_{\mathit{r}}}$)
${\Gamma\mathop{;}A\Rightarrow B}$${\Gamma\Rightarrow
A\mathbin{\makebox[9.68747pt]{$\supset$}}B}$

($\mathrm{\mathbin{\makebox[5.16666pt]{$\wedge$}}_{\mathit{l}}}$)
${\Gamma(B\mathop{;}C)\Rightarrow
A}$${\Gamma(B\mathbin{\makebox[6.45831pt]{$\wedge$}}C)\Rightarrow A}$

($\mathrm{\mathbin{\makebox[5.16666pt]{$\wedge$}}_{\mathit{r}}}$)
${\Gamma\Rightarrow A}$${\Delta\Rightarrow
B}$${\Gamma\mathop{;}\Delta\Rightarrow
A\mathbin{\makebox[6.45831pt]{$\wedge$}}B}$

($\mathrm{WK}$) ${\Gamma(\Delta_{1})\Rightarrow
A}$${\Gamma(\Delta_{1}\mathop{;}\Delta_{2})\Rightarrow A}$

($\mathrm{CR}$) ${\Gamma(\Delta\mathop{;}\Delta)\Rightarrow
A}$${\Gamma(\Delta)\Rightarrow A}$

($\mathrm{\Gamma\mathbin{\equiv}\Delta}$) ${\Gamma\Rightarrow
A}$${\Delta\Rightarrow A}$

($\mathrm{CUT}$) ${\Delta\Rightarrow B}$${\Gamma(B)\Rightarrow
A}$${\Gamma(\Delta)\Rightarrow A}$

Figure 7. The Sequent Calculus $\mathsf{LBI}$.

The $\mathsf{LBI}$ sequent calculus, depicted in Fig. 7, derives sequents of
the form ${\Gamma\Rightarrow C}$, where $\Gamma$ is a bunch and $C$ is a
formula. A formula $C$ is a _theorem_ of $\mathsf{LBI}$ iff
${\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{m}}}\Rightarrow C}$ is
provable in $\mathsf{LBI}$. Let us remark that the inference rules of
$\mathsf{LBI}$ are deep in that they can be applied to formulas anywhere in
the tree structure of a bunch and not only at the root. Let us also mention
that the $\mathrm{CUT}$ rule is admissible in $\mathsf{LBI}$ [Pym02] and that
the contraction rule $\mathrm{CR}$ may duplicate whole bunches and not just
formulas. Indeed, as shown in Example 2.4, restricting contraction to single
formulas would not allow to prove the end sequent.

$\mathsf{LBI}$-proof of
$((p\mathbin{\makebox[9.68747pt]{$-\ast$}}(q\mathbin{\makebox[9.68747pt]{$\supset$}}r)\mathbin{\makebox[6.45831pt]{$\wedge$}}p\mathbin{\makebox[9.68747pt]{$-\ast$}}q)\mathbin{\makebox[6.45831pt]{$\ast$}}p)\mathbin{\makebox[9.68747pt]{$-\ast$}}r$.

($\mathrm{\mathbin{\makebox[7.74998pt]{$-\ast$}}_{\mathit{r}}}$)
($\mathrm{\mathbin{\makebox[5.16666pt]{$\ast$}}_{\mathit{l}}}$)
($\mathrm{\mathbin{\equiv}}$)
($\mathrm{\mathbin{\makebox[5.16666pt]{$\wedge$}}_{\mathit{r}}}$)
($\mathrm{CR}$) ($\mathrm{WK}$) ($\mathrm{WK}$)
($\mathrm{\mathbin{\makebox[7.74998pt]{$-\ast$}}_{\mathit{l}}}$)
($\mathrm{\mathbin{\makebox[7.74998pt]{$-\ast$}}_{\mathit{l}}}$)
($\mathrm{\mathbin{\makebox[7.74998pt]{$\supset$}}_{\mathit{l}}}$)
($\mathrm{id}$) ($\mathrm{id}$) ($\mathrm{id}$) ($\mathrm{id}$) ${p\Rightarrow
p}$ ${p\Rightarrow p}$ ${q\Rightarrow q}$ ${r\mathop{;}q\Rightarrow r}$
${q\mathbin{\makebox[9.68747pt]{$\supset$}}r\mathop{;}q\Rightarrow r}$
${q\mathbin{\makebox[9.68747pt]{$\supset$}}r\mathop{;}(p\mathbin{\makebox[9.68747pt]{$-\ast$}}q\mathop{,}p)\Rightarrow
r}$
${(p\mathbin{\makebox[9.68747pt]{$-\ast$}}(q\mathbin{\makebox[9.68747pt]{$\supset$}}r)\mathop{,}p)\mathop{;}(p\mathbin{\makebox[9.68747pt]{$-\ast$}}q\mathop{,}p)\Rightarrow
r}$
${(p\mathbin{\makebox[9.68747pt]{$-\ast$}}(q\mathbin{\makebox[9.68747pt]{$\supset$}}r)\mathop{,}p)\mathop{;}((p\mathbin{\makebox[9.68747pt]{$-\ast$}}(q\mathbin{\makebox[9.68747pt]{$\supset$}}r)\mathop{;}p\mathbin{\makebox[9.68747pt]{$-\ast$}}q)\mathop{,}p)\Rightarrow
r}$
${((p\mathbin{\makebox[9.68747pt]{$-\ast$}}(q\mathbin{\makebox[9.68747pt]{$\supset$}}r)\mathop{;}p\mathbin{\makebox[9.68747pt]{$-\ast$}}q)\mathop{,}p)\mathop{;}((p\mathbin{\makebox[9.68747pt]{$-\ast$}}(q\mathbin{\makebox[9.68747pt]{$\supset$}}r)\mathop{;}p\mathbin{\makebox[9.68747pt]{$-\ast$}}q)\mathop{,}p)\Rightarrow
r}$
${(p\mathbin{\makebox[9.68747pt]{$-\ast$}}(q\mathbin{\makebox[9.68747pt]{$\supset$}}r)\mathop{;}p\mathbin{\makebox[9.68747pt]{$-\ast$}}q)\mathop{,}p\Rightarrow
r}$
${((p\mathbin{\makebox[9.68747pt]{$-\ast$}}(q\mathbin{\makebox[9.68747pt]{$\supset$}}r)\mathbin{\makebox[6.45831pt]{$\wedge$}}p\mathbin{\makebox[9.68747pt]{$-\ast$}}q)\mathop{,}p)\Rightarrow
r}$
${\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{m}}}\mathop{,}((p\mathbin{\makebox[9.68747pt]{$-\ast$}}(q\mathbin{\makebox[9.68747pt]{$\supset$}}r)\mathbin{\makebox[6.45831pt]{$\wedge$}}p\mathbin{\makebox[9.68747pt]{$-\ast$}}q)\mathop{,}p)\Rightarrow
r}$
${\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{m}}}\mathop{,}((p\mathbin{\makebox[9.68747pt]{$-\ast$}}(q\mathbin{\makebox[9.68747pt]{$\supset$}}r)\mathbin{\makebox[6.45831pt]{$\wedge$}}p\mathbin{\makebox[9.68747pt]{$-\ast$}}q)\mathbin{\makebox[6.45831pt]{$\ast$}}p)\Rightarrow
r}$
${\mathrm{\varnothing_{\scriptscriptstyle\mathfrak{m}}}\Rightarrow((p\mathbin{\makebox[9.68747pt]{$-\ast$}}(q\mathbin{\makebox[9.68747pt]{$\supset$}}r)\mathbin{\makebox[6.45831pt]{$\wedge$}}p\mathbin{\makebox[9.68747pt]{$-\ast$}}q)\mathbin{\makebox[6.45831pt]{$\ast$}}p)\mathbin{\makebox[9.68747pt]{$-\ast$}}r}$

###  2.5. Nested Sequents

Nested sequent calculi were originally defined by Kashima for tense logics
[Kas94] and Bull for the fragment of PDL without the Kleene star [Bul92].444We
note that nested sequent calculi can be seen as ‘upside-down’ versions of
prefixed tableaux [Fit72]. See Fitting [Fit14] for a discussion. The
characteristic feature of such calculi is the use of _trees_ of Gentzen-style
sequents in proofs. This additional structure has led to the development of
cut-free calculi for various logics not known to possess a cut-free Gentzen-
style sequent calculus, and is general in the sense that sizable classes of
logics can be uniformly captured with such systems. For example, cut-free
nested sequent calculi have been given for classical modal logics [Brü09,
Pog09], for intuitionistic modal logics [Str13, Lyo21a], for classical tense
logics [Kas94, GPT11], and for first-order intermediate logics [Fit14, Lyo23].
Moreover, the rules of nested sequent calculi are usually invertible, which—as
mentioned above—are useful in extracting counter-models from failed proof
search (cf. [TIG12, LGA22]).

Nested sequents have also been referred to as _tree-hypersequents_ [Pog09,
Pog11], and are also essentially the same as _tree-sequents_ , introduced in
[GS10], for providing label-free calculi for classical and intuitionistic
modal logics [GS10, GS18]. The notion of tree-sequent can be seen as a kind of
mono-conclusion version of a nested sequent, with the key difference that the
formula associated with a tree-sequent makes use of both modal operators
instead of just one. However, we will stick to the term _nested sequent_ as it
is far more prevalent in the literature and is the original term given by
Kashima [Kas94] and Bull [Bul92].

$(id)$ $\Sigma\\{\Gamma,p,\neg p\\}$ |  $\Sigma\\{\Gamma,A\\}$ $\Sigma\\{\Gamma,B\\}$ $(\land)$ $\Sigma\\{\Gamma,A\land B\\}$
---|---

$\Sigma\\{\Gamma,{\circ}[A]\\}$ $(\Box)$ $\Sigma\\{\Gamma,\Box A\\}$ |  $\Sigma\\{\Gamma,A,{\bullet}[\Delta,\Diamond A]\\}$ $(\Diamond_{2})$ $\Sigma\\{\Gamma,{\bullet}[\Delta,\Diamond A]\\}$
---|---

$\Sigma\\{\blacklozenge A,{\bullet}[\Gamma,A]\\}$ $(\blacklozenge_{1})$ $\Sigma\\{\blacklozenge A,{\bullet}[\Gamma]\\}$ |  $\Sigma\\{\Gamma,A,{\circ}[\Delta,\blacklozenge A]\\}$ $(\blacklozenge_{2})$ $\Sigma\\{\Gamma,{\circ}[\Delta,\blacklozenge A]\\}$
---|---

Figure 8. The nested sequent system $\mathsf{N(Kt)}$ for the modal logic
$\mathsf{Kt}$ [Kas94].

Nested sequents generalize the syntax of Gentzen-style sequents via the
incorporation of a nesting constructor. For instance, for the tense logic
$\mathsf{Kt}$, nested sequents are generated via the following grammar in BNF:

$\Sigma::=A\ |\ \emptyset\ |\ \Sigma,\Sigma\ |\ {\circ}[\Sigma]\ |\
{\bullet}[\Sigma]$

where $A\in\mathcal{L}_{M}$ and $\emptyset$ is the empty nested sequent.
Examples of nested sequents generated in the above syntax include (1)
$\Sigma_{1}=p,\Diamond q$, (2) $\Sigma_{2}=\blacksquare
p,{\circ}[p,{\bullet}[q]]$, and (3) $\Sigma_{3}=p\land
r,{\circ}[\emptyset,{\circ}[\Diamond q,p],{\bullet}[\neg q\lor
q]],{\circ}[\neg q]$, which are graphically displayed below as trees with
labeled edges in order from left to right.

$\boxed{p\land r}$$\boxed{\emptyset}$$\boxed{\neg q}$$\boxed{\Diamond
q,p}$$\boxed{\neg q\lor q}$$\circ$$\circ$$\circ$$\bullet$$\boxed{\blacksquare
p}$$\boxed{p}$$\boxed{q}$$\circ$$\bullet$$\boxed{p,\Diamond q}$

Nested sequent calculi typically exhibit a mode of inference referred to as
_deep-inference_ , whereby inference rules may be applied to any node within
the tree encoded by the sequent [Gug07]. This contrasts with _shallow-
inference_ , where inference rules are only applicable to the root of the tree
encoded by the sequent. We remark that shallow-inference is an essential
feature of _display calculi_ , which will be discussed in Section 2.6 below.
Although nested calculi are typically formulated with deep-inference, shallow-
inference versions have been introduced [GPT08, Kas94].555We note that in
shallow-inference nested calculi certain rules called _display_ or
_residuation_ rules are required for completeness. This will be discussed in
the next section. Nevertheless, as has become standard in the literature, we
understand the term _nested sequent calculus_ to mean _deep-inference nested
sequent calculus_ as the shallow-inference variants are known to be subsumed
by the display calculus formalism [CLRT21] and will be considered as such.

An example of a nested sequent calculus for the tense logic $\mathsf{Kt}$,
referred to as $\mathsf{N(Kt)}$, is provided in Figure 10 and is due to
Kashima [Kas94]. The notation $\Sigma\\{\Gamma\\}$ is commonly employed in the
formulation of nested inference rules and exhibits deep-inference. We read
$\Sigma\\{\Gamma\\}$ as stating that the nested sequent $\Gamma$ occurs at
some node in the tree encoded by the nested sequent $\Sigma$. For example, we
can write the nested sequent $\Sigma_{2}$ above as
$\Sigma_{2}\\{p,{\bullet}[q]\\}$, or the nested sequent $\Sigma_{3}$ above as
$\Sigma_{3}\\{\neg q\\}$ in this notation, thus letting us refer to the
displayed nodes and the data confined within. Similarly, we may refer to
multiple nodes in a nested sequent $\Sigma$ simultaneously by means of the
notation $\Sigma\\{\Gamma_{1}\\}\\{\Gamma_{2}\\}\cdots\\{\Gamma_{n}\\}$. For
instance, we could write $\Sigma_{2}$ as $\Sigma_{2}\\{p\\}\\{q\\}$ or
$\Sigma_{3}$ as $\Sigma_{3}\\{p\land r\\}\\{{\circ}[\Diamond q,p]\\}$.

The $(id)$ rule in $\mathsf{N(Kt)}$ states that any nested sequent containing
both $p$ and $\neg p$ at a node is an axiom. The remaining rules tell us how
complex logical formulae may be constructed within any given node of a
derivable nested sequent. For example, $(\lor)$ states that $A,B$ can be
replaced by $A\lor B$, and $(\Box)$ states that ${\circ}[A]$ can be replaced
by $\Box A$. As an example of how derivations are constructed in nested
sequent calculi, we show how the modal axiom $\mathsf{K}$ (in negation normal
form) can be derived in $\mathsf{N(Kt)}$ below.

$(id)$ $\Diamond(p\land\neg q),\Diamond\neg p,{\circ}[p,\neg p,q]$ $(id)$
$\Diamond(p\land\neg q),\Diamond\neg p,{\circ}[\neg q,\neg p,q]$ $(\land)$
$\Diamond(p\land\neg q),\Diamond\neg p,{\circ}[p\land\neg q,\neg p,q]$
$(\Diamond)\times 2$ $\Diamond(p\land\neg q),\Diamond\neg p,{\circ}[q]$
$(\Box)$ $\Diamond(p\land\neg q),\Diamond\neg p,\Box q$ $(\lor)\times 2$
$\Diamond(p\land\neg q)\lor\Diamond\neg p\lor\Box q$

$(id)^{{\dagger}}$ $\Sigma\\{\Gamma_{1},p\Rightarrow\Delta_{1}\\}_{w}\\{\Gamma_{2}\Rightarrow p,\Delta_{2}\\}_{u}$ |  $(\bot_{l})$ $\Sigma\\{\Gamma,\bot\Rightarrow\Delta\\}_{w}$
---|---

$\Sigma\\{\Gamma,A\Rightarrow\Delta\\}_{w}$ $\Sigma\\{\Gamma,B\Rightarrow\Delta\\}_{w}$ $(\lor_{l})$ $\Sigma\\{\Gamma,A\lor B\Rightarrow\Delta\\}_{w}$ |  $\Sigma\\{\Gamma\Rightarrow A,B,\Delta\\}_{w}$ $(\lor_{r})$ $\Sigma\\{\Gamma\Rightarrow A\lor B,\Delta\\}_{w}$
---|---

$\Sigma\\{\Gamma,A,B\Rightarrow\Delta\\}_{w}$ $(\land_{l})$ $\Sigma\\{\Gamma,A\land B\Rightarrow\Delta\\}_{w}$ |  $\Sigma\\{\Gamma\Rightarrow A,\Delta\\}_{w}$ $\Sigma\\{\Gamma\Rightarrow B,\Delta\\}_{w}$ $(\land_{r})$ $\Sigma\\{\Gamma\Rightarrow A\land B,\Delta\\}_{w}$
---|---

$\Sigma\\{\Gamma_{1},A\supset
B\Rightarrow\Delta_{1}\\}_{w}\\{\Gamma_{2},B\Rightarrow\Delta_{2}\\}_{u}$
$\Sigma\\{\Gamma_{1},A\supset
B\Rightarrow\Delta_{1}\\}_{w}\\{\Gamma_{2}\Rightarrow A,\Delta_{2}\\}_{u}$
$(\supset_{l})^{{\dagger}}$ $\Sigma\\{\Gamma_{1},A\supset
B\Rightarrow\Delta_{1}\\}_{w}\\{\Gamma_{2}\Rightarrow\Delta_{2}\\}_{u}$
---

$\Sigma\\{\Gamma\Rightarrow\Delta,[A\Rightarrow B]_{u}\\}_{w}$ $(\supset_{r})$
$\Sigma\\{\Gamma\Rightarrow\Delta,A\supset B\\}_{w}$
---

Side condition: ${\dagger}$ = $u$ must be reachable from $w$ in
$(\supset_{l})$.

Figure 9. The nested sequent system $\mathsf{N(IL)}$ for intuitionistic logic.

Although nested sequent calculi for logics can be constructed in a ‘bottom-up’
manner by conjecturing inference rules and then reformulating them as needed
to ensure soundness and completeness, there exist ‘top-down’ methods of
construction, which have proven to be rather general. One method is due to
Goré et al. [GPT08, GPT11] and consists of extracting nested sequent calculi
from display calculi, whereas the other method, referred to as _structural
refinement_ , is due to Lyon [Lyo21b, Lyo21a] and consists of extracting
nested sequent calculi from labeled sequent calculi.666Labeled sequent calculi
are discussed in Section 2.7 below. Since methods of construction for display
and labeled calculi are well-understood and general, these top-down approaches
have led to the formulation of broad classes of cut-free nested sequent
calculi for a variety of logics, including bi-intuitionistic logic [GPT08],
grammar logics [TIG12], (deontic) agency logics [LvB19, Lyo21b], and
standpoint logic [LGA22] (used in knowledge integration).

Both methods rely on the elimination of structural rules in a display or
labeled calculus, replacing them with _propagation rules_ [CdCGH97, Fit72,
Sim94], or the more general class of _reachability rules_ [Lyo21b, Lyo23].
Propagation rules operate by (bottom-up) propagating data along paths within a
sequent, whereas reachability rules have the added functionality that data can
be searched for within a sequent, and potentially propagated elsewhere (see
[Lyo21b, Chapter 5] for a discussion of these types of rules). Since
propagation and reachability rules play a crucial role in the formulation of
nested sequent calculi, we will demonstrate their functionality by means of an
example. More specifically, we will introduce the nested sequent calculus
$\mathsf{N(IL)}$, shown in Figure 9, which employs the $(\supset_{l})$
propagation rule and $(id)$ reachability rule.777The calculus $\mathsf{N(IL)}$
is the propositional fragment of the nested calculi given for first-order
intuitionistic logics in [Lyo21b], and is a variation of the nested calculus
given by Fitting [Fit14]. Furthermore, we introduce this calculus for a second
reason, namely, it will serve as an interesting example in our translation
work in Section 3.

Nested sequents in $\mathsf{N(IL)}$ are generated via the following grammars
in BNF:

$\Sigma::=\Gamma\Rightarrow\Gamma\ |\ \Sigma,[\Sigma]_{w}\qquad\Gamma::=A\ |\
\emptyset\ |\ \Gamma,\Gamma$

where $A\in\mathcal{L}_{I}$, $w$ is among a countable set of labels $w$, $u$,
$v$ $\ldots$, and $\emptyset$ is the empty multiset. The notation used in the
rules of $\mathsf{N(IL)}$ marks nestings with labels, e.g. in $(id)$ and
$(\supset_{l})$ the labels $w$ and $u$ are used. It is assumed that each label
is used once in a nested sequent and we note that such labels are merely a
naming device used to simplify the formulation of certain inference rules. We
note that the root of a nested sequent $\Sigma$ is always assigned a unique
label $r$. As stated in Figure 9, the $(id)$ and $(\supset_{l})$ rules have a
side condition stating that each respective rule is applicable only if the
node $u$ is reachable from the node $w$. This means that in the tree encoded
by the nested sequent $\Sigma$, the rule is applicable only if there is a path
(which could be of length $0$) from $w$ to $u$. For example, in the
$\mathsf{N(IL)}$ proof below the $(\supset_{l})$ rule recognizes the $p\supset
q$ in the $w$ nesting and propagates $q$ into $[p\Rightarrow q]_{u}$ in the
left premise and $p$ into $[p\Rightarrow q]_{u}$ in the right premise when
read bottom-up. Each premise of $(\supset_{l})$ can be read as an instance of
$(id)$ since $u$ is reachable from $u$ with a path of length $0$.

$(id)$ $\Rightarrow[p\supset q\Rightarrow[p,q\Rightarrow q]_{u}]_{w}$ $(id)$
$\Rightarrow[p\supset q\Rightarrow[p\Rightarrow p,q]_{u}]_{w}$ $(\supset_{l})$
$\Rightarrow[p\supset q\Rightarrow[p\Rightarrow q]_{u}]_{w}$ $(\supset_{r})$
$\Rightarrow[p\supset q\Rightarrow p\supset q]_{w}$ $(\supset_{r})$
$\Rightarrow(p\supset q)\supset(p\supset q)$

In Section 3, we will show how $\mathsf{N(IL)}$ can be extracted from a
labeled sequent calculus, thus exemplifying the structural refinement method
of [Lyo21b, Lyo21a].

We end this subsection with a brief discussion concerning the relationship
between propagation/reachability rules and the property of _modularity_ , that
is, the ease with which a calculus for one logic may be transformed into a
calculus for another logic within a given class. An interesting feature of
propagation and reachability rules concerns the means by which they introduce
modularity into a proof calculus. It has been argued—most notably by Avron
[Avr96, Section 1] and Wansing [Wan94, Section 3.3]—that modularity ought to
be obtained via _Došen’s Principle_ , which is stated accordingly:

> [T]he rules for the logical operations are never changed: all changes are
> made in the structural rules [Doš88, p. 352]

Although we agree that modularity is an important feature of a proof
formalism, we argue that Došen’s principle is _too strict_. This perspective
is supported by the formulation of propagation/reachability rules within
nested systems, which attain modularity by a different means. Since these
types of rules generalize the functionality of logical rules by permitting
data to be shifted or consumed along paths within a nested sequent, systems
which include such rules possess a high degree of modularity, obtained by
simply changing the paths considered, irrespective of structural rules.

###  2.6. Display Sequents

Introduced by Belnap [Bel82] (and originally called _Display Logic_), the
Display Calculus formalism generalizes Gentzen’s sequent calculus by
supplementing the structural connective (,) and the turnstile ($\Rightarrow$)
with a host of new structural connectives—corresponding to pairs of dual
connectives—and rules manipulating them. Incorporating structural connectives
for pairs of dual connectives has proven fruitful for the construction of cut-
free proof systems for large classes of logics, including modal and
intuitionistic logics [Bel82], tense logics [Kra96, Wan94], bunched
implication logics [Bro12], resource sensitive logics [Gor98], and bi-
intuitionistic logic [Wol98]. Display calculi also admit algorithmic
construcibility starting from Hilbert axioms [CR16, GMP+18]. To provide the
reader with intuition concerning display systems and related concepts we
accompany our general descriptions of such systems with concrete examples in
the context of tense logics [Pri57] and which comes from the work in [Kas94,
Kra96, Wan94].

First, to demonstrate the concept of a structural connective, let us define
_structures_ , which serve as the entire antecedent or consequent of a display
sequent and fuse together formulae by means of structural connectives. When
defining display sequents for tense logics, we let a structure $X$ be a
formula obtained via the following grammar in BNF:

$X::=A\ |\ I\ |\ {\ast}X\ |\ {\bullet}X\ |\ (X\circ X)$

where $A$ is a formula in the language of tense logic, i.e. within the
language $\mathcal{L}_{T}$. Using $X$, $Y$, $Z$, $\ldots$ to represent
structures, we define a _display sequent_ to be a formula of the form
$X\Rightarrow Y$. We provide the reader with an example of a display sequent
as well as show the pair of graphs representing the structures present in the
antecedent and consequent of the display sequent.

[Display Sequent and Corresponding Graphs] As can be seen in the example below
the antecedent (shown bottom left) and consequent (shown bottom right) of a
(tense) display sequent encodes a polytree; cf. [CLR18].

$\underbrace{\bullet(A_{1}\circ\ast A_{2})\circ\bullet A_{3}\circ
A_{4}}_{Antecedent}\Rightarrow\underbrace{A_{5}\circ\bullet(\ast
A_{6}\circ\ast A_{7})\circ\bullet A_{8}}_{Consequent}$

$\boxed{A_{4}}$$\boxed{A_{1}\circ\ast
A_{2}}$$\boxed{A_{3}}$$\boxed{A_{5}}$$\boxed{\ast A_{6}\circ\ast
A_{7}}$$\boxed{A_{8}}$

A characteristic feature of the display calculus is the display property,
which states that every occurrence of a substructure in a sequent can be
written (displayed) as the entire antecedent or succedent (but not both).
Rules enabling the display property are called display rules or residuation
rules, and display sequents derivable from one another via such rules are
called display equivalent. These rules are invertible and hence a sequent can
be identified with the class of its display equivalent sequents. For example,
the bullet $\bullet$ represents a $\blacklozenge$ in the antecedent of a
display sequent and a $\Box$ in the consequent, and since $\blacklozenge
A\rightarrow B$ and $A\rightarrow\Box B$ are equivalent in the setting of
tense logics, the display sequents $\bullet A\Rightarrow B$ and
$A\Rightarrow\bullet B$ are defined to be mutually derivable from one another.
This gives rise to the following _display rule_ introduced by Wansing [Wan94].

$\bullet X\Rightarrow Y$ $(\bullet)$ $X\Rightarrow\bullet Y$

As mentioned in the previous section, nested sequent calculi employing
shallow-inference are also types of display calculi. As an example, if we take
the nested calculus $\mathsf{N(Kt)}$ and add the display/residuation rules
$(r\\!f)$ and $(rp)$ rules shown below left as well as replace the
$(\Diamond_{1})$, $(\Diamond_{2})$, $(\blacklozenge_{1})$, and
$(\blacklozenge_{2})$ rules with the $(\Diamond)$ and $(\blacklozenge)$ rules
shown below right, then we obtain Kashima’s shallow-inference (i.e. display)
calculus $\mathsf{D(Kt)}$ for the logic $\mathsf{Kt}$ [Kas94]. The calculus
$\mathsf{D(Kt)}$ can be seen as a ‘one-sided’ display calculus that equates
nested sequents with structures.

$\Gamma,{\circ}[\Delta]$ $(r\\!f)$ ${\bullet}[\Gamma],\Delta$ |  $\Gamma,\blacklozenge A,{\bullet}[\Delta,A]$ $(\blacklozenge)$ $\Gamma,\blacklozenge A,{\bullet}[\Delta]$
---|---

The rules $(r\\!f)$ and $(rp)$ are similar to Wansing’s display rule
$(\bullet)$, however, they rely on the equivalence between $\blacksquare\neg
A\lor B$ and $\neg A\lor\Box B$.

Quite significantly, Belnap’s seminal paper [Bel82] also proves a _general
cut-elimination theorem_. In other words, it is shown that if a display
calculus satisfies eight conditions (C1)–(C8), shown below, cut-elimination
follows as a corollary.

[Conditions (C1)–(C8)] Belnap’s eight conditions ensuring cut-elimination are
given below.

  * (C1)

Every formula occurring in the premise of a rule instance is a subformula of
some formula in the conclusion.

  * (C2)

A structure variable in the premise of a rule is defined to be _congruent_ to
a structure variable in the conclusion iff the two are identical.

  * (C3)

Every structure variable in the premise of a rule is congruent to at most one
structure variable in the conclusion.

  * (C4)

Congruent structure variables in an inference are either both a-parts or both
c-parts.

  * (C5)

If a formula variable is in the conclusion of a rule, then it is either the
entire antecedent or consequent.

  * (C6)

Every rule is closed under uniform substitutions of arbitrary structures in
c-parts for congruent structure variables.

  * (C7)

Every rule is closed under uniform substitutions of arbitrary structures in
a-parts for congruent structure variables.

  * (C8)

If an inference ends with $X\Rightarrow A$ and an inference ends with
$A\Rightarrow Y$ with $A$ principal in both, then either (1) $X\Rightarrow Y$
equals $X\Rightarrow A$ or $A\Rightarrow Y$, or (2) there exists a derivation
of $X\Rightarrow Y$ from the premises of each inference where $(cut)$ is only
used on proper subformulae of $A$.

######  Theorem 2 (General Cut-Elimination [Bel82]).

If a display calculus satisfies (C1)–(C8), then $(cut)$ is admissible.

The display formalism has been used to supply truly sizable classes of logics
with cut-free proof systems, proving the formalism general. Furthermore, the
formalism is highly uniform and modular as structural rules are used to
capture distinct logics, and due to the algorithms permitting their
construction [CR16, GMP+18], they enjoy constructibility. These nice features
come at the cost of syntactic parsimony however as display sequents utilize
complex structures to facilitate reasoning.

###  2.7. Labeled Sequents

Labeled sequents generalize Gentzen-style sequents by annotating formuale with
labels and introducing semantic elements into the syntax of sequents. For
example, the labeled sequents used for intuitionistic and modal logics (cf.
[Sim94, Vig00]) are typically of the form shown below top in the following
example and encode a graph of the form shown below bottom. One can see that
labeled sequents employ arbitrary graphs of Gentzen-style sequents which
properly generalizes all sequents considered in previous sections.

A labeled sequent is shown below top and its corresponding graph is shown
below bottom.

$\underbrace{wRu,uRv,vRw,zRz}_{\text{Relational
Atoms}},\underbrace{w:A,u:B,v:C}_{\text{Labeled Formulae}}\
\Rightarrow\underbrace{u:D,z:E,z:F}_{\text{Labeled Formulae}}$
$\overset{\boxed{A\Rightarrow\emptyset}}{w}$$\overset{\boxed{B\Rightarrow
C}}{u}$$\overset{\boxed{D\Rightarrow\emptyset}}{v}$$\overset{\boxed{\emptyset\Rightarrow
E,F}}{z}$

The idea of labeling formulae in sequents comes from Kanger [Kan57], who made
use of _spotted formulae_ (now called _labeled formulae_) to construct sequent
systems for normal modal logics.888We note that labeling has also been used in
tableaux for modal logics, e.g. the prefixed tableaux of Fitting [Fit72]. The
work of Kanger inspired the construction of labeled sequent systems for
numerous types of logics; e.g., intuitionistic (modal) logics [DN12, Sim94],
normal modal logics [Hei05, Min97, Neg05, Vig00], predicate modal logics
[CS02, KO03], relevance logics [Vig00], (deontic) agency logics [vBL19, vBL21,
LvB19], and a variety of other non-classical logics [DON18, Gab96].

The labeled sequent formalism has been remarkably successful in producing
classes of proof systems that cover extensive classes of logics in a uniform
and modular manner. This uniformity and modularity is typically obtained by
taking a _base calculus_ for a particular logic and showing that through the
addition of structural rules the calculus can be extended into a calculus for
another logic within a specified class. A favorable feature of the labeled
sequent formalism is the existence of general theorems confirming properties
such as cut-admissibility, invertibility of rules, and admissibility of
standard structural rules [DN12, Neg05, Sim94, Vig00]. Another desirable
characteristic concerns the ease with which labeled systems are constructed;
e.g., for logics with a Kripkean semantics one straightforwardly obtains
labeled calculi by transforming the semantic clauses and frame/model
conditions into inference rules. In fact, the process of constructing labeled
calculi for logics with a Kripkean semantics (e.g. modal or intermediate
logics) has been shown to be automatable [CMS13]. Thus, the labeled formalism
is highly general, uniform, modular, and constructible, but as with the
display formalism, this comes at a cost of syntactic complexity.

To provide the reader with intuition about the generality, uniformity, and
modularity of labeled sequent systems we consider a specific system for the
tense logic $\mathsf{Kt}$ (cf. [CLRT21, Vig00]). The labeled sequents used are
defined to be formulae of the form $\mathcal{R}\Rightarrow\Gamma$, where
$\mathcal{R}$ is a multiset of relational atoms of the form $wRu$ and $\Gamma$
is a multiset of labeled formulae of the form $w:A$ with
$A\in\mathcal{L}_{T}$. The labeled sequent system $\mathsf{L(Kt)}$ is
presented in Figure 10 and contains the axiom $(id)$ as well as six logical
rules; note that the $(\Box)$ and $(\blacksquare)$ rules is subject to a side
condition, namely, the label $u$ must be _fresh_ and not occur in the
conclusion of a rule application.

$(id)$ $\mathcal{R}\Rightarrow w:p,w:\neg p,\Gamma$ |  $\mathcal{R}\Rightarrow w:A,w:B,\Gamma$ $(\lor)$ $\mathcal{R}\Rightarrow w:A\lor B,\Gamma$
---|---

$\mathcal{R}\Rightarrow w:A,\Gamma$ $\mathcal{R}\Rightarrow w:B,\Gamma$
$(\land)$ $\mathcal{R}\Rightarrow w:A\land B,\Gamma$
---

$\mathcal{R},wRu\Rightarrow w:\Diamond A,u:A,\Gamma$ $(\Diamond)$ $\mathcal{R},wRu\Rightarrow w:\Diamond A,\Gamma$ |  $\mathcal{R},uRw\Rightarrow w:\blacklozenge A,u:A,\Gamma$ $(\blacklozenge)$ $\mathcal{R},uRw\Rightarrow w:\blacklozenge A,\Gamma$
---|---

$\mathcal{R},wRu\Rightarrow u:A,\Gamma$ $(\Box)$ $\mathcal{R}\Rightarrow w:\Box A,\Gamma$ |  $\mathcal{R},uRw\Rightarrow u:A,\Gamma$ $(\blacksquare)$ $\mathcal{R}\Rightarrow w:\blacksquare A,\Gamma$
---|---

Side condition: $u$ must be fresh in $(\Box)$ and $(\blacksquare)$.

Figure 10. The labeled sequent system $\mathsf{L(Kt)}$ for the tense logic
$\mathsf{Kt}$ [Bor08, CLRT21].

This calculus may be extended with structural rules to obtain labeled sequent
systems for _extensions_ of $\mathsf{Kt}$ (e.g. tense $\mathsf{S4}$ and
$\mathsf{S5}$). Such rules encode frame properties corresponding to axioms.
For example, to obtain a labeled sequent system for $\mathsf{Kt}$ with serial
frames one can extend $\mathsf{L(Kt)}$ with the $(ser)$ rule shown below, and
to obtain a labeled sequent calculus for tense $\mathsf{S4}$ one can extend
$\mathsf{L(Kt)}$ with the structural rules $(ref)$ and $(tra)$.

$\mathcal{R},wRu\Rightarrow\Gamma$ $(ser)$ $u$ fresh $\mathcal{R}\Rightarrow\Gamma$ |  $\mathcal{R},wRw\Rightarrow\Gamma$ $(ref)$ $\mathcal{R}\Rightarrow\Gamma$
---|---

$\mathcal{R},wRu,uRv,wRv\Rightarrow\Gamma$ $(tra)$
$\mathcal{R},wRu,uRv\Rightarrow\Gamma$

In fact, most commonly studied frame properties for logics with Kripkean
semantics (such as seriality, reflexivity, and transitivity) can be
transformed into equivalent structural rules. Simpson shown that a large class
of properties, referred to as _geometric axioms_ , could be transformed into
equivalent structural rules, referred to as _geometric rules_ , in labeled
sequent calculi [Sim94]. A geometric axiom is a formula of the form shown
below, where each $A_{i}$ and $B_{j,k}$ is a first-order atom.

$\forall x_{1},\ldots,x_{t}\big{(}A_{1}\land\cdots\land
A_{n}\rightarrow\exists
y_{1},\ldots,y_{s}(\bigvee_{j=1}^{m}\bigwedge_{k=1}^{l_{j}}B_{1,k})\big{)}$

Each geometric formula is equivalent to the geometric rule of the form shown
below, where $\overline{A}:=A_{1},\ldots,A_{n}$,
$\overline{B}_{j}:=B_{j,1},\ldots,B_{j,l_{j}}$, and each variable
$y_{1},\ldots,y_{s}$ is fresh, i.e. the rule can be applied only if none of
the variables $y_{1},\ldots,y_{s}$ occur in the conclusion.

$\mathcal{R},\overline{A},\overline{B}_{1},\Gamma\Rightarrow\Delta$ $\cdots$
$\mathcal{R},\overline{A},\overline{B}_{m},\Gamma\Rightarrow\Delta$
$\mathcal{R},\overline{A},\Gamma\Rightarrow\Delta$

In Figure 11 is a selection of structural rules that are typically admissible
in labeled sequent systems with geometric rules. The weakening rules
$(wk_{l})$ and $(wk_{r})$ add additional formulae to the antecedent and
consquent of a labeled sequent, the contraction rules $(ctr_{l})$ and
$(ctr_{r})$ remove additional copies of formulae, and the substitution rule
$(ls)$ replaces a label $u$ with a label $w$ in a labeled sequent. Also, the
$(cut)$ rule is usually admissible and the $(lft)$ rule is admissible in
intuitionistic systems. Such admissibility results tend to hold generally for
labeled sequent systems, along with all logical rules being invertible [DN12,
Hei05, LvB19, Sim94]. Beyond admissibility and invertibility properties,
labeled systems allow for easy counter-model extraction due to the
incorporation of semantic notions into the syntax of sequents, though
termination of proof-search is not easily achieved as labeled sequents contain
a large amount of structure.

$\mathcal{R},\Gamma\Rightarrow\Delta$ $(wk_{l})$ $\mathcal{R},\Gamma,w:A\Rightarrow\Delta$ |  $\mathcal{R},\Gamma,w:A,w:A\Rightarrow\Delta$ $(ctr_{l})$ $\mathcal{R},\Gamma,w:A\Rightarrow\Delta$
---|---

$\mathcal{R},\Gamma\Rightarrow w:A,w:A,\Delta$ $(ctr_{r})$ $\mathcal{R},\Gamma\Rightarrow w:A,\Delta$ |  $\mathcal{R},w\leq u,\Gamma,w:A,u:A\Rightarrow\Delta$ $(lft)$ $\mathcal{R},w\leq u,\Gamma,w:A\Rightarrow\Delta$
---|---

$\mathcal{R},\Gamma\Rightarrow\Delta$ $(ls)$ $\mathcal{R}[w/u],\Gamma[w/u]\Rightarrow\Delta[w/u]$ |  $\mathcal{R},\Gamma\Rightarrow w:A,\Delta$ $\mathcal{R},\Gamma,w:A\Rightarrow\Delta$ $(cut)$ $\mathcal{R},\Gamma\Rightarrow\Delta$
---|---

Figure 11. Labeled structural rules.

Last, we note that although $(cut)$ is usually admissible in labeled sequent
systems, it is often the case that a _strict_ form of the subformula property
fails to hold. In other words, in the labeled setting cut-admissibility does
not typically imply that every formula occurring within a cut-free derivation
is a subformula of the conclusion. This phenomenon arises due to the
incorporation of geometric rules which may delete relational atoms from the
premise when inferring the conclusion. Nevertheless, it is usually the case
that labeled sequent systems possess a _weak_ version of the subformula
property, i.e. it can be shown that every _labeled formula_ occurring in a
derivation is a subformula of some labeled formula in the conclusion [Neg05,
Vig00].

##  3\. Navigating the Proof-Theoretic Jungle

As discussed in Section 2 and shown in Figure 2, the data structure underlying
sequents naturally imposes a hierarchy on the various types of proof systems
we have been considering. At the base of this hierarchy sits Gentzen-style
sequents, which are incrementally generalized at each level of the hierarchy
by defining ever more complex data structures, until labeled sequents are
reached at the top. As we are interested in exploring this hierarchy, we
present translations of proofs between systems in different proof-theoretic
formalisms, thus letting us ‘shift’ derivations up and down the hierarchy. The
lesson we learn is that translating proofs down the hierarchy requires
significantly more work than translating proofs up the hierarchy.

###  3.1. Translations for $\mathsf{S5}$: Labeled and Hypersequent Calculi

We begin our demonstration of how to translate proofs between distinct proof-
theoretic formalisms by considering translations in the context of the normal
modal logic $\mathsf{S5}$. By utilizing the simplified $\mathsf{S5}$ semantics
(see Definition 1), we may formulate a relatively simple labeled sequent
calculus for $\mathsf{S5}$ (shown in Figure 12), which permits a
straightforward translation into a hypersequent calculus for the logic.

$(id)$ $\Gamma,w:p\Rightarrow w:p,\Delta$ |  $\Gamma,w:A,\Rightarrow\Delta$ $(\neg_{r})$ $\Gamma\Rightarrow w:\neg A,\Delta$
---|---

$\Gamma,\Rightarrow w:A,\Delta$ $\Gamma,w:B\Rightarrow\Delta$ $(\rightarrow_{l})$ $\Gamma,w:A\rightarrow B\Rightarrow\Delta$ |  $\Gamma,w:A\Rightarrow w:B,\Delta$ $(\rightarrow_{l})$ $\Gamma\Rightarrow w:A\rightarrow B,\Delta$
---|---

$\Gamma\Rightarrow\Delta,y:A$ $(\Box_{r})$ $\Gamma\Rightarrow\Delta,x:\Box A$ |  $\Gamma,x:\Box A,y:A\Rightarrow\Delta$ $(\Box_{l})$ $\Gamma,x:\Box A\Rightarrow\Delta$
---|---

Side conditions: $y$ is fresh in $(\Box_{r})$ and $y\in\Gamma\cup\Delta$ in
$(\Box_{l})$.

Figure 12. The labeled calculus $\mathsf{L(\mathsf{S5})}$ for the modal logic
$\mathsf{S5}$.

A labeled calculus for $\mathsf{S5}$ can be obtained by adding the
$(\Box_{l})$ and $(\Box_{r})$ rules (shown in Figure 12) to a labeled version
of the classical propositional calculus, that is, a calculus consisting of the
rules $(id)$, $(\neg_{l})$, $(\neg_{r})$, $(\rightarrow_{l})$, and
$(\rightarrow_{l})$ (also shown in Figure 12). We note that our calculus
utilizes labeled sequents of the form $\Gamma\Rightarrow\Delta$, where
$\Gamma$ and $\Delta$ are (potentially empty) multisets of labeled formulae of
the form $w:A$ with $w$ among a denumerable set $\\{w,u,v,\ldots\\}$ of labels
and $A\in\mathcal{L}_{M}$. For a multiset $\Gamma$ of labeled formulae, we
define $\Gamma_{w}$ to be the multiset $\\{w:A\ |\ w:A\in\Gamma\\}$ and we
define $\Gamma\restriction w$ to be the multiset $\\{A\ |\ w:A\in\Gamma\\}$.
Using this notation, we re-write the $(\Box_{l})$ and $(\Box_{r})$ rules in a
more convenient notation by partitioning the antecedents and consequents of
the rules.

For the rule $(\Box_{l})$, we distinguish when a formula $w_{i}:\Box A$ is
propagated to the same $w_{i}$, or to a different $w_{j}$ (when the rule is
applied bottom-up). In the the first case, the rule may be formalized as
follows:

$\Gamma_{w_{1}},\ldots,\Gamma_{w_{i}}\cup\\{w_{i}:\Box
A,w_{i}:A\\},\ldots,\Gamma_{w_{n}}\Rightarrow\Delta$ $(\Box_{l1})$
$\Gamma_{w_{1}},\ldots,\Gamma_{w_{i}}\cup\\{w_{i}:\Box
A\\},\ldots,\Gamma_{w_{n}}\Rightarrow\Delta$

In the second case, the rule may be presented accordingly:

$\Gamma_{w_{1}},\ldots,\Gamma_{w_{i}}\cup\\{w_{i}:\Box
A\\},\ldots,\Gamma_{w_{j}}\cup\\{w_{j}:A\\},\ldots,\Gamma_{w_{n}}\Rightarrow\Delta$
$(\Box_{l2})$ $\Gamma_{w_{1}},\ldots,\Gamma_{w_{i}}\cup\\{w_{i}:\Box
A\\},\ldots,\Gamma_{w_{j}},\ldots,\Gamma_{w_{n}}\Rightarrow\Delta$

In both rules above, we assume that the labels $w_{1},\ldots,w_{n}$ are all
labels occurring in the antecedent of the premise.

For the $(\Box_{r})$ rule, we assume that the labels
$w_{1},\ldots,w_{n},w_{n+1}$ are all labels occurring in the consequent of the
premise. The rule may be re-written as shown below, and is subject to the side
condition that $w_{n+1}$ is fresh.

$\Gamma\Rightarrow\Delta_{w_{1}},\ldots,\Delta_{w_{i}},\ldots\Delta_{w_{n}},\\{w_{n+1}:A\\}$
$(\Box_{r})$
$\Gamma\Rightarrow\Delta_{w_{1}},\ldots,\Delta_{w_{i}}\cup\\{w_{i}:\Box
A\\},\ldots,\Delta_{w_{n}}$

We obtain an hypsersequent calculus by making each Gentzen-style sequent
$\Gamma\restriction{w_{i}}\Rightarrow\Delta\restriction{w_{i}}$ a component of
a hypersequent. Thus, supposing that $w_{1},\ldots,w_{n}$ are all labels
occurring in a labeled sequent $\Gamma\Rightarrow\Delta$, we may define the
corresponding hypersequent as:

$(\Gamma\restriction{w_{1}}\Rightarrow\Delta\restriction{w_{1}})\mid\ldots\mid(\Gamma\restriction{w_{n}}\Rightarrow\Delta\restriction{w_{n}})$

Since labels do not occur in the above formula, it is unnecessary to keep the
labels $w_{i}$ occurring as indexed. Hence, we may write the above
hypersequent more simply as:

$\Gamma_{1}\Rightarrow\Delta_{1}\mid\ldots\mid\Gamma_{n}\Rightarrow\Delta_{n}$

We may now translate the above (labeled) rules into hypersequent notation, as
shown below:

$\Gamma_{1}\Rightarrow\Delta_{1}\mid\ldots\mid\Gamma_{i},\Box
A,A\Rightarrow\Delta_{i}\mid\ldots\mid\Gamma_{n}\Rightarrow\Delta_{n}$
$(\Box_{l1})$ $\Gamma_{1}\Rightarrow\Delta_{1}\mid\ldots\mid\Gamma_{i},\Box
A\Rightarrow\Delta_{i}\mid\ldots\mid\Gamma_{n}\Rightarrow\Delta_{n}$

$\Gamma_{1}\Rightarrow\Delta_{1}\mid\ldots\mid\Gamma_{i},\Box
A\Rightarrow\Delta_{i}\mid\ldots\mid\Gamma_{j},A\Rightarrow\Delta_{j}\mid\ldots\mid\Gamma_{n}\Rightarrow\Delta_{n}$
$(\Box_{l2})$ $\Gamma_{1}\Rightarrow\Delta_{1}\mid\ldots\mid\Gamma_{i},\Box
A\Rightarrow\Delta_{i}\mid\ldots\mid\Gamma_{j}\Rightarrow\Delta_{j}\mid\ldots\mid\Gamma_{n}\Rightarrow\Delta_{n}$

$\Gamma_{1}\Rightarrow\Delta_{1}\mid\ldots\mid\Gamma_{i}\Rightarrow\Delta_{i}\mid\ldots\mid\Gamma_{n}\Rightarrow\Delta_{n}\mid\
\Rightarrow A$ $(\Box_{r})$
$\Gamma_{1}\Rightarrow\Delta_{1}\mid\ldots\mid\Gamma_{i}\Rightarrow\Delta_{i},\Box
A\mid\ldots\mid\Gamma_{n}\Rightarrow\Delta_{n}$

Since the order is immaterial, we can focus on the first (two) component(s)
and abbreviate all the others with the side hypersequent $H$. Thus, we rewrite
the rules in their standard formulation:

$\Gamma,\Box A,A\Rightarrow\Delta\mid H$ $(\Box_{l1})$ $\Gamma,\Box A\Rightarrow\Delta\mid H$ |  $\Gamma_{1},\Box A\Rightarrow\Delta_{1}\mid\Gamma_{2},A\Rightarrow\Delta_{2}\mid H$ $(\Box_{l2})$ $\Gamma_{1},\Box A\Rightarrow\Delta_{1}\mid\Gamma_{2}\Rightarrow\Delta_{2}\mid H$
---|---

$\Gamma\Rightarrow\Delta\mid\ \Rightarrow A\mid H$ $(\Box_{r})$
$\Gamma\Rightarrow\Delta,\Box A\mid H$

We now establish a correspondence between the labeled calculus for
$\mathsf{S5}$ and the hypersequent calculus, obtained as described above by
translating each labeled rule into a hypersequent rule. Toward this end, we
define the translation of a labeled sequent $\Gamma\Rightarrow\Delta$ as
follows:

$\mathcal{H}(\Gamma\Rightarrow\Delta)=(\Gamma\restriction{w_{1}}\Rightarrow\Delta\restriction{w_{1}})\mid\ldots\mid(\Gamma\restriction{w_{n}}\Rightarrow\Delta\restriction{w_{n}})$

where $w_{1},\ldots,w_{n}$ are all labels occurring in the input labeled
sequent. There is a one to one correspondence between the rules of the labeled
calculus and rules of the hypersequent calculus, obtained by applying the
above translation to all rules of $\mathsf{L(\mathsf{S5})}$. Regarding the
hypersequent calculus, we remark that the calculus does not require structural
rules for its completeness; e.g. rules such as external weakening or
contraction are admissible in the calculus. Thus, by allowing implicit
applications of external exchange, we obtain the following result.

######  Proposition 3.

There is an isomorphism between derivations in the labeled calculus
$\mathsf{L(\mathsf{S5})}$ and derivations in the corresponding hypersequent
calculus.

######  Proof 3.1.

Every rule $(r)$ in $\mathsf{L(\mathsf{S5})}$ of the form shown below left may
be translated into a corresponding rule via $\mathcal{H}$ as shown below
right:

$\Gamma_{1}\Rightarrow\Delta_{1},\ \ldots,\Gamma_{n}\Rightarrow\Delta_{n}$ $(r)$ $\Gamma\Rightarrow\Delta$ | $\leadsto$ |  $\mathcal{H}(\Gamma_{1}\Rightarrow\Delta_{1}),\ \ldots,\mathcal{H}(\Gamma_{n}\Rightarrow\Delta_{n})$ $(r)$ $\mathcal{H}(\Gamma\Rightarrow\Delta)$
---|---|---

We show an example of corresponding derivations in the two calculi. We
consider proofs of $\neg\Box p\rightarrow\Box\neg\Box p$, namely an instance
of the $\mathsf{5}$ axiom.

$z:\Box p,y:p\Rightarrow,y:p$ $(\Box_{l2})$ $z:\Box p\Rightarrow,y:p$ $(\neg_{r})$ $\Rightarrow y:p,z:\neg\Box p$ $(\Box_{r})$ $\Rightarrow y:p,x:\Box\neg\Box p$ $(\Box_{r})$ $\Rightarrow x:\Box p,x:\Box\neg\Box p$ $(\neg_{l})$ $x:\neg\Box p\Rightarrow x:\Box\neg\Box p$ $(\rightarrow_{l})$ $\Rightarrow x:\neg\Box p\rightarrow\Box\neg\Box p$ |  $\Rightarrow\ \mid\ p\Rightarrow p\mid\ \Box p\Rightarrow$ $(\Box_{l2})$ $\Rightarrow\ \mid\ \Rightarrow p\mid\ \Box p\Rightarrow$ $(\neg_{r})$ $\Rightarrow\ \mid\ \Rightarrow p\mid\ \Rightarrow\neg\Box p$ $(\Box_{r})$ $\Rightarrow\Box\neg\Box p\mid\ \Rightarrow p$ $(\Box_{r})$ $\Rightarrow\Box p,\Box\neg\Box p$ $(\neg_{l})$ $\neg\Box p\Rightarrow\Box\neg\Box p$ $(\rightarrow_{l})$ $\Rightarrow\neg\Box p\rightarrow\Box\neg\Box p$
---|---

###  3.2. From Hypersequents to Sequents with Cuts

Hypersequent calculi are more expressive than sequent calculi since the latter
are a particular case of the former. There are logics that possess a cut-free
hypersequent calculus but for which no cut-free sequent calculus is known.
This is the case, for instance, of the modal logic S5. A syntactic
transformation from cut-free hypersequent calculi to sequent calculi with cuts
whose cut-formulas have a certain bounded shape has been introduced in
[CLR21]. The transformation works for large classes of substructural and modal
logics.

Given a proof of a sequent in the hypersequent calculus, the high-level idea
is to progressively convert hypersequents to sequents (with the addition of
cuts), starting from each “peculiar” hypersequent rule working downwards
towards the root. The key observation here is that we can extract a sequent
calculus from a hypersequent calculus that does not make use of hypersequent
rules, other than $(EW)$ and $(EC)$, that operates on more than one
components. The subformula property in the hypersequent calculus is used to
bound the form of the sequent cuts that need to be introduced. We sketch below
the argument for S5999This argument provides an alternative proof of Takano’s
result [Tak92]., whose corresponding sequent calculus – obtained by adding to
the calculus for S4 the rule

$\Box\Gamma\Rightarrow A,\Box\Delta$ $(5)$ $\Box\Gamma\Rightarrow\Box
A,\Box\Delta$

only uses bounded cuts of a special form: analytic cuts, that are cuts in
which the cut formula is a subformula of the conclusion.

The translation: First notice that the peculiar rule $(s5^{\prime})$ for S5 in
Section 2.2 can be replaced by the equivalent version below

$G\mid\square A,\Gamma^{\prime}\Rightarrow\Pi$ $G\mid\square
A\Rightarrow\mid\Gamma^{\prime}\Rightarrow\Pi$

Consider a cut-free hypersequent derivation $d$ of a sequent
$\Sigma\Rightarrow\Delta$. For simplicity, suppose that $d$ contains a single
instance of the above rule. From this instance, we can obtain the following
derivations in this hypersequent calculus:

$\Box A\Rightarrow\Box A$ $(ew)$ $G\;\mid\;\Box A\Rightarrow\Box A\;\mid\;\Gamma^{\prime}\Rightarrow\Pi,\Box A$ |  $G\;\mid\;\Box A,\Gamma^{\prime}\Rightarrow\Pi$ $(ew)$ $G\;\mid\;\Box A\Rightarrow\;\mid\;\Box A,\Gamma^{\prime}\Rightarrow\Pi$
---|---

Above left (right), the component $\Box A\Rightarrow\Box A$ (resp. $\Box
A,\Gamma^{\prime}\Rightarrow\Pi$) has a $\Box A$ in the consequent (resp.
antecedent) that was not present in the original derivation $d$. Proceed
downward from each hypersequent following the rules in $d$, (propagating also
these additional $\Box A$ formulas downwards from premise to conclusion). This
is not possible only if the $(4)$ rule is encountered as this rule permits
only a single formula in the consequent and the additional $\Box A$ in the
consequent would violate this. Solution: use $(5)$ at this point instead of
$(4)$. In this way we obtain hypersequent derivations that does not make use
of the peculiar structural rule of S5 of $\Box A,\Sigma\Rightarrow\Delta$ and
$\Sigma\Rightarrow\Delta,\Box A$. As none of the rules in these derivations
operate on more than one component, we can extract out of them sequent
derivations. The claim follows by applying the cut-rule on $\Box A$ (which is
an analytic cut formula as it did occur in the cut-free hypersequent
derivation $d$).

###  3.3. Translations for $\mathsf{Kt}$: Labeled and Display Calculi

We show how to translate proofs from $\mathsf{L(Kt)}$ into $\mathsf{D(Kt)}$.
The method of translation we present was first defined in [CLRT21] and is
strong enough to not only translate labeled proofs into display proofs for
$\mathsf{Kt}$, but also for any extension of $\mathsf{Kt}$ with _path axioms_
of the form
$\langle?\rangle_{1}\cdots\langle?\rangle_{n}p\rightarrow\langle?\rangle_{n+1}p$
with $\langle?\rangle_{i}\in\\{\blacklozenge,\Diamond\\}$ for $1\leq i\leq
n+1$. We note that the converse translation from $\mathsf{D(Kt)}$ to
$\mathsf{L(Kt)}$ is simpler so we omit it, though the details can be found in
[CLRT21] for the interested reader.

The key to translating labeled proofs into display proofs is to recognize that
‘non-treelike’ data (e.g. loops and cycles) cannot occur in proofs of
theorems. We refer to these labeled sequents as _labeled polytree sequents_
[CLRT21] and define them below. This insight is useful as labeled polytree
sequents and display sequents are notational variants of one another, which
facilitates our translation from $\mathsf{L(Kt)}$ to $\mathsf{D(Kt)}$.

[Labeled Polytree] Let $\Lambda:=\mathcal{R},\Gamma\Rightarrow\Delta$ be a
labeled sequent, and define the graph $G(\mathcal{R})=(V,E)$ such that $V$ is
the set of labels ocurring in $\mathcal{R}$ and $E=\\{(w,u)\ |\
wRu\in\mathcal{R}\\}$. We define $\Lambda$ to be a _labeled polytree sequent_
iff $\mathcal{R}$ forms a polytree, i.e. the graph $G(\mathcal{R})$ is
connected and cycle-free, and all labels in $\Gamma,\Delta$ occur in
$\mathcal{R}$ (unless $\mathcal{R}$ is empty, in which case every labeled
formula in $\Gamma,\Delta$ must share the same label). We define a _labeled
polytree derivation_ to be a derivation containing only labeled polytree
sequents.

######  Lemma 4.

Every derivation of a formula $A$ in $\mathsf{L(Kt)}$ is a labeled polytree
derivation.

######  Proof 3.2.

Suppose we are given a derivation of the labeled polytree sequent $\Rightarrow
w:A$ in $\mathsf{L(Kt)}$. Observe that every rule of $\mathsf{L(Kt)}$, if
applied bottom-up to a labeled polytree sequent, yields a labeled polytree
sequent since rules either preserve the set $\mathcal{R}$ of relational atoms
when applied bottom-up (e.g. $(\lor)$ and $(\Diamond)$), or via $(\Box)$ or
$(\blacksquare)$, add a new relational atom from a label occurring in the
labeled sequent to a fresh label (which has the effect of adding a new forward
or backward edge in the polytree encoded by the labeled sequent). Hence, the
derivation of $\Rightarrow w:A$ in $\mathsf{L(Kt)}$ must be a labeled polytree
derivation.

We now define the $\mathrm{D}$ function that maps labeled polytree sequents to
display sequents, which can be stepwise applied to translate entire labeled
polytree proofs into display proofs. As it will be useful here, and later on,
we define the _sequent composition_ $\Lambda\odot\Lambda^{\prime}$ between two
labeled sequents $\Lambda=\mathcal{R}\Rightarrow\Gamma$ and
$\Lambda^{\prime}=\mathcal{R}^{\prime}\Rightarrow\Gamma^{\prime}$ to be
$\Lambda\odot\Lambda^{\prime}:=\mathcal{R},\mathcal{R}^{\prime}\Rightarrow\Gamma,\Gamma^{\prime}$.

[Translation $\mathrm{D}$] Let $\Lambda:=\mathcal{R}\Rightarrow\Gamma$ be a
labeled polytree sequent containing the label $u$. We define
$\Lambda^{\prime}\subseteq\Lambda$ iff there exists a labeled polytree sequent
$\Lambda^{\prime\prime}$ such that
$\Lambda=\Lambda^{\prime}\odot\Lambda^{\prime\prime}$. Let us define
$\Lambda_{u}:=\mathcal{R}^{\prime}\Rightarrow\Gamma^{\prime}$ to be the unique
labeled polytree sequent rooted at $u$ such that $\Lambda_{u}\subseteq\Lambda$
and $\Gamma^{\prime}\restriction u=\Gamma\restriction u$. We define
$\mathrm{D}_{u}(\Lambda)$ recursively on the polytree structure of $\Lambda$:

Base case. If $\mathcal{R}=\emptyset$, then
$\mathrm{D}_{v}(\Lambda):=(\Rightarrow\Gamma\restriction v)$.

Inductive step. If $vRx_{1},\ldots vRx_{n}$ and $y_{1}Rv,\ldots y_{n}Rv$ are
all relational atoms of the form $vRx$ and $yRx$, respectively, then

$\mathrm{D}_{v}(\Lambda):=\Gamma\restriction
v,{\circ}[\mathrm{D}_{x_{1}}(\Lambda_{x_{1}})],\ldots,{\circ}[\mathrm{D}_{x_{n}}(\Lambda_{x_{n}})],{\bullet}[\mathrm{D}_{y_{1}}(\Lambda_{y_{1}})],\ldots,{\bullet}[\mathrm{D}_{y_{k}}(\Lambda_{y_{k}})].$

We let $\Lambda=\ wRv,vRu\Rightarrow w:\Diamond q,w:r\lor
q,v:p,v:q,u:\blacksquare p$ and show the output display sequent for $w$, $u$,
and $v$.

$\displaystyle\mathrm{D}_{w}(\Lambda)$ $\displaystyle=\Diamond q,r\lor
q,{\circ}[p,q,,{\circ}[\blacksquare p]]$
$\displaystyle\mathrm{D}_{v}(\Lambda)$ $\displaystyle={\bullet}[\Diamond
q,r\lor q],p,q,{\circ}[\blacksquare p]$ $\displaystyle\mathrm{D}_{u}(\Lambda)$
$\displaystyle={\bullet}[{\bullet}[\Diamond q,r\lor q],p,q],\blacksquare p$

We find something interesting if we observe the display sequents
$\mathrm{D}_{w}(\Lambda)$, $\mathrm{D}_{v}(\Lambda)$, and
$\mathrm{D}_{u}(\Lambda)$ above, namely, each display sequent is derivable
from the other by means of the display rules $(r\\!f)$ and $(rp)$. In fact, as
stated in the following lemma, this relationship holds generally; its proof
can be found in [CLRT21].

######  Lemma 5.

If $\Lambda=\mathcal{R}\Rightarrow\Gamma$ is a labeled polytree sequent with
labels $w$ and $u$, then $\mathrm{D}_{w}(\Lambda)$ and
$\mathrm{D}_{u}(\Lambda)$ are display equivalent, i.e. both are mutually
derivable with the $(r\\!f)$ and $(rp)$ rules.

Relying on Lemma 4 and 5, we can define a proof translation from
$\mathsf{L(Kt)}$ to $\mathsf{D(Kt)}$ as specified in the proof of the
following theorem.

######  Theorem 6.

Every proof of a formula $A$ in $\mathsf{L(Kt)}$ can be step-wise translated
into a proof of $A$ in $\mathsf{D(Kt)}$.

######  Proof 3.3.

Suppose we are given a proof of a formula $A$ in $\mathsf{L(Kt)}$, we know by
Lemma 10 that the proof is a labeled polytree proof, and thus, $\mathrm{D}$ is
defined for every labeled sequent in the proof. We show that the proof can be
translated into a proof in $\mathsf{D(Kt)}$ by induction on the height of the
proof. We only consider the $(\Box)$ and $(\blacklozenge)$ cases of the
inductive step as the remaining cases are trivial or similar.

$\mathcal{R},wRu\Rightarrow u:A,\Gamma$ $(\Box)$ $\mathcal{R}\Rightarrow w:\Box A,\Gamma$ | $\leadsto$ |  $\mathrm{D}_{w}(\mathcal{R},wRu\Rightarrow u:A,\Gamma)$ = $\mathrm{D}_{w}(\mathcal{R}\Rightarrow\Gamma),{\circ}[A]$ $(\Box)$ $\mathrm{D}_{w}(\mathcal{R}\Rightarrow\Gamma),\Box A$ = $\mathrm{D}_{w}(\mathcal{R}\Rightarrow w:\Box A,\Gamma)$
---|---|---

$\mathcal{R},wRu\Rightarrow u:A,\Gamma$ $(\blacklozenge)$ $\mathcal{R}\Rightarrow w:\blacklozenge A,\Gamma$ | $\leadsto$ |  $\mathrm{D}_{u}(\mathcal{R},wRu\Rightarrow w:A,u:\blacklozenge A,\Gamma)$ = $X,\blacklozenge A,{\bullet}[Y,A]$ $(\blacklozenge)$ $X,\blacklozenge A,{\bullet}[Y]$ = $\mathrm{D}_{u}(\mathcal{R},wRu\Rightarrow u:\blacklozenge A,\Gamma)$
---|---|---

The remaining cases of the translation can be found in [CLRT21].

$(id)$ $\mathcal{R},w\leq u,\Gamma,w:p\Rightarrow u:p,\Delta$ |  $(\bot_{l})$ $\mathcal{R},w\leq u,\Gamma,w:\bot\Rightarrow\Delta$
---|---

$\mathcal{R},w\leq u,\Gamma,u:A\Rightarrow u:B,\Delta$ $(\supset_{r})$
$\mathcal{R},\Gamma\Rightarrow w:A\supset B,\Delta$

$\mathcal{R},\Gamma,w:A\Rightarrow\Delta$ $\mathcal{R},\Gamma,w:B\Rightarrow\Delta$ $(\lor_{l})$ $\mathcal{R},\Gamma,w:A\lor B\Rightarrow w:\Delta$ |  $\mathcal{R},\Gamma\Rightarrow w:A,w:B,\Delta$ $(\lor_{r})$ $\mathcal{R},\Gamma\Rightarrow w:A\lor B,\Delta$
---|---

$\mathcal{R},\Gamma,w:A,w:B\Rightarrow\Delta$ $(\land_{l})$ $\mathcal{R},\Gamma,w:A\land B\Rightarrow\Delta$ |  $\mathcal{R},\Gamma\Rightarrow w:A,\Delta$ $\mathcal{R},\Gamma\Rightarrow w:B,\Delta$ $(\land_{r})$ $\mathcal{R},\Gamma\Rightarrow w:A\land B,\Delta$
---|---

$\mathcal{R},w\leq u,\Gamma,w:A\supset B,u:B\Rightarrow\Delta$
$\mathcal{R},w\leq u,\Gamma,w:A\supset B\Rightarrow u:A,\Delta$
$(\supset_{l})$ $\mathcal{R},w\leq u,\Gamma,w:A\supset B\Rightarrow\Delta$
---

$\mathcal{R},w\leq w,\Gamma\Rightarrow\Delta$ $(ref)$ $\mathcal{R},\Gamma\Rightarrow\Delta$ |  $\mathcal{R},w\leq u,u\leq v,w\leq v,\Gamma\Rightarrow\Delta$ $(tra)$ $\mathcal{R},w\leq u,u\leq v,\Gamma\Rightarrow\Delta$
---|---

Side conditions: $u$ is fresh in $(\supset_{r})$.

Figure 13. The labeled sequent calculus $\mathsf{L(IL)}$ for intuitionistic
logic [DN12].

###  3.4. Translations for $\mathsf{IL}$: Labeled, Nested, and Sequent Calculi

We now consider translating proofs between the sequent calculus
$\mathsf{S(IL)}$ and a labeled calculus $\mathsf{L(IL)}$ for intuitionistic
logic shown in Figure 13. The translation from the sequent calculus to the
‘richer’ labeled sequent calculus is relatively straightforward and
demonstrates the ease with which proofs may be translated up the proof-
theoretic hierarchy (Figure 2). As traditional sequents are simpler than
labeled sequents, the converse translation requires special techniques to
remove extraneous structure from labeled proofs. To accomplish this task we
utilize structural rule elimination (cf. [Lyo21b, Lyo20a]) to first transform
labeled proofs into nested proofs in $\mathsf{N(IL)}$ (see Figure 9), and then
extract sequent proofs from these.

####  3.4.1. From Sequents to Labeled Sequents.

The labeled sequent calculus $\mathsf{L(IL)}$ (Figure 13) makes use of labeled
sequents of the form $\mathcal{R},\Gamma\Rightarrow\Delta$, where
$\mathcal{R}$ is a (potentially empty) multiset of relational atoms of the
form $w\leq u$ and $\Gamma$ and $\Delta$ are (potentially empty) multisets of
labeled formulae of the form $w:A$ with $A\in\mathcal{L}_{I}$. The theorem
below gives a translation of proofs in $\mathsf{S(IL)}$ into proofs in
$\mathsf{L(IL)}$.

######  Theorem 7.

Every proof of a sequent $\Gamma\Rightarrow\Delta$ in $\mathsf{S(IL)}$ can be
step-wise translated into a proof of $w:\Gamma\Rightarrow w:\Delta$ in
$\mathsf{L(IL)}$.

######  Proof 3.4.

We prove the result by induction on the height of the given derivation.

Base case. The $(id)$ rule is translated as shown below; translating the
$(\bot_{l})$ rule is similar.

$(id)$ $\Gamma,p\Rightarrow p,\Delta$ | $\leadsto$ |  $(id)$ $wRw,w:\Gamma,w:p\Rightarrow w:p,w:\Delta$ $(ref)$ $w:\Gamma,w:p\Rightarrow w:p,w:\Delta$
---|---|---

Inductive step. As the $(\lor_{l})$, $(\lor_{r})$, $(\land_{l})$, and
$(\land_{r})$ cases are simple, we only show the more interesting cases of
translating the $(\supset_{l})$ and $(\supset_{r})$ rules.

$(\supset_{l})$. For the $(\supset_{l})$ case, we assume we are given a
derivation in $\mathsf{S(IL)}$ ending with an application of the
$(\supset_{l})$ rule, as shown below:

$\Gamma,A\supset B,B\Rightarrow\Delta$ $\Gamma,A\supset B\Rightarrow A,\Delta$
$(\supset_{l})$ $\Gamma,A\supset B\Rightarrow\Delta$

To translate the proof and inference into the desired proof in
$\mathsf{L(IL)}$, we invoke IH, apply $(\supset_{l})$, and finally, apply
$(ref)$ as shown below:

$\mathcal{D}_{1}=$ |  IH $w\leq w,w:\Gamma,w:A\supset B,w:B\Rightarrow w:\Delta$
---|---
$\mathcal{D}_{2}=$ |  IH $w\leq w,w:\Gamma,w:A\supset B\Rightarrow w:A,w:\Delta$
---|---

$\mathcal{D}_{1}$ $\mathcal{D}_{2}$ $(\supset_{l})$ $w\leq
w,w:\Gamma,w:A\supset B\Rightarrow w:\Delta$ $(ref)$ $w:\Gamma,w:A\supset
B\Rightarrow w:\Delta$

$(\supset_{r})$. Translating the $(\supset_{r})$ rule requires more effort. We
must employ the admissibility of certain structural rules for the translation
to go through. In particular, we apply the admissibility of $(ls)$, $(wk)$,
and $(lft)$ (see Figure 11) as shown in the translated proof below right.

$\Gamma,A\Rightarrow B$ $(\supset_{r})$ $\Gamma\Rightarrow A\supset B,\Delta$ | $\leadsto$ |  IH $w:\Gamma,w:A\Rightarrow w:B$ $(ls)$ $u:\Gamma,u:A\Rightarrow u:B$ $(wk)$ $w\leq u,w:\Gamma,u:\Gamma,u:A\Rightarrow u:B$ $(lft)$ $w\leq u,w:\Gamma,u:A\Rightarrow u:B$ $(\supset_{r})$ $w\leq u,w:\Gamma\Rightarrow u:A\supset B$ $(ls)$ $w\leq w,w:\Gamma\Rightarrow w:A\supset B$ $(ref)$ $w:\Gamma\Rightarrow w:A\supset B$
---|---|---

####  3.4.2. From Labeled Sequents to Sequents.

We now consider the converse translation from $\mathsf{L(IL)}$ to
$\mathsf{S(IL)}$, which demonstrates the non-triviality of translating from
the richer labeled sequent formalism to the sequent formalism. In this
section, our main aim is to establish the following theorem:

######  Theorem 8.

Every proof of a formula $A$ in $\mathsf{L(IL)}$ can be step-wise translated
into a proof of $A$ in $\mathsf{S(IL)}$.

We prove the above theorem by establishing two lemmata: (1) we translate
labeled proofs from $\mathsf{L(IL)}$ into nested proofs in $\mathsf{N(IL)}$,
and (2) we translate nested proofs into sequent proofs in $\mathsf{S(IL)}$. We
then obtain the desired translation from $\mathsf{L(IL)}$ to $\mathsf{S(IL)}$
by composing the two aforementioned ones. We first focus on proving the
labeled to nested translation, and then argue the nested to sequent
translation.

[Labeled Tree] We define a _labeled tree sequent_ to be a labeled sequent
$\Lambda:=\mathcal{R},\Gamma\Rightarrow\Delta$ such that $\mathcal{R}$ forms a
tree and all labels in $\Gamma,\Delta$ occur in $\mathcal{R}$ (unless
$\mathcal{R}$ is empty, in which case every labeled formula in $\Gamma,\Delta$
must share the same label). We define a _labeled tree derivation_ to be a
proof containing only labeled tree sequents. We say that a labeled tree
derivation has the _fixed root property_ iff every labeled sequent in the
derivation has the same root.

[Translation $\mathrm{N}$] Let $\Lambda:=\mathcal{R},\Gamma\Rightarrow\Delta$
be a labeled tree sequent with root $u$. We define
$\Lambda^{\prime}\subseteq\Lambda$ iff there exists a labeled tree sequent
$\Lambda^{\prime\prime}$ such that
$\Lambda=\Lambda^{\prime}\odot\Lambda^{\prime\prime}$. Let us define
$\Lambda_{u}:=\mathcal{R}^{\prime},\Gamma^{\prime}\Rightarrow\Delta^{\prime}$
to be the unique labeled tree sequent rooted at $u$ such that
$\Lambda_{u}\subseteq\Lambda$, $\Gamma^{\prime}\restriction
u=\Gamma\restriction u$, and $\Delta^{\prime}\restriction u=\Delta\restriction
u$. We define $\mathrm{N}(\Lambda):=\mathrm{N}_{u}(\Lambda)$ recursively on
the tree structure of $\Lambda$:

$\mathrm{N}_{v}(\Lambda):=\begin{cases}\Gamma\restriction
v\Rightarrow\Delta\restriction v&\text{if $\mathcal{R}=\emptyset$};\\\
\Gamma\restriction v\Rightarrow\Delta\restriction
v,[\mathrm{N}_{z_{1}}(\Lambda_{z_{1}})],\ldots,[\mathrm{N}_{z_{n}}(\Lambda_{z_{n}})]&\text{otherwise}.\end{cases}$

In the second case above, we assume that $v\leq z_{1},\ldots v\leq z_{n}$ are
all of the relational atoms occurring in the input sequent which have the form
$v\leq x$.

We let $\Lambda:=w\leq v,v\leq u,v:p,u:p\Rightarrow w:p\supset q,v:r,u:q$ and
show the output nested sequent under the translation $\mathrm{N}$.

$\mathrm{N}(\Lambda)=\mathrm{N}_{w}(\Lambda)=\emptyset\Rightarrow p\supset
q,[p\Rightarrow r,[p\Rightarrow q]]$

As discussed in the section on the nested sequent formalism (Section 2.5),
propagation and reachability rules play a crucial role in the formulation of
nested sequent calculi. As we aim to transform labeled proofs in
$\mathsf{L(IL)}$ into nested sequent proofs in $\mathsf{N(IL)}$, we must
define reachability rules in the context of labeled sequents. Toward this end,
we define _directed paths_ in labeled sequents accordingly.

[Directed Path [Lyo20a]] Let $\Lambda=\mathcal{R},\Gamma\Rightarrow\Delta$ be
a labeled sequent. We say that there exists a _directed path_ from $w$ to $u$
in $\mathcal{R}$ (written $w\leadsto_{\mathcal{R}}u$) iff $w=u$, or there
exist labels $v_{i}$ (with $i\in\\{1,\ldots,n\\}$) such that $w\leq
v_{1},\ldots,v_{n}\leq u\in\mathcal{R}$ (we stipulate that $w\leq
u\in\mathcal{R}$ when $n=0$).

Directed paths are employed in the formulation of the labeled reachability
rule $(r_{id})$ and the labeled propagation rule $(p_{\supset_{l}})$, shown in
Figure 14 and based on the work of [Lyo20a, Lyo21b]. As the lemma below
demonstrates, by adding these rules to $\mathsf{L(IL)}$, the structural rules
$(ref)$ and $(tra)$ become eliminable. Since analogs of these structural rules
do not exist in $\mathsf{N(IL)}$, showing their eliminability is a crucial
step in translating proofs from the labeled setting to the (nested) sequent
setting, as discussed later on.

$(r_{id})$ $\mathcal{R},\Gamma,w:p\Rightarrow u:p,\Delta$
---

$\mathcal{R},\Gamma,w:A\supset B\Rightarrow u:A,\Delta$
$\mathcal{R},\Gamma,w:A\supset B,u:B\Rightarrow\Delta$ $(p_{\supset_{l}})$
$\mathcal{R},\Gamma,w:A\supset B\Rightarrow\Delta$
---

Side conditions: Both rules are applicable only if $w\leadsto_{\mathcal{R}}u$.

Figure 14. Reachability rules for $\mathsf{L(IL)}$.

######  Lemma 9.

The rules $(ref)$ and $(tra)$ are eliminable in
$\mathsf{L(IL)}+\\{(r_{id}),(p_{\supset_{l}})\\}$.

######  Proof 3.5.

We argue the eliminability of both rules by induction on the height of the
given derivation.