11institutetext:  TU Vienna, Austria 11email<EMAIL_ADDRESS>22institutetext:
University College London, United Kingdom 22email<EMAIL_ADDRESS>33institutetext: University of Groningen, Netherlands
33email<EMAIL_ADDRESS>
# A theory of cut-restriction: first steps

Agata Ciabattoni 11 0000-0001-6947-8772 Timo Lang 22 0000-0002-8257-968X
Revantha Ramanayake 33 0000-0002-7940-9065

###### Abstract

Cut-elimination is the bedrock of proof theory. It is the algorithm that
eliminates cuts from a sequent calculus proof that leads to cut-free calculi
and applications. Cut-elimination applies to many logics irrespective of their
semantics. Such is its influence that whenever cut-elimination is not provable
in a sequent calculus the invariable response has been a move to a richer
proof system to regain it. In this paper we investigate a radically different
approach to the latter: adapting age-old cut-elimination to restrict the shape
of the cut-formulas when elimination is not possible. We tackle the “first
level” above cut-free: analytic cuts. Our methodology is applied to the
sequent calculi for bi-intuitionistic logic and $S5$ where analytic cuts are
already known to be required. This marks the first steps in a theory of cut-
restriction.

###### Keywords:

Sequent Calculus Cut-Elimination Analytic Cut Bi-intuitionistic logic S5

##  1 Introduction

Cut-elimination is the fundamental result of proof theory. At its heart, it is
an algorithm for transforming any proof into an analytic proof, i.e. the only
formu- las that occur in the proof are subformulas of the final statement.
This is done by eliminating the most common source of non-analyticity: the
cut-rule. Though larger in size, analytic proofs are better behaved and more
amenable to meta-theoretic investigation, especially because the space of
proofs under consideration is greatly constrained. Gentzen’s motivation in the
1930’s was a finitistic proof of the consistency of arithmetic (paving the way
for ordinal analysis) but the influence of cut-elimination is far beyond that.
The cut-free calculi that are the offspring of cut-elimination are central in
structural proof theory where they are used to prove properties of the
underlying logic (e.g., consistency, decidability, upper bounds, various
flavours of interpolation, and disjunction properties), and appear as semantic
tableaux and within automated theorem proving.

Let us pick up the story in the decades following Gentzen’s seminal result.
Cut-elimination was originally proved for the sequent calculi for classical
and intuitionistic logic IL. The programme of developing cut-free calculi via
cut-elimination was soon extended to non-classical logics, notably modal
logics. The first significant obstacle was encountered in the early 1950’s:
how to eliminate cuts in the proof calculus for the modal logic $S5$? While
syntactic decision arguments for $S5$ were obtained (see Ohnishi and Matsumoto
[17, 18]), it seems that the first proof of cut-elimination was by Mints [16]
who extended the metalanguage of Gentzen’s sequent calculus to essentially
what is today called the hypersequent calculus. Hypersequent calculi were
rediscovered independently in the 1980’s, by Pottinger [21] to obtain cut-
elimination for modal logics, and Avron [1], who applied them to relevant,
modal, and intermediate logics. The floodgates had been opened: when cut-
elimination cannot be obtained for a logic of interest, the standard response
in structural proof theory is to look for (or invent) a new proof formalism by
extending the metalanguage of the sequent calculus such that cut-elimination
does hold. Most proof formalisms have been introduced in the last three
decades in this way; nested, labelled, bunched, linear, tree-hypersequent,
display sequent, and many more.

A question that has received little attention in all this time is whether it
is possible to adapt cut-elimination to simplify those cuts that are not
eliminable. This is cut-restriction, an idea (and terminology) already
introduced111 There, an algorithm to obtain sequent calculi with restricted
cuts (parametric on the end formula but not necessarily subformulas) for many
families of logics was introduced by essentially composing two algorithms: the
algorithms to transform logic specifications into cut-free hypersequent
calculi [5, 15], and the reduction of cut-free hypersequent calculi to sequent
calculi with restricted cuts. This is evidence that cut-restriction is in
principle possible on a broad and ambitious scale. in Ciabattoni et al. [6]
but not pursued. It is the subject of this paper.

A result in the spirit of cut-restriction is contained in Takano’s 1992 paper
[24] on the analytic cut property (cuts can be restricted to subformulas of
the rule conclusion) of $S5$. Even there, the argument does not appear to have
the generic character that is a hallmark of Gentzen’s arguments. Other results
restricting cuts rely on the semantics of the logics under consideration,
e.g., [11, 10, 14, 2, 25, 3, 27]. In contrast, Gentzen’s cut-elimination
method applies rather uniformly across diverse proof systems irrespective of
the logic’s semantics. A major motivation for choosing to adapt cut-
elimination as the path to restricting cuts is the ambition that it too will
be applicable as broadly.

In addition to the theoretical interest in adapting this most fundamental
notion in proof theory, there are several further motivations.

Cut-restriction is an alternative to moving to proof formalisms more complex
than the sequent calculus to obtain cut-elimination. New proof formalisms are
designed so that the cut-elimination proof goes through, but it is always
possible that the same could have been achieved using a simpler formalism. For
example, the hypersequent calculus for $S5$ manipulates arbitrarily many
component sequents although it turns out that only two are in fact required
[13]. Additional structure in the proof formalism is often a hindrance to
proving metalogical results, and for limiting the proof search space. At this
stage we do not intend to compare restricted cuts with additional structure in
a proof formalism but we do note that decidability and complexity arguments
proceed in the presence of finitely many sequent cuts, and interpolation
proofs too, at least in the case of analytic (or almost analytic) cuts, e.g.,
[24, 14]. In addition, restricted sequent cuts may also be useful from a
computational viewpoint [8], and the usual blow-up in the size of cut-free
proofs can be alleviated if one admits analytic cuts [9].

In this paper we tackle the first “level” of cut-restriction above cut-free
proofs: from arbitrary cuts to analytic cuts. The restriction to analytic cuts
is of particular conceptual interest because it corresponds directly to the
subformula property [14], whereas cut-elimination is a strictly stronger
property. We achieve this restriction by replacing Gentzen’s permutation
reductions with suitable intermediary cuts. The idea is first discussed
informally in Section 2. Our method is presented using as main case study the
sequent calculus [22] for bi-intuitionistic logic—a conservative extension of
intuitionistic logic with the connective $\prec$ dual to implication. The main
ingredients for the cut-restriction proof to go through are identified in
Section 4 and the argument is adapted to the case of the modal logic $S5$. We
emphasise that completeness of these sequent calculi with analytic cuts is
already known. For bi-intuitionistic logic it was independently proved using
semantics in Kowalski and Ono [14] and Avron and Lahav [2]. The problem of
establishing this result using proof-theoretic methods—accomplished in this
paper—was left open in [20] where it was shown that infinitely many cut-
formulas of a certain (co)implicational form ensures completeness. For $S5$,
the result dates back to Takano [24] whose proof has inspired our work. The
point in this paper is that we uncover how to obtain these results as an
adaptation of age-old cut-elimination. These are the first steps in the theory
of cut-restriction.

##  2 Cut-Elimination adapted to Cut-Restriction: the idea

Gentzen’s cut-elimination argument is well known: stepwise applications of
reductions replace cut-rules in the proof by smaller cut-rules with respect to
a well-founded relation. An appeal to (transfinite) induction ultimately
yields a cut-free proof. These stepwise reductions come in two flavours:
permutation and principal reduction. The former shifts a cut one step upwards
in either the left premise or the right premise. Following repeated
applications, the situation is reached of a cut in which the cut-formula is
principal (i.e. created by the rule immediately above it) in both premises.
The principal reduction is now used to replace that cut with cuts on proper
subformulas.

The principal reductions depend on the shape of the introduction rules and in
some cases they can be hard to find. This is what happens with the modal rule
in provability logic $GL$, for example: the change in polarity of the diagonal
formula from conclusion to premise necessitates a highly intricate and
customised principal reduction [29]. Here we will consider cut-restriction for
sequent calculi with standard rules hence the principal reductions are
unproblematic. Therefore we shift our attention to permutation reductions.

When permutation reductions fail, it is usually because a rule has some
condition that is violated when it is shifted from above the cut to below it.
The rules in Gentzen’s LJ calculus for IL have no such conditions so the
permutation reductions are unproblematic. In Maehara’s calculus for IL—a
multiple-conclusion sequent calculus in which the succedent of the
${\supset}_{R}$ rule permits no context, see, e.g. [28]— some permutation
reductions do fail. Consider the following cut (we use the notation $cut^{*}$
to indicate weakening followed by $cut$):

$\delta_{1}$ $\Gamma\Rightarrow A\supset B,\Delta$ $\delta_{2}$
$\Gamma,A\supset B,C\Rightarrow D$ $\supset_{R}$ $\Gamma,A\supset B\Rightarrow
C\supset D$ $cut^{*}$ $\Gamma\Rightarrow C\supset D,\Delta$ (1)

If we attempt to shift this cut upwards in the right premise we get

$\delta_{1}$ $\Gamma\Rightarrow A\supset B,\Delta$ $\delta_{2}$
$\Gamma,A\supset B,C\Rightarrow D$ $cut^{*}$ $\Gamma,C\Rightarrow D,\Delta$

This does not work because from $\Gamma,C\Rightarrow\Delta,D$ we cannot obtain
$\Gamma\Rightarrow\Delta,C\supset D$: the context $\Delta$ in the former
blocks the application of the ${\supset}_{R}$ rule. The solution is to
repeatedly shift the cut upwards in the left premise $\delta_{1}$ until the
cut-formula is principal there. It is not an issue if we encounter a
${\supset}_{R}$ in the left premise because this rule must be the one that
creates the cut-formula.

There is another way of expressing the composite move: trace the predecessors
of the $A\supset B$ in the left premise to identify the inference that creates
it. Assume for simplicity that there is just a single such critical inference:

$\Sigma,A\Rightarrow B$ $\supset_{R}$ $\Sigma\Rightarrow A\supset B$
$\delta_{1}$ $\Gamma\Rightarrow A\supset B,\Delta$ $\Gamma,A\supset
B,C\Rightarrow D$ $\supset_{R}$ $\Gamma,A\supset B\Rightarrow C\supset D$
$cut^{*}$ $\Gamma\Rightarrow C\supset D,\Delta$

Now shift the cut up to the critical inference to get the following picture.

$\Sigma,A\Rightarrow B$ $\supset_{R}$ $\Sigma\Rightarrow A\supset B$
$\Gamma,A\supset B,C\Rightarrow D$ $\supset_{R}$ $\Gamma,A\supset B\Rightarrow
C\supset D$ $cut^{*}$ $\Sigma,\Gamma\Rightarrow C\supset D$ $+\delta_{1}$
$\Gamma,\Gamma\Rightarrow C\supset D,\Delta$ $contr$ $\Gamma\Rightarrow
C\supset D,\Delta$

Here $+\delta_{1}$ indicates that the sequents in the ‘featured branch’ in
$\delta_{1}$—i.e. the branch from $\Sigma\Rightarrow A\supset B$ to
$\Gamma\Rightarrow A\supset B,\Delta$—are enriched with an additional multiset
(in this case $\Gamma$) in the antecedent. Since Maehara’s calculus has no
rule with a context restriction in the antecedent, $+\delta_{1}$ is well-
defined despite the additional multiset. What next? Trace the predecessors of
$A\supset B$ in the right premise of cut until $A\supset B$ becomes principal
in an inference (once again for simplicity we assume a single such critical
inference).

$\Sigma,A\Rightarrow B$ $\supset_{R}$ $\Sigma\Rightarrow A\supset B$
$\Sigma^{\prime}\Rightarrow A,\Pi$ $\Sigma^{\prime},B\Rightarrow\Pi$
$\supset_{L}$ $\Sigma^{\prime},A\supset B\Rightarrow\Pi$ $\delta_{2}$
$\Gamma,A\supset B,C\Rightarrow D$ $\supset_{R}$ $\Gamma,A\supset B\Rightarrow
C\supset D$ $cut^{*}$ $\Sigma,\Gamma\Rightarrow C\supset D$ $+\delta_{1}$
$\Gamma,\Gamma\Rightarrow C\supset D,\Delta$ $contr$ $\Gamma\Rightarrow
C\supset D,\Delta$ (2)

Shifting the cut up to the critical inference in the right premise we reach

$\Sigma,A\Rightarrow B$ $\supset_{R}$ $\Sigma\Rightarrow A\supset B$
$\Sigma^{\prime}\Rightarrow A,\Pi$ $\Sigma^{\prime},B\Rightarrow\Pi$
$\supset_{L}$ $\Sigma^{\prime},A\supset B\Rightarrow\Pi$ $cut^{*}$
$\Sigma,\Sigma^{\prime}\Rightarrow\Pi$ $+\delta_{2}$
$\Sigma,\Gamma,C\Rightarrow D$ $\supset_{R}$ $\Sigma,\Gamma\Rightarrow
C\supset D$ $+\delta_{1}$ $\Gamma,\Gamma\Rightarrow C\supset D,\Delta$ $contr$
$\Gamma\Rightarrow C\supset D,\Delta$

Here again, $+\delta_{2}$ indicates that the sequents along the featured
branch in $\delta_{2}$ are enriched with an additional multiset in the
antecedent. The cut-formula is principal in both the left and right premise so
we use the principal reduction:

$\Sigma^{\prime}\Rightarrow A,\Pi$ $\Sigma,A\Rightarrow B$ $cut^{*}$
$\Sigma,\Sigma^{\prime},\Rightarrow B,\Pi$ $\Sigma^{\prime},B\Rightarrow\Pi$
$cut^{*}$ $\Sigma,\Sigma^{\prime}\Rightarrow\Pi$ $+\delta_{2}$
$\Sigma,\Gamma,C\Rightarrow D$ $\supset_{R}$ $\Sigma,\Gamma\Rightarrow
C\supset D$ $+\delta_{1}$ $\Gamma,\Gamma\Rightarrow C\supset D,\Delta$ $contr$
$\Gamma\Rightarrow C\supset D,\Delta$ (3)

The transformation from (1) to (3) expresses cut-elimination in terms of
predecessors of the cut-formulas and principal reduction. This perspective
will help us to adapt the argument to the situation where the parametric
reductions are no longer sound and the calculus does not admit cut-
elimination.

We encounter precisely this situation in the well-known sequent calculus [22]
for bi-intuitionistic logic. This calculus is obtained from the Maehara
calculus by extending the language with coimplication $\prec$ and adding the
rules $\prec_{L}$ and $\prec_{R}$ in Fig. 1. Notice: the antecedent of the
$\prec_{L}$ rule permits no context. From (3) alone we can see that the
argument above will no longer work: $+\delta_{1}$ is not well-defined as the
additional multiset in the antecedent may block an application of $\prec_{L}$.

Our ultimate aim is to adapt the picure in (3) to obtain a proof of
$\Gamma\Rightarrow C\supset D,\Delta$ replacing the non-well-defined
derivations by cuts on subformulas of this sequent. The following adaptation
already brings us closer. Here $\land\Sigma$ is the conjunction of all
formulas in $\Sigma$ and $\Sigma\Rightarrow\land\Sigma$ has an easy cut-free
proof.

$\Sigma\Rightarrow\land\Sigma$ $\delta_{1}[\land\Sigma]$
$\Gamma\Rightarrow\Delta,\land\Sigma$ $\Sigma^{\prime}\Rightarrow A,\Pi$
$\Sigma,A\Rightarrow B$ $cut^{*}$ $\Sigma,\Sigma^{\prime},\Rightarrow B,\Pi$
$\Sigma^{\prime},B\Rightarrow\Pi$ $cut^{*}$
$\Sigma,\Sigma^{\prime}\Rightarrow\Pi$ some $\land_{L}$’s
$\land\Sigma,\Sigma^{\prime}\Rightarrow\Pi$ $+\delta_{2}$
$\land\Sigma,\Gamma,C\Rightarrow D$ $\supset_{R}$
$\land\Sigma,\Gamma\Rightarrow C\supset D$ $cut^{*}$
$\Gamma\Rightarrow\Delta,C\supset D$ (4)

We denote by $\delta_{1}[\land\Sigma]$ the derivation obtained by replacing in
the derivation $\delta_{1}$ all the predecessors of the cut-formula $A\supset
B$ (including the cut-formula itself) with $\land\Sigma$. This derivation is
sound as the potentially problematic calculus rules are $\supset_{R}$ and
$\prec_{L}$ and: a $\supset_{R}$ application could not have occurred along the
featured branch in $\delta_{1}$ as the traced cut-formula would have blocked
it, and placing $\land\Sigma$ in the succedent will not disturb any
applications of $\prec_{L}$.

The key issue is: what can we say about the cut on $\land\Sigma$? It is not
immediate that every formula in $\Sigma$ is a subformula of the endsequent as
non-subformulas might trace from cuts below the originally chosen cut, or be
an $A\supset B$ that traces from an analytic cut (this is a cut where the cut-
formula is a subformula of its conclusion c.f. Def. 2) on $A\supset B$ within
$\delta_{1}$. The latter is a subtle point that arises because we are working
in the setting where analytic cuts are not eliminable. And even if they are
subformulas, we cannot expect $\land\Sigma$ to be a subformula of the
endsequent. The solution to these issues will—in the general case—require
selecting an uppermost non-analytic cut and the introduction of many cuts on
the formulas in $\Sigma$ (in fact, exponentially many in $|\Sigma|$), rather
than on $\land\Sigma$.

In summary, our strategy to adapt cut-elimination to cut-restriction is to
retain the principal reductions, replace permutation reductions by tracing the
predecessors of the cut-formulas, using only those enriched branches that are
well-defined, and applying cut to remove formulas that cannot propagate down.

##  3 The case of bi-intuitionistic logic

Initial rule and cut: $p\Rightarrow p\hskip
56.9055pt\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow
A,\Delta\Gamma,A\Rightarrow\Delta$ Structural rules:
$\Gamma,\Sigma\Rightarrow\Delta,\Pi\Gamma\Rightarrow\Delta\hskip
56.9055pt\Gamma,\Sigma\Rightarrow\Delta,\Pi\Gamma,\Sigma,\Sigma\Rightarrow\Delta,\Delta,\Pi$
Logical rules: $\Rightarrow\top\hskip 56.9055pt\bot\Rightarrow$ $\Gamma,A\land
B\Rightarrow\Delta\Gamma,A,B\Rightarrow\Delta\hskip 56.9055pt\Gamma\Rightarrow
A\land B,\Delta\lx@proof@logical@and\Gamma\Rightarrow
A,\Delta\Gamma\Rightarrow B,\Delta$ $\Gamma,A\lor
B\Rightarrow\Delta\lx@proof@logical@and\Gamma,A\Rightarrow\Delta\Gamma,B\Rightarrow\Delta\hskip
56.9055pt\Gamma\Rightarrow A\lor B,\Delta\Gamma\Rightarrow A,B,\Delta$
$\Gamma,A\supset B\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow
A,\Delta\Gamma,B\Rightarrow\Delta\hskip 56.9055pt\Gamma\Rightarrow A\supset
B\Gamma,A\Rightarrow B$ $A\prec B\Rightarrow\Delta A\Rightarrow B,\Delta\hskip
56.9055pt\Gamma\Rightarrow A\prec
B,\Delta\lx@proof@logical@and\Gamma\Rightarrow
A,\Delta\Gamma,B\Rightarrow\Delta$

Figure 1: The sequent calculus $\mathbf{BiInt}$.

We present our method using the sequent calculus $\mathbf{BiInt}$ for bi-
intuitionistic logic as a case study (Fig. 1). Bi-intuitionistic logic—also
known as Heyting–Brouwer logic or subtractive logic—is the conservative
extension of intuitionistic logic with a $\prec$ connective that is dual to
implication (coimplication). Proposed in [22] the calculus $\mathbf{BiInt}$
extends Maehara’s multiple-conclusion calculus for intuitionistic logic (built
from sequents of the form $\Gamma\Rightarrow\Delta$ where $\Gamma,\Delta$ are
multisets) with left and right rules for $\prec$. A counterexample to the
admissibility of cut stated in [22] (and in [7]) was identified by Uustalu and
Pinto [19]. Failure of cut-elimination prompted a search for analytic calculi
for bi-intuitionistic logic using formalisms extending the meta-language of
the sequent calculus [4], including nested [12], and labelled sequents [19].
Relationships between the calculi were studied in [20] where the problem of
finding a syntactic proof of the completeness of $\mathbf{BiInt}$ with
analytic cuts was left open (see [2, 14] for semantic proofs).

The notion of a _subformula_ is defined as usual. $A$ is a _proper subformula_
of $B$ if it is a subformula and $A\neq B$. For a set or sequent $X$, we say
that $A$ is a subformula of $X$ if $A$ is a subformula of one of the formulas
appearing in $X$.

The rules of the $\mathbf{BiInt}$ calculus in Fig. 1 are actually rule
schemata. With an abuse of notation we use $\Gamma,\Delta,\dots$ both for
formula multisets and for formula multiset variables. The formulas
instantiating $\Gamma$ and $\Delta$ in the rules are called _context_. We have
chosen an _additive_ formulation of all rules including cut. This means that
contexts are always copied to both premises instead of being distributed among
the premises. This is a design choice: in the presence of contraction and
weakening, we can freely move between the additive and multiplicative
formulations. Already in Section 2 we have adopted the convention of writing
$cut^{*}$ to abbreviate inferences of $w$ followed by $cut$, e.g.

$\Gamma,\Delta\Rightarrow A,\Sigma,\Pi$
$\Gamma,\Delta^{\prime},A\Rightarrow\Sigma,\Pi^{\prime}$ $cut^{*}$
$\Gamma,\Delta,\Delta^{\prime}\Rightarrow\Sigma,\Pi,\Pi^{\prime}$

The exposed formula in the conclusion of a logical rule is called the
_principal formula_ of that rule. An _initial sequent_ of $\mathbf{BiInt}$ is
the conclusion of a rule without premise, i.e. $p\Rightarrow p$,
$\Rightarrow\top$ or $\bot\Rightarrow$. These are standard definitions. The
_logical constants_ $\top$ and $\bot$ are not counted as atomic propositions,
so in particular $\top\Rightarrow\top$ and $\bot\Rightarrow\bot$ do not
constitute initial sequents.

###### Remark 1

Similar to classical logic, the connectives and rules of $\mathbf{BiInt}$ come
in dual pairs: $(\top,\bot),(\land,\lor)$, and $(\supset,\prec)$. Using a
formula translation $(\cdot)^{\sharp}$ that replaces each connective by its
dual and inverts the left/right hand side in implications, i.e. $(A\supset
B)^{\sharp}=(B^{\sharp}\prec A^{\sharp})$, $(A\prec
B)^{\sharp}=(B^{\sharp}\supset A^{\sharp})$ yields that
$\Gamma\Rightarrow\Delta$ is provable in $\mathbf{BiInt}$ iff
$\Delta^{\sharp}\Rightarrow\Gamma^{\sharp}$ is. Due to this symmetry, when
proving properties of $\mathbf{BiInt}$ it often suffices to consider just one
half of the set of connectives, as the remaining cases are in a precise sense
“the same”—namely, up to $(\cdot)^{\sharp}$.

###### Definition 1

A _$\mathbf{BiInt}$ -proof_ of a sequent $\Gamma\Rightarrow\Delta$ is a tree
of sequents rooted in $\Gamma\Rightarrow\Delta$ (the _endsequent_) that is
composed of rule instances of $\mathbf{BiInt}$, and such that all leaves are
initial sequents of $\mathbf{BiInt}$.

Note that in $init$ we require $p$ to be an atomic formula. By an easy
induction on the formula $A$ we can prove completeness of atomic axioms (axiom
expansion).

###### Lemma 1

The sequent $A\Rightarrow A$ is derivable in $\mathbf{BiInt}$ without cuts.

The following definition of “analytic cut” goes back to [23].

###### Definition 2

An instance of the cut rule

$\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow
A,\Delta\Gamma,A\Rightarrow\Delta$

is _analytic_ if $A$ is a subformula of $\Gamma\cup\Delta$. A proof is
_locally analytic_ if every cut in the proof is analytic. A sequent calculus
has the _analytic cut property_ if every provable sequent has a locally
analytic proof.

Any calculus whose other rules are analytic222In the sense that every formula
in a premise is a subformula of the endsequent. has the following property:
every formula occurring in a locally analytic proof is a subformula of the
endsequent. In other words, the analytic cut property implies the _subformula
property_. This holds, in particular, for $\mathbf{BiInt}$. The nontrivial
converse direction was shown in [14, Lem. 4.6] using an elegant induction
argument.

###  3.1 Proof of Cut-Restriction

The analytic cut property for $\mathbf{BiInt}$ is an immediate corollary of
the following main theorem which formalises the cut-restriction proof
described in Section 2.

###### Theorem 3.1

Every proof in $\mathbf{BiInt}$ that is locally analytic aside from a single
non-analytic $cut$ as its lowest inference can be transformed into a locally
analytic proof of the same endsequent.

###### Proof

Let $\delta$ be a proof ending in a non-analytic cut

$\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow
C,\Delta\Gamma,C\Rightarrow\Delta$

and assume that the subproofs $\delta_{1},\delta_{2}$ are locally analytic.
The statement is proved by induction on the size of the cut-formula.

We distinguish cases according to the shape of $C$.

$\blacktriangleright$ $C$ is an atomic formula $p$. Since $\mathbf{BiInt}$ is
consistent, $\Gamma\cup\Delta\not=\emptyset$. Replace every occurrence of $p$
in $\delta$ by some atomic formula or constant occuring as a subformula in
$\Gamma\cup\Delta$. In doing so the lowermost cut becomes analytic, and all
cuts in $\delta_{1},\delta_{2}$ remain analytic. The endsequent is unchanged
because by assumption the cut on $p$ was non-analytic. If we replaced $p$ by a
constant $x\in\\{\top,\bot\\}$ and in doing so created a non-initial sequent
$x\Rightarrow x$ from $p\Rightarrow p$, use $\top_{R}/\bot_{L}$ and weakening
to obtain an initial sequent.

_Predecessors._ If the cut formula $C$ is not atomic, we will _trace_
occurrences of $C$ upwards in the proofs $\delta_{1}$ and $\delta_{2}$.
Formally, define the predecessor relation333This is also called the parametric
ancestor relation. matching context occurences of $C$ in the conclusion of an
inference to the corresponding occurrence(s) in the premise(s). Stop when the
occurrence $C$ is principal in the conclusion of logical inference (a
_critical inference of $\delta$_), or if $C$ is removed by a weakening rule.
We will not encounter an initial sequent $C\Rightarrow C$ because we have
assumed that $C$ is not atomic. Note that we consider the occurrence of the
cut-formula in the premise of the cut as the first predecessor.

There may be multiple predecessors in a sequent since a predecessor in the
conclusion of a contraction rule can become two predecessors in its premise.
Clearly all predecessors in $\delta_{1}$ occur in the succedent while all
predecessors in $\delta_{2}$ occur in the antecedent.

Without loss of generality we will assume the following property:

irredundance:

No sequent in $\delta$ that contains a predecessor of $C$ appears as the
conclusion of a cut with cut-formula $C$.

This is justified because any such cut can be replaced by a contraction, e.g.,

$\Sigma,C\Rightarrow\Pi\lx@proof@logical@and\Sigma,C\Rightarrow
C,\Pi\Sigma,C,C\Rightarrow\Pi\hskip 21.33955pt\text{to}\hskip
21.33955pt\Sigma,C\Rightarrow\Pi\Sigma,C,C\Rightarrow\Pi$

Moreover for $\delta_{*}\in\\{\delta_{1},\delta_{2}\\}$ we denote by
$\delta_{*}[\Sigma]$ the tree (which is not necessarily a proof) resulting
from substituting all predecessors of $C$ in $\delta_{*}$ by the multiset of
formulas $\Sigma$. The following properties hold:

pre-soundness:

Every inference in $\delta_{*}$ _with the possible exception of the critical
ones_ remains a sound inference of the same rule in $\delta_{*}[\Sigma]$.

reductivity:

If an analytic cut in $\delta_{*}$ becomes non-analytic in
$\delta_{*}[\Sigma]$, then that cut is on a _proper_ subformula of $C$.

In every sequent that is not the conclusion of a critical inference, the
predecessor instantiates the context of the inference. By inspection of the
rules, replacing a formula occurring in the context of an inference rule with
any multiset preserves the soundness of that inference hence pre-soundness.

If an analytic cut becomes non-analytic then the cut-formula must be a
subformula of $C$. It cannot be $C$ itself because of the irredundance
property so it must be a proper subformula and hence reductivity holds.

With these preparations, we now resume the case distinction.

$\blacktriangleright$ $C$ is $\top$. Observe that there are no critical
inferences in $\delta_{2}$ as we do not have a rule for $\top$ in the
antecedent, hence $\top$ has been introduced by weakening. By pre-soundness
$\delta_{2}[\emptyset]$ is a $\mathbf{BiInt}$-proof of
$\Gamma\Rightarrow\Delta$. Since $\top$ has no proper subformulas, reductivity
implies that $\delta_{2}[\emptyset]$ is locally analytic.

$\blacktriangleright$ $C$ is $\bot$. Similar to the previous case (by
symmetry).

$\blacktriangleright$ $C$ is $A\land B$. Here we can use a standard
invertibility-style argument. Consider the trees $\delta_{1}[A],\delta_{1}[B]$
and $\delta_{2}[A,B]$ with their respective roots $\Gamma\Rightarrow A,\Delta$
and $\Gamma\Rightarrow B,\Delta$ and $\Gamma,A,B\Rightarrow\Delta$. With some
minor modifications we can make all the trees into $\mathbf{BiInt}$ proofs (by
pre-soundness it suffices to check critical inferences). For example, let

$\Sigma\Rightarrow A\land B,(A\land
B)^{*},\Pi\lx@proof@logical@and\Sigma\Rightarrow A,(A\land
B)^{*},\Pi\Sigma\Rightarrow B,(A\land B)^{*},\Pi$

be a critical inference in $\delta_{1}$. Here $(A\wedge B)^{*}$ indicates some
number of predecessors (possibly none) that are not the principal formula, and
$\Sigma,\Pi$ contains no predecessors. Then in $\delta_{1}[A]$ we have the
unsound inference

$\Sigma\Rightarrow A,A^{*},\Pi\lx@proof@logical@and\Sigma\Rightarrow
A,A^{*},\Pi\Sigma\Rightarrow B,A^{*},\Pi$

Nevertheless the above can simply be replaced using the left premise
$\Sigma\Rightarrow A,A^{*},\Pi$. Similar reasoning applies to $\delta_{1}[B]$
and $\delta_{2}[A,B]$. By an abuse of notation, let
$\delta_{1}[A],\delta_{1}[B]$ and $\delta_{2}[A,B]$ indicate below the
$\mathbf{BiInt}$-proofs where these modifications have been carried out. We
then obtain the following cut-restriction:

$\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow
A,\Delta\Gamma,A\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow
B,\Delta\Gamma,A,B\Rightarrow\Delta$

By reductivity, all non-analytic cuts in this proof are on proper subformulas
of $A\land B$, and hence eliminable by induction hypothesis.

$\blacktriangleright$ $C$ is $A\lor B$.
Similar to the previous case (by symmetry).

$\blacktriangleright$ $C$ is $A\supset B$.

This case is the crucial part of the proof. Define the critical antecedent and
critical succedent of a critical inference as the set of formulas in its
antecedent and succedent of the conclusion, respectively, omitting
predecessors (if any). E.g. suppose that the following is a critical inference
in $\delta_{2}$ containing exactly two predecessors in its conclusion.

$A\supset B,\Sigma\Rightarrow\Pi,A$ $A\supset B,B,\Sigma\Rightarrow\Pi,A$
$\supset_{L}$ $A\supset B,A\supset B,\Sigma\Rightarrow\Pi$

Then its critical antecedent is $\Sigma$ and its critical succedent is $\Pi$.
We remark that due to the shape of $\supset_{R}$, each critical inference in
$\delta_{1}$ contains exactly one predecessor—the principal formula of
$\supset_{R}$—and the critical succedent is empty:

$A,\Sigma\Rightarrow B$ $\supset_{R}$ $\Sigma\Rightarrow A\supset B$

Thus no two critical inferences in $\delta_{1}$ appear on the same branch.

We show the following important property:

tameness:

Every formula in the critical antecedent $\Sigma$ of a critical inference in
$\delta_{1}$ is a subformula of $\Gamma\cup\Delta$ or a proper subformula of
$A\supset B$.

Since $\delta_{1}$ is locally analytic by assumption, we know that every
formula in it is a subformula of $\Gamma\cup\Delta\cup\\{A\supset B\\}$. So
the only case we have to exclude for tameness is that the critical antecedent
contains $A\supset B$. Indeed: Assume towards a contradiction that $D=A\supset
B\in\Sigma$, and follow the occurences of $D$ downwards in $\delta_{1}$. Being
in the antecedent, $D$ cannot become the $A\supset B$ in the succedent of the
endsequent; but also $D$ cannot appear as a subformula of $\Gamma\cup\Delta$
as this would violate the non-analyticity of the lowermost cut. It follows
that $D$ must be removed by a cut in $\delta_{1}$. By irredundance, this cut
cannot be on $D=A\supset B$ itself, so it must be on a formula
$D^{\prime}_{A\supset B}$ containing $A\supset B$ as a proper subformula.
Again by local analyticity of $\delta_{1}$, $D^{\prime}_{A\supset B}$ must be
a subformula of $\Gamma\cup\Delta\cup\\{A\supset B\\}$. Then
$D^{\prime}_{A\supset B}$ must be a subformula of $\Gamma\cup\Delta$ and hence
so too is $A\supset B$, contradicting the non-analyticity of the cut in
$\delta$.

Now, let $\Sigma_{1},\ldots,\Sigma_{n}$ be all the critical antecedents in
$\delta_{1}$ (i.e. the antecedents of all the critical inferences in
$\delta_{1}$).

Step 1. For $r\leq n$ fix the $r$-th critical inference in $\delta_{1}$ with
subderivation $\delta_{1}^{r}$

$\vdots\,\delta_{1}^{r}$ $\Sigma_{r},A\Rightarrow B$ $\supset_{R}$
$\Sigma_{r}\Rightarrow A\supset B$

and turn to $\delta_{2}$. Every critical inference in $\delta_{2}$ has the
following form where $A\supset B^{*}$ indicates other predecessors (possibly
none) and $\Sigma$ contains no predecessors.

$\Sigma,A\supset B^{*}\Rightarrow A,\Pi$ $\Sigma,A\supset
B^{*},B\Rightarrow\Pi$ $\supset_{L}$ $\Sigma,A\supset B^{*},A\supset
B\Rightarrow\Pi$

Obtain the tree $\delta_{2}[\Sigma_{r}]$ with root
$\Gamma,\Sigma_{r}\Rightarrow\Delta$ by replacing all critical formulas in
$\delta_{2}$ with the critical antecedent $\Sigma_{r}$. We need to modify
$\delta_{2}[\Sigma_{r}]$ into a $\mathbf{BiInt}$-proof. By pre-soundness it
suffices to inspect critical inferences in $\delta_{2}$. In
$\delta_{2}[\Sigma_{r}]$ each such inference becomes the unsound

$\Sigma,\Sigma_{r}^{*}\Rightarrow A,\Pi$
$\Sigma,\Sigma_{r}^{*},B\Rightarrow\Pi$ $unsound$
$\Sigma,\Sigma_{r}^{*},\Sigma_{r}\Rightarrow\Pi$

Using the subderivation $\delta_{1}^{r}$ of $\delta_{1}$ and cuts on $A$ and
$B$ we replace this unsound inference in $\delta_{2}[\Sigma_{r}]$ by

$\Sigma,\Sigma_{r}^{*}\Rightarrow A,\Pi$ $\vdots\,\delta_{1}^{r}$
$A,\Sigma_{r}\Rightarrow B$ $cut^{*}$
$\Sigma,\Sigma_{r}^{*},\Sigma_{r},\Rightarrow B,\Pi$
$\Sigma,\Sigma_{r}^{*},B\Rightarrow\Pi$ $cut^{*}$
$\Sigma,\Sigma_{r}^{*},\Sigma_{r}\Rightarrow\Pi$ (5)

In this way we obtain a $\mathbf{BiInt}$-proof of
$\Gamma,\Sigma_{r}\Rightarrow\Delta$. By construction and reductivity all non-
analytic cuts in this proof are on proper subformulas of $A\supset B$. So by
the induction hypothesis, we obtain a locally analytic proof of

$\Gamma,\Sigma_{r}\Rightarrow\Delta$ (6)

In particular, if $\Sigma_{r}=\emptyset$ we are already done. For the
remainder of the proof let us therefore assume that all critical antecedents
$\Sigma_{1},\ldots,\Sigma_{n}$ are nonempty.

Step 2. Let $(D_{1},\ldots,D_{n})\in\Sigma_{1}\times\ldots\times\Sigma_{n}$
and consider the tree $\delta_{1}[D_{1},\ldots,D_{n}]$ with root
$\Gamma\Rightarrow D_{1},\ldots,D_{n},\Delta$. Again using pre-soundness we
make $\delta_{1}[D_{1},\ldots,D_{n}]$ into a $\mathbf{BiInt}$ proof by
replacing any critical inference turned unsound

$\Sigma_{r}\Rightarrow D_{1},\ldots,D_{n}\Sigma_{r},A\Rightarrow B$

with a cut-free proof of $\Sigma_{r}\Rightarrow D_{1},\ldots,D_{n}$, which
exists (by Lemma 1) since $D_{r}\in\Sigma_{r}$. Again all non-analytic cuts in
the resulting $\mathbf{BiInt}$-proof are on proper subformulas of $A\supset B$
by reductivity, and so we can use the induction hypothesis to obtain a locally
analytic proof of

$\Gamma\Rightarrow D_{1},\ldots,D_{n},\Delta$ (7)

Step 3. We now combine all instances of (6) and (7) using cuts on formulas in
$\bigcup_{i=1}^{n}\Sigma_{i}$ to obtain a locally analytic proof of
$\Gamma\Rightarrow\Delta$.

Enumerate the elements of $\Sigma_{r}$ as
$D_{r}^{1},D_{r}^{2},\ldots,D_{r}^{m_{r}}$. For every
$(D_{2},\ldots,D_{n})\in\Sigma_{2}\times\ldots\times\Sigma_{n}$, obtain a
derivation of

$\Gamma\Rightarrow D_{2},\ldots,D_{n},\Delta$ (8)

as follows by cuts on the elements of $\Sigma_{1}$. In the following, the cut-
formula has been boxed to make it easier to identify.

(7) $\Gamma\Rightarrow\text{\framebox{$D_{1}^{m_{1}}$}}D_{2}\ldots
D_{n},\Delta$ (7) $\Gamma\Rightarrow\text{\framebox{$D_{1}^{2}$}}D_{2}\ldots
D_{n},\Delta$ (7)
$\Gamma\Rightarrow\text{\framebox{$D_{1}^{1}$}}D_{2}..D_{n},\Delta$ (6)
$\text{\framebox{$D_{1}^{1}$}}D_{1}^{2}..D_{1}^{m_{1}},\Gamma\Rightarrow\Delta$
$cut^{*}$ $\text{\framebox{$D_{1}^{2}$}},D_{1}^{3}\ldots
D_{1}^{m_{1}},\Gamma\Rightarrow D_{2}\ldots D_{n},\Delta$ $cut^{*}$
$D_{1}^{3}\ldots D_{1}^{m_{1}},\Gamma\Rightarrow D_{2}\ldots D_{n},\Delta$
$\vdots$ $\text{\framebox{$D_{1}^{m_{1}}$}},\Gamma\Rightarrow D_{2}\ldots
D_{n},\Delta$ $cut$ $\Gamma\Rightarrow D_{2}\ldots D_{n},\Delta$

Next, for every
$(D_{3},\ldots,D_{n})\in\Sigma_{3}\times\ldots\times\Sigma_{n}$, proceed as
follows by cuts on the elements of $\Sigma_{2}$:

(8) $\Gamma\Rightarrow\text{\framebox{$D_{2}^{m_{2}}$}},D_{3}\ldots
D_{n},\Delta$ (8) $\Gamma\Rightarrow\text{\framebox{$D_{2}^{2}$}}D_{3}\ldots
D_{n},\Delta$ (8)
$\Gamma\Rightarrow\text{\framebox{$D_{2}^{1}$}}D_{3}..D_{n},\Delta$ (6)
$\text{\framebox{$D_{2}^{1}$}}D_{2}^{2}..D_{2}^{m_{2}},\Gamma\Rightarrow\Delta$
$cut^{*}$ $\text{\framebox{$D_{2}^{2}$}},D_{2}^{3}\ldots
D_{2}^{m_{2}},\Gamma\Rightarrow D_{3},\ldots,D_{n},\Delta$ $cut^{*}$
$D_{2}^{3}\ldots D_{2}^{m_{2}},\Gamma\Rightarrow D_{3}\ldots D_{n},\Delta$
$\vdots$ $\text{\framebox{$D_{2}^{m_{2}}$}},\Gamma\Rightarrow D_{3}\ldots
D_{n},\Delta$ $cut$ $\Gamma\Rightarrow D_{3},\ldots,D_{n},\Delta$

In this way we ultimately get $\Gamma\Rightarrow\Delta$. Every introduced cut
is on a formula from a critical antecedent $\Sigma_{r}$ in $\delta_{1}$ so by
tameness the cut is analytic or eliminable by induction hypothesis. Hence
there is a locally analytic proof of $\Gamma\Rightarrow\Delta$.

$\blacktriangleright$ $C$ is $A\prec B$. Similar to the previous case (by
symmetry).

This concludes the case distinction and thus the proof of the theorem. ∎

###### Theorem 3.2

$\mathbf{BiInt}$ has the analytic cut property.

###### Proof

Starting with the uppermost one, all non-analytic cuts in a
$\mathbf{BiInt}$-proof can be eliminated by repeatedly applying Theorem 3.1.∎

After an uppermost non-analytic cut in a proof is replaced with analytic cuts
by the method of Theorem 3.1, it is in general _not_ true that their cut-
formulas are subformulas of the endsequent. After all, there might be non-
analytic cuts further down in the proof. In the course of restricting those
lower non-analytic cuts, higher cuts will be revisited and modified again. It
is only once the last non-analytic cut has been restricted that all cuts
become “globally analytic” i.e. cut-formulas that are subformulas of the
endsequent.

##  4 The Core Ideas

The above proof of the analytic cut property for $\mathbf{BiInt}$ is not
tailored to this specific calculus. Here we identify the key properties that
allow the proof to go through, and apply them to the case of the modal logic
$\mathbf{S5}$. The first three properties are well-known to any proof
theorist.

  1. 1.

principal reductions: replace a cut that is principal in left and right
premise by cuts on smaller formulas (see Sect. 2).

  2. 2.

invertibility of certain left and right rules: given a proof of the conclusion
of a logical rule there are proofs of its premises with no new cuts.

  3. 3.

axiom expansion: completeness of atomic axioms.

If the above properties hold for all connectives then cut-elimination is
close: given a cut on a formula $C$ whose left and right rules are both
invertible, replace the cut-formula in each premise with its immediate
subformulas using invertibility and then apply the principal cut reduction.

All rules for connectives in $\mathbf{BiInt}$ admit principal reductions,
_including_ $\supset$ and $\prec$; e.g.,

$\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow A\prec
B,\Delta\lx@proof@logical@and\Gamma,B\Rightarrow\Delta\Gamma\Rightarrow
A,\Delta A\prec B\Rightarrow\Delta A\Rightarrow B,\Delta$

can be replaced by

$\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow
A,\Delta\Gamma,A\Rightarrow\Delta\lx@proof@logical@and A\Rightarrow
B,\Delta\Gamma,B\Rightarrow\Delta$

Moreover in the proof for $\mathbf{BiInt}$ we (implicitly) used the
invertibility of $\land_{L}$, $\land_{R}$ and $\lor_{L}$, $\lor_{R}$. We also
used that $\top$ ($\bot$) can be removed from an antecedent (resp. succedent).
Finally, axiom expansion holds for $\mathbf{BiInt}$ (Lemma 1). However, the
right rule of $\supset$ and the left rule of $\prec$ are not invertible. What
comes to the rescue are the following properties, here formulated for an
arbitrary connective $\circ$:

  1. 4.

right-compatible: Let $X$ and $Y$ be multisets of formulas that are permitted
in the antecedent context and succedent context of the right rule for $\circ$
respectively. For every rule instance $r$ of the calculus (excluding initial
sequents) with non-empty antecedent resp. succedent context: appending $(X,Y)$
to the (antecedent,succedent) resp. (succedent,antecedent) everywhere yields a
valid rule instance.

  2. 5.

left-compatible: Replace “right rule” in the above with “left rule”.

These properties relate the context restrictions of the introduction rule of a
connective with the context restrictions of every other rule. In particular,
the motivation for ‘switching the contexts’ from (antecedent,succedent) to
(succedent,antecedent) is that the antecedent $\Sigma$ of the conclusion
$\Sigma\Rightarrow A\supset B$ of a critical inference must play a dual role,
appending antecedent and appending succedent of other rule instances. It is
this that enables a picture as (4).

###### Example 1

$\supset$ is right-compatible. The antecedent context of the rule
$\supset_{R}$ can be instantiated by any multiset $X$. The succedent context
can only be instantiated by the empty multiset. We must ensure that appending
$(X,\emptyset)$ to every rule instance with non-empty antecedent context
yields a rule instance (no need to check any $\prec_{L}$ rule instance as it
never has a non-empty antecedent context); also appending $(\emptyset,X)$ to
every rule instance that has a non-empty succedent context (ruling out a rule
instance of $\supset_{R}$) yields a rule instance.

Similarly $\prec$ is left-compatible.

Another example ($\Box$ in $\mathbf{S5}$ is right-compatible) appears in
Section 4.1.

If a connective $\circ$ has a principal cut reduction, axiom expansion and a
compatibility property, then a non-analytic cut on $C$ with main connective
$\circ$ might be simplified along the following lines: trace $C$ upwards on
each premise until principal, perform a principal reduction _across different
branches_ (cf. (5) in main proof), then propagate the appended context
downwards to the endsequent (relying on compatibility). Cut (cf. Step 3 in
main proof) each appended formula using a proof obtained (relying on
compatibility) by the context appended to the ‘other side’ i.e. antecedent
appended to succedent.

To summarise, the argument works for $\mathbf{BiInt}$ because (a) all
connectives of $\mathbf{BiInt}$ admits principal reductions, (b) every
connective of $\mathbf{BiInt}$ is either invertible
$\\{\top,\bot,\land,\lor\\}$ or has some compatibility property
$\\{\supset,\prec\\}$, and (c) axiom expansion holds.

###  4.1 An application: the case of $\mathbf{S5}$

A sequent calculus $\mathbf{S5}$ [17] for the modal logic $S5$ extends
Gentzen’s calculus $\mathbf{LK}$ for classical propositional logic with the
following two rules for the modality $\Box$:

$\Gamma,\Box
A\Rightarrow\Delta\Gamma,A,\Rightarrow\Delta\qquad\qquad\qquad\Box\Gamma\Rightarrow\Box
A,\Box\Theta\Box\Gamma\Rightarrow A,\Box\Theta$ (9)

As is well know, cut elimination fails but as shown by Takano [24] the
calculus has the analytic cut property. Cut-restriction provides a proof too.

First notice that $\mathbf{S5}$ admit principal cut reductions for all
connectives, and axiom expansion. Also, the left and right rules of $\land$
and $\lor$ are invertible. As the implication $A\supset B$ is classical, it
can be considered as a derived connective and therefore removed from the
signature. The role of the problematic connectives for cut-elimination
($\supset$ and $\prec$ in $\mathbf{BiInt}$) is taken here by the modality
$\Box$.

A boxed formula is principal in the antecedent by $T$ (“left rule”) and in the
succedent by $5$ (“right rule”). In the latter, the context consists of boxed
formulas only, namely $\Box\Gamma$ in the antecedent and $\Box\Theta$ in the
succedent. For every non-initial rule instance in $\mathbf{S5}$, appending
arbitrary multisets of boxed formulas to the antecedent and succedent yields a
new rule instance. It follows that $\Box$ is right-compatible. Once this is
noted, essentially the same proof as for Theorem 3.1 also works for
$\mathbf{S5}$. For illustration, we picture a simple case below.

$\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow\Box A,\Delta\Box D\Rightarrow\Box A\Box D\Rightarrow A\Gamma,\Box A\Rightarrow\Delta\Sigma,\Box A\Rightarrow\Pi\Sigma,A\Rightarrow\Pi$ to |  $\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow\Box D,\Delta\Box D\Rightarrow\Box D\Gamma,\Box D\Rightarrow\Delta\Sigma,\Box D\Rightarrow\Pi\lx@proof@logical@and\Box D\Rightarrow A\Sigma,A\Rightarrow\Pi$
---|---

Concluding Remark: We have investigated the first level of cut-restriction,
adapting cut-elimination to obtain analytic cuts (when elimination is not
possible). Our proof makes use of the structural rules of weakening and
contraction. This leaves open the question of adapting it to substructural
logics.

What is the next level of cut-restriction to investigate? Sequent calculi
requiring mild violations of analytic cut, as in the case, e.g., of the
calculi for the modal logics $K5$, $K5D$, and $S4.2$ [25, 26]. Here are some
intuitions for $K5$. Takano [25] observed that analytic cuts do not suffice
but cuts on $K5$-subformulas do. These are subformulas of the endsequent, or
$\Box\lnot\Box B$ or $\lnot\Box B$ where $\Box B$ is a subformula of some
boxed formula that is a subformula of the endsequent.

The sequent calculus for $K5$ extends $\mathbf{LK}$ with the following variant
of $5$:

$\Gamma\Rightarrow\Box\Theta,A$ $5^{*}$ $\Box\Gamma\Rightarrow\Box\Theta,\Box
A$

Here is the main case (to simplify, assume one critical inference in each
premise).

$\Gamma^{\prime}\Rightarrow\Box\Theta^{\prime},A$ $5^{*}$
$\Box\Gamma^{\prime}\Rightarrow\Box\Theta^{\prime},\Box A$ $\delta_{1}$
$\Gamma\Rightarrow\Theta,\Box A$ $A\Rightarrow\Box Y^{\prime},B$ $5^{*}$ $\Box
A\Rightarrow\Box Y^{\prime},\Box B$ $\delta_{2}$ no $5^{*}$ rule on featured
branch $\Box A,X\Rightarrow Y$ $cut^{*}$ $\Gamma,X\Rightarrow\Theta,Y$

The rule $5^{*}$ is not invertible, nor is it left/right-compatible: adding
the same formula to the premise and conclusion antecedent breaks the rule
instance (as the rule appends a box when passing from premise to conclusion
antecedent). This suggests applying cuts on formulas that, in $\mathbf{S5}$,
we propagated downwards. For simplicity, in the following, read each multiset
as a single formula:

$\Box\Theta^{\prime}\Rightarrow\Box\Theta^{\prime}$ $\lnot_{R}$
$\Rightarrow\Box\Theta^{\prime},\lnot\Box\Theta^{\prime}$ $5^{*}$
$\Rightarrow\Box\Theta^{\prime},\Box\lnot\Box\Theta^{\prime}$ $w$
$\Box\Gamma^{\prime}\Rightarrow\Box\Theta^{\prime},\Box\lnot\Box\Theta^{\prime}$
$\delta_{1}+$
$\Gamma\Rightarrow\Theta,\text{\framebox{$\Box\lnot\Box\Theta^{\prime}$}}$
$\Box\Gamma^{\prime}\Rightarrow\Box\Gamma^{\prime}$ $w$
$\Box\Gamma^{\prime}\Rightarrow\Box\Theta^{\prime},\Box\Gamma^{\prime}$
$\delta_{1}+$
$\Gamma\Rightarrow\Theta,\text{\framebox{$\Box\Gamma^{\prime}$}}$
$\Gamma^{\prime}\Rightarrow\Box\Theta^{\prime},A$ $A\Rightarrow\Box
Y^{\prime},B$ $cut^{*}$ $\Gamma^{\prime}\Rightarrow\Box\Theta^{\prime},\Box
Y^{\prime},B$ $\lnot_{L}$
$\Gamma^{\prime}\lnot\Box\Theta^{\prime}\Rightarrow\Box Y^{\prime},B$ $5^{*}$
$\text{\framebox{$\Box\Gamma^{\prime}$}},\Box\lnot\Box\Theta^{\prime}\Rightarrow\Box
Y^{\prime},\Box B$ $cut^{*}$
$\Gamma,\text{\framebox{$\Box\lnot\Box\Theta^{\prime}$}}\Rightarrow\Theta,\Box
Y^{\prime},\Box B$ $cut^{*}$ $\Gamma\Rightarrow\Theta,\Box Y^{\prime},\Box B$
$+\delta_{2}+$ $\Gamma,X\Rightarrow\Theta,Y$

The cut on $\Box\Gamma^{\prime}$ is like those we encountered before i.e. on a
formula occurring in the original proof. There is also a cut on
$\Box\lnot\Box\Theta^{\prime}$ while it was $\Box\Theta^{\prime}$ that
occurred in the original proof but this is not unexpected (given Takano’s
result).

A significant issue remains: showing that $\Box\Theta^{\prime}$ is a
subformula of the endsequent (how to rule out a $K5$-subformula that is not a
subformula?). A suitable irredundance property (and generalised tameness
property) seems required.

## References

  * [1] A. Avron.  A constructive analysis of RM.  J. of Symbolic Logic, 52(4):939–951, 1987.
  * [2] A. Avron and O. Lahav.  A unified semantic framework for fully structural propositional sequent systems.  ACM Trans. Comput. Logic, 14(4), 2013.
  * [3] N. Bezhanishvili and S. Ghilardi.  The bounded proof property via step algebras and step frames.  Annals of Pure and Applied Logic, 165(12):1832 – 1863, 2014.
  * [4] L. Buisman and R. Goré.  A cut-free sequent calculus for bi-intuitionistic logic.  In N. Olivetti, editor, TABLEAUX 2007, volume 4548 of Lecture Notes in Computer Science, pages 90–106. Springer, 2007.
  * [5] A. Ciabattoni, N. Galatos, and K. Terui.  From axioms to analytic rules in nonclassical logics.  In LICS 2008, pages 229–240, 2008.
  * [6] A. Ciabattoni, T. Lang, and R. Ramanayake.  Bounded-analytic sequent calculi and embeddings for hypersequent logics.  J. Symb. Log., 86(2):635–668, 2021.
  * [7] T. Crolard.  A formulae-as-types interpretation of subtractive logic.  J. Log. Comput., 14(4):529–570, 2004.
  * [8] M. D’Agostino and M. Mondadori.  The taming of the cut. classical refutations with analytic cut.  J. of Logic and Computation, 4:285–319, 1994.
  * [9] M. D’Agostino.  Are tableaux an improvement on truth-tables?  Journal of Logic Language and Information, 1:235–252, 08 1992.
  * [10] M. J. Fischer and R. E. Ladner.  Propositional dynamic logic of regular programs.  Journal of Computer and System Sciences, 18(2):194–211, 1979.
  * [11] M. Fitting.  Subformula results in some propositional modal logics.  Studia Logica, 37(4):387–391, 1978.
  * [12] R. Goré, L. Postniece, and A. Tiu.  Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.  In C. Areces and R. Goldblatt, editors, Advances in Modal Logic 7, pages 43–66. College Publications, 2008.
  * [13] A. Indrzejczak.  Two is enough–bisequent calculus for s5.  In International Symposium on Frontiers of Combining Systems, pages 277–294. Springer, 2019.
  * [14] T. Kowalski and H. Ono.  Analytic cut and interpolation for bi-intuitionistic logic.  The Review of Symbolic Logic, 10(2):259–283, 2017.
  * [15] O. Lahav.  From frame properties to hypersequent rules in modal logics.  In LICS 2013, IEEE, pages 408–417, 2013.
  * [16] G. E. Minc.  Some calculi of modal logic.  Trudy Mat. Inst. Steklov, 98:88–111, 1968.
  * [17] M. Ohnishi and K. Matsumoto.  Gentzen method in modal calculi.  Osaka Math. J., 9:113–130, 1957.
  * [18] M. Ohnishi and K. Matsumoto.  Gentzen method in modal calculi. II.  Osaka Math. J, 11:115–120, 1959.
  * [19] L. Pinto and T. Uustalu.  Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents.  In M. Giese and A. Waaler, editors, Automated Reasoning with Analytic Tableaux and Related Methods. Proceedings, volume 5607 of LNCS, pages 295–309. Springer, 2009.
  * [20] L. Pinto and T. Uustalu.  A proof-theoretic study of bi-intuitionistic propositional sequent calculus.  J. Log. Comput., 28(1):165–202, 2018.
  * [21] G. Pottinger.  Uniform, cut-free formulations of T, S4 and S5 (abstract).  J. of Symbolic Logic, 48(3):900, 1983.
  * [22] C. Rauszer.  A formalization of the propositional calculus of $H-B$ logic.  Studia Logica, 33:23–34, 1974.
  * [23] R. M. Smullyan.  Analytic cut.  J. Symbolic Logic, 33:560–564, 1968.
  * [24] M. Takano.  Subformula property as a substitute for cut-elimination in modal propositional logics.  Mathematica japonica, 37:1129–1145, 1992.
  * [25] M. Takano.  A modified subformula property for the modal logics K5 and K5D.  Bulletin of the Section of Logic, 30, 01 2001.
  * [26] M. Takano.  A modified subformula property for the modal logic S4.2.  Bulletin of the Section of Logic, 48:19–28, 2019.
  * [27] M. Takano.  New modification of the subformula property for a modal logic.  Bulletin of the Section of Logic, 49, 08 2020.
  * [28] G. Takeuti.  Proof theory, volume 81 of Studies in Logic and the Foundations of Mathematics.  North Holland, Amsterdam, 1987.
  * [29] S. Valentini.  The modal logic of provability: cut-elimination.  J. Philos. Logic, 12(4):471–476, 1983.