X_{i}\models\boldsymbol{A}\sigma_{i}\\}\in\mathfrak{U}$, where $\sigma_{i}$
replaces $\\{y^{1},\dots,y^{k}\\}$ with $\\{y^{1}_{i},\dots,y^{k}_{i}\\}$, and
hence $\\{i\mid TX_{i}\models\boldsymbol{W}\\}\in\mathfrak{U}$, contradiction
as in Lemma 37.

######  Proof 5.4 (Proof (Theorem 40)).

By Lemma 41 and finitary one-step compactness, there exists $\xi(x)$
satisfying the set $\Psi$ from Lemma 41. To show 13 for $A\subseteq X$, we
regard $A$ as the extension of a unary predicate $P$. Then
$\xi(x)\models\heartsuit A$ is equivalent to

$x\models\exists y^{1},\dots,y^{k}.\,(P(y^{1})\land\dots\land P(y^{k})\land
x\heartsuit\lceil z:z=y^{1},\dots,z=y^{k}\rceil).$

Thus it suffices to prove the Łoś equivalence for formulas $x\heartsuit\lceil
z:z=y^{1},\dots,z=y^{k}\rceil$. This, however, is exactly what satisfaction of
$\Psi$ by $\xi(x)$ guarantees.

For operators that are $\omega$-bounded but not $k$-bounded for any $k$, the
ultraproduct construction cannot be available, in consequence of Theorem 22.
However, the downward Löwenheim-Skolem theorem does survive under the weaker
assumption of $\omega$-boundedness:

######  Theorem 42 (Downward Löwenheim-Skolem Theorem).

Over $\omega$-bounded finitary one-step compact $\Lambda$-structures,
$\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$ satisfies the downward Löwenheim-
Skolem theorem; that is, every model of infinite cardinality $\kappa$ has, for
every infinite cardinal $\lambda\leq\kappa$, an elementary substructure of
cardinality $\lambda$.

Here, we use the term _elementary substructure_ in the usual way to designate
first-order substructures whose elements satisfy the same formulas as they do
in the original model; we explicitly do _not_ require that the coalgebra
structure on the substructure forms a subcoalgebra.

The proof needs the following simple lemma.

######  Lemma 43.

Let $Y$ be an infinite subset of $X$,
$\tau:\mathsf{sVar}\to\mathcal{P}_{\mathit{fin}}(Y)$ and
$\boldsymbol{A}\in\mathsf{Prop}(\mathsf{sVar})$. Then
$Y\models\boldsymbol{A}\tau$ iff $X\models\boldsymbol{A}\tau$.

######  Proof 5.5.

Only finitely many $\boldsymbol{p}\in\mathsf{sVar}$ are relevant, so we can,
for the rest of the proof, assume that $\mathsf{sVar}$ is finite. Define the
$\tau$-valuation of $x\in X$ as the valuation $\kappa:\mathsf{sVar}\to 2$
given by $\kappa(\boldsymbol{p})=\top$ iff $x\in\tau(\boldsymbol{p})$. Then
the claim of the lemma is equivalent to saying that every $\tau$-valuation
occurring in $X$ occurs also in $Y$. Now if $x\in X\setminus Y$, then the
$\tau$-valuation of $x$ is everywhere false; this valuation occurs also in
$Y$, as $\mathsf{sVar}$ and the $\tau(\boldsymbol{p})$ are finite.

######  Proof 5.6 (Proof (Theorem 42)).

Let $\mathfrak{M}=(C,\gamma,I)$ be a coalgebraic model of cardinality
$\kappa$. Pick Skolem functions for all formulas $\exists x.\,\phi$ as usual,
and for every formula $x\heartsuit\lceil y:\phi\rceil$ a finitely non-
deterministic Skolem function $f_{x\heartsuit\lceil
y:\phi\rceil}:C^{\mathsf{FV}(x\heartsuit\lceil
y:\phi\rceil)}\to\mathcal{P}_{\mathit{fin}}(C)$ with the property that for
every valuation $\eta\in C^{\mathsf{FV}(x\heartsuit\lceil y:\phi\rceil)}$,
$f_{x\heartsuit\lceil
y:\phi\rceil}(\eta)\subseteq_{\mathit{fin}}{[\\![\phi]\\!]}_{C,\eta}$ and

$C,\eta\models x\heartsuit\lceil
y:\phi\rceil\iff\gamma(\eta(x))\models\heartsuit f_{x\heartsuit\lceil
y:\phi\rceil}(\eta).$

(Such a function $f_{x\heartsuit\lceil y:\phi\rceil}$ exists because
$\heartsuit$ is $\omega$-bounded.) Pick a countably infinite subset
$Y_{0}\subseteq C$ and let $Y$ be the closure of $Y_{0}$ under the Skolem
functions, in the case of the non-deterministic Skolem functions
$f_{x\heartsuit\lceil y:\phi\rceil}$ in the sense that $f_{x\heartsuit\lceil
y:\phi\rceil}[Y]\subseteq Y$. Then $Y$ is countable: it consists of the
possible values of countably many finitely non-deterministic finite Skolem
terms.

It remains to define a coalgebra structure $\zeta$ on $c\in Y$ in such a way
that

$\zeta(c)\models\heartsuit A\iff\gamma(c)\models\heartsuit A$ (14)

for all $A\subseteq_{\mathit{fin}}Y$; that is, we have to prove that the set

$\Psi=\\{\epsilon\heartsuit A\mid\gamma(c)\models\epsilon\heartsuit A\\}$

of one-step formulas over $\mathcal{P}_{\mathit{fin}}(Y)$ is satisfiable over
$Y$ (where $\heartsuit$ ranges over $\mathrm{\Lambda}$, $A$ ranges over
$\mathcal{P}_{\mathit{fin}}(Y)$, and $\epsilon$ ranges over
$\\{\cdot,\neg\\}$). By finitary one-step compactness, it suffices to prove
that $\Psi$ is finitely satisfiable. Assume the contrary; then by Lemma 38
there exists a sound one-step rule $\boldsymbol{A}/\boldsymbol{P}$ valuation
$\tau:\mathsf{sVar}\to\mathcal{P}(Y)$ such that $Y\models\boldsymbol{A}\tau$
and $\boldsymbol{P}\tau$ propositionally contradicts some finite subset
$\Psi_{0}$ of $\Psi$. By Lemma 43, $C\models\boldsymbol{A}\tau$, and hence
$C\models\boldsymbol{P}\tau$; therefore, $\Psi_{0}$ is unsatisfiable over $C$,
in contradiction to the fact that $\gamma(c)$ satisfies $\Psi$ by
construction.

Since $\Psi$ is satisfiable, we have a coalgebra structure $\zeta$ satisfying
(14). It follows by induction over the formula structure that for every
coalgebraic first-order formula $\phi$ and every valuation $v$ in $Y$,

$\mathfrak{N},v\models\phi\quad\text{iff}\quad\mathfrak{M},v\models\phi:$

where $\mathfrak{N}=(Y,\zeta,J)$ and $J$ is the induced substructure obtained
by restricting $I$ to $Y$. The Boolean cases are trivial. The case for
existential quantification is as in the classical case. The case
$x\heartsuit\lceil y:\phi\rceil$ is as follows: $\mathfrak{N},v\models
x\heartsuit\lceil y:\phi\rceil$ iff
$\zeta(v(x))\models\heartsuit{[\\![\phi]\\!]}_{\mathfrak{N},v}=\heartsuit({[\\![\phi]\\!]}_{\mathfrak{M},v}\cap
Y)$ (where the equality holds by induction) iff (by $\omega$-boundedness)
$\zeta(v(x))\models\heartsuit A$ for some
$A\subseteq_{\mathit{fin}}{[\\![\phi]\\!]}_{\mathfrak{M},v}\cap Y$,
equivalently $\gamma(v(x))\models\heartsuit A$ by (14). The latter implies
$\mathfrak{M},v\models x\heartsuit\lceil y:\phi\rceil$ by monotonicity;
conversely, $\mathfrak{M},v\models x\heartsuit\lceil y:\phi\rceil$ implies
$\gamma(v(x))\models\heartsuit f_{x\heartsuit\lceil y:\phi\rceil}(v)$ by
construction, and $f_{x\heartsuit\lceil
y:\phi\rceil}(v)\subseteq_{\mathit{fin}}{[\\![\phi]\\!]}_{\mathfrak{M},v}\cap
Y$.

The above version of the downward Löwenheim-Skolem theorem applies to our main
bounded examples (relational, graded, and positive Presburger modalities) as
well as to probabilistic modalities over non-standard or zerodimensional
subdistributions, respectively, which are $\omega$-bounded but not $k$-bounded
for any $k$ (Examples 3.5 and 3.5). Finally, we note that the downward
Löwenheim-Skolem theorem holds also for the one-step compact case; this is in
mild generalization of a corresponding result for the neighbourhood case
proved already by Chang [Chang73].

######  Theorem 44.

Over one-step compact $\Lambda$-structures,
$\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$ satisfies the downward Löwenheim-
Skolem theorem (in the same formulation as in Theorem 42).

######  Proof 5.7.

Let $\Phi$ be a set of coalgebraic first-order formulas in
$\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$, and let $\mathfrak{M}=(C,\gamma,I)$
be such that $\mathfrak{M}\models\Phi$. Pick Skolem functions for all formulas
$\exists x.\,\phi$ as usual, and for every one-step sound one-step rule
$R=\boldsymbol{A}/\boldsymbol{P}$ fix a Skolem function that given an element
$x\in C$ satisfying some instance of $\neg\boldsymbol{P}$ picks an element of
$C$ that satisfies the corresponding instance of $\neg\boldsymbol{A}$. More
precisely: let $\sigma:\mathsf{iVar}\to\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$
be a substitution, let $x,y$ be variables with $x$ fresh, let
$\boldsymbol{P}^{x,y}\sigma$ be the formula obtained by replacing in
$\boldsymbol{P}$ each modal operator application $\heartsuit\boldsymbol{p}$
with $x\heartsuit\lceil y:\sigma(\boldsymbol{p})\rceil$, and let $v$ be a
valuation such that $\mathfrak{M},v\models\neg\boldsymbol{P}^{x,y}\sigma$.
Then there exists a $y$-variant $v^{\prime}$ of $v$ such that
$\mathfrak{M},v^{\prime}\models\neg\boldsymbol{A}\sigma$, and the Skolem
function $f_{R,\sigma}$ assigns such a $v^{\prime}(y)$ to
$v|_{\mathsf{FV}(\boldsymbol{P}^{x,y}\sigma)}$. As
$\mathsf{FV}(\boldsymbol{P}^{x,y}\sigma)$ is finite, $f_{R,\sigma}$ is a
finitary function, so that closing a given subset $Y_{0}\subseteq C$ of
cardinality $|Y_{0}|=\lambda$ under the Skolem functions yields a set
$Y\subseteq C$ of the same cardinality $|Y|=\lambda$.

The coalgebra structure $\zeta$ that we are to define on $Y$ has to satisfy
the _coherence_ condition

$\zeta(c)\models\heartsuit({[\\![\rho]\\!]}^{y}_{v}\cap Y)\text{ iff
}\gamma(c)\models\heartsuit{[\\![\rho]\\!]}^{y}_{v}$

for all $c\in Y$, all formulas $\rho$, and all valuations $v$ in $Y$, where
the second condition is by definition equivalent to
$c\in{[\\![x\heartsuit\lceil y:\rho\rceil]\\!]}^{x}_{v}$. Once this is
established, we can show as usual that $\mathfrak{N}=(Y,\zeta,J)$, with $J$
interpreting $\Sigma$ by restricting $I$ to $Y$, is an elementary substructure
of $(C,\gamma,I)$, and we are done.

Now assume that $\zeta(c)$ as required fails to exist, which means that the
set $\Phi$ of constraints of the form
$\epsilon\heartsuit({[\\![\rho]\\!]}^{y}_{v}\cap Y)$ (where $\epsilon$ stands
for either nothing or negation) on $\zeta(c)$ determined by the coherence
condition is one-step unsatisfiable. By one-step compactness, already some
finite subset $\Phi_{0}$ of $\Phi$ is unsatisfiable. By Lemma 38 and the
format of $\Phi$, there exist a sound one-step rule
$R=\boldsymbol{A}/\boldsymbol{P}$ and a substitution
$\sigma:\mathsf{sVar}\to\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$ such that
$Y\models\boldsymbol{A}\tau$ and $\boldsymbol{P}\tau=\neg\bigwedge\Phi_{0}$
where $\tau(\boldsymbol{p})={[\\![\sigma(\boldsymbol{p})]\\!]}_{v}^{y}\cap Y$.
However, by construction of $\Phi$ we have
$\gamma(c)\in{[\\![\neg\boldsymbol{P}]\\!]}\hat{\tau}$, where $\hat{\tau}$ is
the $\mathcal{P}(C)$-valuation sending $\boldsymbol{p}\in\mathsf{sVar}$ to
${[\\![\sigma(\boldsymbol{p})]\\!]}^{y}_{v}$, and hence
$\mathfrak{M},v\models\neg\boldsymbol{P}^{x,y}\sigma$ where $x$ is fresh and
we assume w.l.o.g. that $v(x)=c$. Then
$f_{R,\sigma}(v|_{\mathsf{FV}(\boldsymbol{P}^{x,y}\sigma)})\in{[\\![\neg\boldsymbol{A}]\\!]}\tau$,
in contradiction to $Y\models\boldsymbol{A}\tau$.

Besides the plain neighbourhood case, Theorem 44 covers all instances of CPL
defined by imposing rank-1 frame conditions on neighbourhood frames, e.g. CPL
over monotone neighbourhood frames and various deontic logics.

##  6\. Proof theory

###  6.1. Sequent system for CPL

In § 3, we have seen a complete Hilbert calculus for coalgebraic predicate
logic. The present goal is a cut-free, complete sequent calculus. Our basis is
the system $\mathsf{G1c}$ of [Troelstra:1996:BPT] that we extend with modal
rules describing the (fixed) $\Lambda$-structure. Our treatment of equality,
on the other hand, is inspired by Kanger [Kanger1957], Degtyarev and Voronkov
[DegtyarevVoronkov2001] and Seligman [Seligman01:jlc]. In fact, the syntactic
cut-elimination proof presented here is based on Seligman’s ideas.

We take _sequents_ to be pairs $(\Gamma,\Delta)$, written
$\Gamma\Rightarrow\Delta$ where $\Gamma,\Delta\subseteq\mathcal{L}$ are finite
multisets. The sequent calculus for coalgebraic predicate logic contains four
types of rules: the standard logical and structural rules for first-order
logic, rules for equality and rules for the modal operators. The logical rules
are standard as in Table 3. The formula introduced in the conclusion of a
logical rule is called the _principal_ formula of the rule. This applies, in
particular, to the structural rules in Table 3: the formula $\phi$ in the
conclusion is the principal one. Note that, somewhat counterintuitively, in
the equality rules the formula $x=y$ in the conclusion is the _context_ ,
i.e., the only _non-principal_ formula and all the remaining ones are
_principal_!

To account for the modal operators, we incorporate the one-step rules
$\mathcal{R}$ into the sequent system. In principle, we just generate a
sequent rule within CPL from every one-step rule in $\mathcal{R}$. Only for
presentational purposes, we factor this process through an alternative modal
rule format where propositional operators are fully dissolved into sequents:
A rule

$\heartsuit_{1}\vec{\boldsymbol{p}}_{1},\dots,\heartsuit_{n}\vec{\boldsymbol{p}}_{n}\Rightarrow\heartsuit_{n+1}\vec{\boldsymbol{p}}_{n+1},\dots,\heartsuit_{n+m}\vec{\boldsymbol{p}}_{n+m}\Gamma_{1}\Rightarrow\Delta_{1}\cdots\Gamma_{k}\Rightarrow\Delta_{k}$

_represents_ a one-step rule $\boldsymbol{A}/\boldsymbol{P}$ _in sequent
format_ if $\boldsymbol{A}$ is propositionally equivalent to
$\bigwedge_{i=1}^{k}((\bigwedge\Gamma_{i})\to(\bigvee\Delta_{i})$, and
$\boldsymbol{P}$ is propositionally equivalent to
$(\bigwedge_{j=1}^{n}\heartsuit_{j}\vec{\boldsymbol{p}}_{j})\to(\bigvee_{j=n+1}^{m}\heartsuit_{j}\vec{\boldsymbol{p}}_{j})$.
We transfer the existing syntactic restrictions on one-step rules according to
Definition 3.1 to this format by requiring that every schematic variable
occurring in the premise occurs also in the conclusion, and every schematic
variable occurs at most once in the conclusion. It is clear that every one-
step rule can be represented in sequent format (just transform the premise
into conjunctive normal form and then trivially translate disjunctive clauses
into sequents in both premise and conclusion). Subsequently, we generate a
sequent rule $\mathcal{S}(R)$ in CPL syntax, adding weakening contexts
$\Sigma$, $\Theta$ to both the conclusion and all the premises:

$\Sigma,z\heartsuit_{1}\boldsymbol{\lceil
x_{1}\\!:\\!\phi_{1}\rceil},\dots,z\heartsuit_{n}\boldsymbol{\lceil
x_{n}\\!:\\!\phi_{n}\rceil}\Rightarrow\\\ z\heartsuit_{n+1}\boldsymbol{\lceil
x_{n+1}\\!:\\!\phi_{n+1}\rceil},\dots,z\heartsuit_{n+m}\boldsymbol{\lceil
x_{n+m}\\!:\\!\phi_{n+m}\rceil,\Theta}\lx@proof@logical@and\Sigma,\Gamma_{1}\sigma_{\boldsymbol{x}}^{y}\Rightarrow\Delta_{1}\sigma_{\boldsymbol{x}}^{y},\Theta\cdots\Sigma,\Gamma_{k}\sigma_{\boldsymbol{x}}^{y}\Rightarrow\Delta_{k}\sigma_{\boldsymbol{x}}^{y},\Theta$

with syntactic details as summarized in Table 3. The formulas
$z\heartsuit_{i}\boldsymbol{\lceil x\\!:\\!\phi_{i}\rceil}$ are the principal
formulas of $\mathcal{S}(R)$.

Table 3. Sequent System of Coalgebraic Predicate Logic

In all the rules below, $\mathbf{\dagger}_{y}$ means that $y$ is fresh in the
conclusion.

Axioms

$\phi\Rightarrow\phi\quad\bot\Rightarrow\quad\Rightarrow x=x$

Logical Rules

$\Gamma\Rightarrow\Delta,\phi\to\psi\phi,\Gamma\Rightarrow\Delta,\psi\quad\phi\to\psi,\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow\Delta,\phi\psi,\Gamma\Rightarrow\Delta$

$\Gamma\Rightarrow\Delta,\forall
x.\phi\Gamma\Rightarrow\Delta,\phi[y/x]\quad\forall
x.\phi,\Gamma\Rightarrow\Delta\phi[z/x],\Gamma\Rightarrow\Delta$

Equality Rules

$x=y,\Gamma[y/z]\Rightarrow\Delta[y/z]x=y,\Gamma[x/z]\Rightarrow\Delta[x/z]\quad
x=y,\Gamma[x/z]\Rightarrow\Delta[x/z]x=y,\Gamma[y/z]\Rightarrow\Delta[y/z]$

Modal Rules $\mathcal{S}(\mathcal{R})$: for every one-step rule
$R\in\mathcal{R}$,

$z\heartsuit_{n+1}\boldsymbol{\lceil
x_{n+1}\\!:\\!\phi_{n+1}\rceil},\dots,z\heartsuit_{n+m}\boldsymbol{\lceil
x_{n+m}\\!:\\!\phi_{n+m}\rceil},\Theta\Sigma,z\heartsuit_{1}\boldsymbol{\lceil
x_{1}\\!:\\!\phi_{1}\rceil},\dots,z\heartsuit_{n}\boldsymbol{\lceil
x_{n}\\!:\\!\phi_{n}\rceil}\Rightarrow\lx@proof@logical@and\Sigma,\Gamma_{1}\sigma_{\boldsymbol{x}}^{y}\Rightarrow\Delta_{1}\sigma_{\boldsymbol{x}}^{y},\Theta\cdots\Sigma,\Gamma_{k}\sigma_{\boldsymbol{x}}^{y}\Rightarrow\Delta_{k}\sigma_{\boldsymbol{x}}^{y},\Theta$

where

  * •

$R$ is represented in sequent format as
$\heartsuit_{1}\vec{\boldsymbol{p}}_{1},\dots,\heartsuit_{n}\vec{\boldsymbol{p}}_{n}\Rightarrow\heartsuit_{n+1}\vec{\boldsymbol{p}}_{n+1},\dots,\heartsuit_{n+m}\vec{\boldsymbol{p}}_{n+m}\lx@proof@logical@and\Gamma_{1}\Rightarrow\Delta_{1}\cdots\Gamma_{k}\Rightarrow\Delta_{k}$

  * •

$\boldsymbol{\lceil x_{i}\\!:\\!\phi_{i}\rceil}=\lceil
x^{1}_{i}\\!:\\!\phi_{i}^{1}\rceil\dots\lceil
x^{\mathsf{ar}\heartsuit}_{i}\\!:\\!\phi_{i}^{\mathsf{ar}\heartsuit}\rceil$ is
a finite sequence of comprehension formulas according to
$\mathsf{ar}\heartsuit_{i}$, and

  * •

the substitution $\sigma_{\boldsymbol{x}}^{y}$ sends $\boldsymbol{p}_{i}^{j}$
to the formula $\phi_{i}^{j}[y/x_{i}^{j}]$ of $\mathcal{L}$.

Structural Rules

$\Gamma\Rightarrow\Delta,\phi\Gamma\Rightarrow\Delta\quad\phi,\Gamma\Rightarrow\Delta\Gamma\Rightarrow\Delta$

$\Gamma\Rightarrow\Delta,\phi\Gamma\Rightarrow\Delta,\phi,\phi\quad\phi,\Gamma\Rightarrow\Delta\phi,\phi,\Gamma\Rightarrow\Delta$

Cut Rule (optional)

$\Gamma,\Sigma\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow\Delta,\phi\phi,\Sigma\Rightarrow\Theta$

Recall from Example 3.1 that the rule set for the normal modal logic
$\mathsf{K}$ consists of rules that are represented in sequent format as

$\Diamond\boldsymbol{p}\Rightarrow\Diamond\boldsymbol{q}_{1},\dots,\Diamond\boldsymbol{q}_{n}\boldsymbol{p}\Rightarrow\boldsymbol{q}_{1},\dots,\boldsymbol{q}_{n}$

for all $n\geqslant 0$. We obtain the following first-order version

$\Sigma,z\Diamond\lceil x_{0}\\!:\\!\phi_{0}\rceil\Rightarrow z\Diamond\lceil
x_{1}\\!:\\!\phi_{1}\rceil,\dots,z\Diamond\lceil
x_{n}\\!:\\!\phi_{n}\rceil,\Theta\Sigma,\phi_{0}[y/x_{0}]\Rightarrow\phi_{1}[y/x_{1}],\dots,\phi_{n}[y/x_{n}],\Theta$

(where $y$ is fresh in the conclusion) by the previous definition. Recall also
that modal neighbourhood semantics is axiomatised by a one-step rule that is
represented in sequent format as

$\Box\boldsymbol{p}\Rightarrow\Box\boldsymbol{q}\boldsymbol{p}\Rightarrow\boldsymbol{q}\quad\boldsymbol{q}\Rightarrow\boldsymbol{p},$

which expresses that $\Box$ is a congruential operator. The first order
version of $\mathsf{C}$ then reads

$\Sigma,z\Box\lceil x_{0}\\!:\\!\phi_{0}\rceil\Rightarrow z\Box\lceil
x_{1}\\!:\\!\phi_{1}\rceil,\Theta\lx@proof@logical@and\Sigma,\phi_{0}[y/x_{0}]\Rightarrow\phi_{1}[y/x_{1}],\Theta\Sigma,\phi_{1}[y/x_{1}]\Rightarrow\phi_{0}[y/x_{0}],\Theta$

(where $y$ is fresh in the conclusion) which provides a complete and, as we
are going to see below, cut-free axiomatisation of Chang’s original logic.

We write $\mathcal{S}\mathcal{R}\vdash\Gamma\Rightarrow\Delta$ if
$\Gamma\Rightarrow\Delta$ can be derived using the logical rules, equality
rules, and axiom rules of Table 3, together with the rules $\mathcal{S}(R)$
from Table 3 for every rule $R\in\mathcal{R}$.We write
$\mathcal{S}\mathcal{R}\mathsf{Cut}\vdash\Gamma\Rightarrow\Delta$ if the _cut
rule_ $\mathsf{Cut}$ of Table 3 is used additionally. If
$\mathfrak{M}=(C,\gamma,I)$ is a first-order model over a $\Lambda$-structure,
we write $\mathfrak{M},v\models\Gamma\Rightarrow\Delta$ if
$\mathfrak{M},v\models\bigwedge\Gamma\to\bigvee\Delta$ and, as usual
$\mathfrak{M}\models\Gamma\Rightarrow\Delta$ if
$\mathfrak{M},v\models\Gamma\Rightarrow\Delta$ for all variable assignments
$v$ and finally $\models\Gamma\Rightarrow\Delta$ if
$\mathfrak{M}\models\Gamma\Rightarrow\Delta$ for all first-order models
$\mathfrak{M}$ over the corresponding structure, which we elide in the
notation.

######  Proposition 45.

For any one-step rule $R\in\mathcal{R}$ and any model $\mathfrak{M}$ =
$(C,\gamma,I)$, $\mathcal{S}(R)$ preserves the validity on $\mathfrak{M}$.

######  Proof 6.1.

Let $R\in\mathcal{R}$ be represented in sequent format as

$\heartsuit_{1}\vec{\boldsymbol{p}}_{1},\dots,\heartsuit_{n}\vec{\boldsymbol{p}}_{n}\Rightarrow\heartsuit_{n+1}\vec{\boldsymbol{p}}_{n+1},\dots,\heartsuit_{n+m}\vec{\boldsymbol{p}}_{n+m}\lx@proof<EMAIL_ADDRESS>
By Assumption 3.1, $R$ is one-step sound. Let $\mathfrak{M}$ = $(C,\gamma,I)$
be a model. To show that $\mathcal{S}(R)$ preserves validity, assume that all
of
$\Sigma,\Gamma_{i}\sigma_{{\boldsymbol{x}}}^{y}\Rightarrow\Delta_{i}\sigma_{{\boldsymbol{x}}}^{y},\Theta$
($1\leqslant i\leqslant k$) are valid in $\mathfrak{M}$. Fix any variable
assignment $v$ on $C$. To show that the conclusion of $\mathcal{S}(R)$ is true
at $M,v$, assume that $M,v\models\bigwedge\Sigma$ and
$M,v\not\models\bigvee\Theta$. Our goal is to show that

$M,v\models\bigwedge_{1\leqslant i\leqslant
n}z\heartsuit_{i}\boldsymbol{\lceil
x_{i}\\!:\\!\phi_{i}\rceil}\to\bigvee_{1\leqslant j\leqslant
m}z\heartsuit_{n+j}\boldsymbol{\lceil x_{n+j}\\!:\\!\phi_{n+j}\rceil},$

i.e.,

if $\gamma(v(z))\in\bigcap_{1\leqslant i\leqslant
n}\llbracket\heartsuit_{i}\rrbracket_{C,v}(\llbracket\phi_{i}^{1}\rrbracket^{x_{i}^{1}}_{C,v},\ldots,\llbracket\phi_{i}^{\mathsf{ar}\heartsuit_{i}}\rrbracket^{x_{i}^{\mathsf{ar}\heartsuit_{i}}}_{C,v})$

then $\gamma(v(z))\in\bigcup_{1\leqslant j\leqslant
m}\llbracket\heartsuit_{n+j}\rrbracket_{C,v}(\llbracket\phi_{n+j}^{1}\rrbracket^{x_{n+j}^{1}}_{C,v},\ldots,\llbracket\phi_{n+j}^{\mathsf{ar}\heartsuit_{n+j}}\rrbracket^{x_{n+j}^{\mathsf{ar}\heartsuit_{n+j}}}_{C,v})$
.

Let us define a valuation $\tau:\mathsf{sVar}\to\mathcal{P}(C)$ by
$\tau(\boldsymbol{p_{i}^{j}})$ =
$\llbracket\phi_{i}^{j}[y/x_{i}^{j}]\rrbracket^{y}_{C,v}$. To show that
$C,\tau\models\bigwedge\Gamma_{i}\to\bigvee\Delta_{i}$ for all $1\leqslant
i\leqslant k$, let us fix any $c\in C$. Since $y$ is fresh in the conclusion
of $\mathcal{S}(R)$, it follows from $M,v\models\bigwedge\Sigma$ and
$M,v\not\models\bigvee\Theta$ that $M,v[c/y]\models\bigwedge\Sigma$ and
$M,v[c/y]\not\models\bigvee\Theta$. Then from our assumption of the validity
of all premises of $\mathcal{S}(R)$ on a pair $(M,v)$, we obtain
$M,v[c/y]\models\Gamma_{i}\sigma_{{\boldsymbol{x}}}^{y}\Rightarrow\Delta_{i}\sigma_{{\boldsymbol{x}}}^{y}$,
which implies $c\in\tau(\bigwedge\Gamma_{i}\to\bigvee\Delta_{i})$, as desired.
Since $R$ is one-step sound, we have that
$TC,\tau\models{\bigwedge}_{1\leqslant i\leqslant
n}\heartsuit_{i}\vec{\boldsymbol{p}}_{i}\to{\bigvee}_{1\leqslant j\leqslant
m}\heartsuit_{n+j}\vec{\boldsymbol{p}}_{n+j}$. Because
$\tau(\boldsymbol{p_{i}^{j}})$ =
$\llbracket\phi_{i}^{j}[y/x_{i}^{j}]\rrbracket^{y}_{C,v}$ =
$\llbracket\phi_{i}^{j}\rrbracket^{x_{i}^{j}}_{C,v}$ by freshness of $y$, we
can conclude our desired implication above.

We show soundness and completeness of the sequent system
$\mathcal{S}\mathcal{R}$ by translating into, and from, the Hilbert system
$\mathcal{H}\mathcal{R}$ which is known to be (semantically) complete when
$\mathcal{R}$ is strongly one-step complete. Note that
$\mathcal{H}\mathcal{R}$ does not include the the BdPL♭Λ-axioms. Before
showing that both systems $\mathcal{H}\mathcal{R}$ and
$\mathcal{S}\mathcal{R}\mathsf{Cut}$ have the same deductive power, we note
one consequence of the congruence rule (Remark 4) provided that the rules
absorb congruence. We introduce the concept of absorption in a slightly more
general form which will be used later.

We say that a finite set $\mathbb{S}$ of sequents _covers_ a finite set
$\mathbb{S}^{\prime}$ of sequents if each element $\Gamma\Rightarrow\Delta$ of
$\mathbb{S}^{\prime}$ contains some element $\Pi\Rightarrow\Sigma$ of
$\mathbb{S}$ in the sense that $\Pi\subseteq\Gamma$ and
$\Sigma\subseteq\Delta$. We write $\mathbb{S}\rhd\mathbb{S}^{\prime}$ if
$\mathbb{S}$ covers $\mathbb{S}^{\prime}$ where we identify sequents with
singleton sets. A set $\mathcal{R}$ of rules _absorbs_ a rule
$\Sigma_{1}\Rightarrow\Theta_{1},\cdots,\Sigma_{m}\Rightarrow\Theta_{m}/\Sigma\Rightarrow\Theta$
if there exists a rule
$R=\Gamma_{1}\Rightarrow\Delta_{1},\cdots,\Gamma_{n}\Rightarrow\Delta_{n}/\Gamma_{R}\Rightarrow\Delta_{R}\in\mathcal{R}$
such that

$\\{\Sigma_{1}\Rightarrow\Theta_{1},\ldots,\Sigma_{m}\Rightarrow\Theta_{m}\\}\rhd\\{\Gamma_{1}\Rightarrow\Delta_{1},\ldots,\Gamma_{n}\Rightarrow\Delta_{n}\\}$

and $\Gamma_{R}\Rightarrow\Delta_{R}\rhd\Sigma\Rightarrow\Theta$. A rule set
_absorbs congruence_ if it absorbs the rule

$\heartsuit(p_{1},\ldots,p_{n})\Rightarrow\heartsuit(q_{1},\ldots,q_{n})\lx@proof@logical@and
p_{1}\Rightarrow q_{1}\cdots p_{n}\Rightarrow q_{n}q_{1}\Rightarrow
p_{1}\cdots q_{n}\Rightarrow p_{n}$

and it _absorbs monotonicity of $\heartsuit$ in the $i$-th argument_ if the
rule

$\heartsuit(p_{1},\dots,p_{n})\Rightarrow\heartsuit(p_{1},\dots,p_{i-1},q_{i},p_{i+1},\dots
p_{n})p_{i}\Rightarrow q_{i}$

is absorbed.

######  Lemma 46.

When $\mathcal{R}$ absorbs congruence, the following congruence rule

$\Sigma,z\heartsuit\boldsymbol{\lceil x_{0}:\phi_{0}\rceil}\Rightarrow
z\heartsuit\boldsymbol{\lceil
x_{1}:\phi_{1}\rceil},\Theta\lx@proof@logical@and\\{\Sigma,\phi_{0}^{j}[y/{x_{0}^{j}}]\Rightarrow\phi_{1}^{j}[y/{x_{1}^{j}}],\Theta\Sigma,\phi_{1}^{j}[y/{x_{1}^{j}}]\Rightarrow\phi_{0}^{j}[y/{x_{0}^{j}}],\Theta\,|\,1\leqslant
j\leqslant n\\}$

$($where $y$ is fresh in the conclusion and $n$ is the arity of
$\heartsuit$$)$ is admissible in $\mathcal{S}\mathcal{R}$ and
$\mathcal{S}\mathcal{R}\mathsf{Cut}$.

######  Proof 6.2.

Since $\mathcal{R}$ absorbs congruence, we can find a one-step rule $R$ =
$\Gamma_{1}\Rightarrow\Delta_{1},\cdots,\Gamma_{m}\Rightarrow\Delta_{m}/\Gamma_{R}\Rightarrow\Delta_{R}\in\mathcal{R}$
such that $\\{p_{j}\Rightarrow q_{j},q_{j}\Rightarrow p_{j}\,|\,1\leqslant
j\leqslant
n\\}\rhd\\{\Gamma_{1}\Rightarrow\Delta_{1},\ldots,\Gamma_{m}\Rightarrow\Delta_{m}\\}$
and
$\Gamma_{R}\Rightarrow\Delta_{R}\rhd\heartsuit(p_{1},\ldots,p_{n})\Rightarrow\heartsuit(q_{1},\ldots,q_{n})$.
Fix such a one-step rule $R$. Assume that
$\Sigma,\phi_{0}^{j}[y/{x_{0}^{j}}]\Rightarrow\phi_{1}^{j}[y/{x_{1}^{j}}],\Theta$
and
$\Sigma,\phi_{1}^{j}[y/{x_{1}^{j}}]\Rightarrow\phi_{0}^{j}[y/{x_{0}^{j}}],\Theta$
are derivable in $\mathcal{S}\mathcal{R}$ for all $1\leqslant j\leqslant n$.
Let us define the substitution $\sigma_{\boldsymbol{x}}^{y}$ which sends each
$\boldsymbol{p}^{j}_{i}$ to a formula $\phi^{j}_{i}[y/x_{i}^{j}]$, where $i$ =
$0$ or $1$. Since $\\{p_{j}\Rightarrow q_{j},q_{j}\Rightarrow
p_{j}\,|\,1\leqslant j\leqslant
n\\}\rhd\\{\Gamma_{1}\Rightarrow\Delta_{1},\ldots,\Gamma_{m}\Rightarrow\Delta_{m}\\}$,
we can obtain the derivability of
$\Sigma,\Gamma_{k}\sigma_{\boldsymbol{x}}^{y}\Rightarrow\Delta_{k}\sigma_{\boldsymbol{x}}^{y},\Theta$
($1\leqslant k\leqslant m$) in $\mathcal{S}\mathcal{R}$ with the help of
weakening rules. Since $R\in\mathcal{R}$, the covering
$\Gamma_{R}\Rightarrow\Delta_{R}\rhd\heartsuit(p_{1},\ldots,p_{n})\Rightarrow\heartsuit(q_{1},\ldots,q_{n})$
and the weakening rules allow us to obtain the derivability of
$\Sigma,z\heartsuit\boldsymbol{\lceil x_{0}:\phi_{0}\rceil}\Rightarrow
z\heartsuit\boldsymbol{\lceil x_{1}:\phi_{1}\rceil},\Theta$ in
$\mathcal{S}\mathcal{R}$, as required.

By our equality rules, the following lemma is immediate.

######  Lemma 47.

The replacement axiom $x=y,\phi[x/z]\Rightarrow\phi[y/z]$ is derivable in
$\mathcal{S}\mathcal{R}$.

One direction of the translation between the two proof systems can now be
given as follows:

######  Theorem 48.

Suppose that $\mathcal{R}$ absorbs congruence and let
$\mathcal{H}\mathcal{R}\vdash\phi$. Then
$\mathcal{S}\mathcal{R}\mathsf{Cut}\vdash\Rightarrow\phi$.

######  Proof 6.3.

First, we demonstrate admissibility of modus ponens in
$\mathcal{S}\mathcal{R}\mathsf{Cut}$ by

$\Rightarrow\psi\lx@proof@logical@and\Rightarrow\phi\phi\Rightarrow\psi\lx@proof@logical@and\Rightarrow\phi\to\psi\phi\to\psi,\phi\Rightarrow\psi$

where the derivability of $\phi\to\psi,\phi\Rightarrow\psi$ is easily
established by $\mathsf{L\to}$. Note that this is the only place in this proof
where we need $\mathsf{Cut}$. Hence, it suffices to show that all the axioms
of $\mathcal{H}\mathcal{R}$ (recall Table 3) are derivable in cut-free
$\mathcal{S}\mathcal{R}$. All of equality axioms En5, En6.1 and En6.2 are
derivable by the equality axiom $\mathsf{R=}$ and the equality rules
$\mathsf{L=_{i}}$. Moreover, since this is easy to show for logical but non-
modal axioms, we focus on Cong, Alpha and Onestep($\mathcal{R}$). Firstly, the
derivability of Cong follows from Lemma 46. Secondly, for Alpha we have the
following derivation:

$z\heartsuit{\lceil x_{0}:\phi_{0}\rceil}\cdots{\lceil
x_{i}:\phi_{i}\rceil}\cdots{\lceil x_{n}:\phi_{n}\rceil}\Rightarrow
z\heartsuit{\lceil x_{0}:\phi_{0}\rceil}\cdots{\lceil
u:\phi_{i}[u/x_{i}]\rceil}\cdots{\lceil
x_{n}:\phi_{n}\rceil}\lx@proof@logical@and\\{\phi_{j}[y/{x_{j}}]\Rightarrow\phi_{j}[y/{x_{j}}]\,|\,j\neq
i\\}\phi_{i}[y/{x_{i}}]\Rightarrow\phi_{i}[u/{x_{i}}][y/u]\phi_{i}[u/{x_{i}}][y/u]\Rightarrow\phi_{i}[y/{x_{i}}]$

where we note that $\mathsf{Cong}\heartsuit$ is admissible by Lemma 46. All
the premises are axioms since $u$ is assumed to be fresh in $\phi_{i}$.
Finally, let us move to the provability of Onestep($\mathcal{R}$). Suppose
that
$R=\Gamma_{1}\Rightarrow\Delta_{1},\dots,\Gamma_{k}\Rightarrow\Delta_{k}/\Gamma_{R}\Rightarrow\Delta_{R}$
is a one-step rule as in Definition 3.1. With the help of contraction rules,
we note that the following are derivable rules in $\mathcal{S}\mathcal{R}$:
for any finite multiset $\Theta$,

$\bigwedge\Theta,\Gamma\Rightarrow\Delta\Theta,\Gamma\Rightarrow\Delta\quad\Gamma\Rightarrow\Delta,\bigvee\Theta\Gamma\Rightarrow\Delta,\Theta.$

We obtain the following derivation where $N$ = $\\{1,...,n\\}$, $M$ =
$\\{n+1,...,n+m\\}$ and $\pi_{i}$ is an abbreviation of
$(\bigwedge\Gamma_{i}\to\bigvee\Delta_{i})\sigma$:

$\forall
x.(\pi_{1}\land\cdots\land\pi_{n}),\bigwedge\\{x\heartsuit_{i}\boldsymbol{\lceil
x:\phi_{i}\rceil}\,|\,i\in
N\\}\Rightarrow\bigvee\\{x\heartsuit_{i}\boldsymbol{\lceil
x:\phi_{i}\rceil}\,|\,i\in M\\}\forall
x.(\pi_{1}\land\cdots\land\pi_{n}),\\{x\heartsuit_{i}\boldsymbol{\lceil
x:\phi_{i}\rceil}\,|\,i\in N\\}\Rightarrow\\{x\heartsuit_{i}\boldsymbol{\lceil
x:\phi_{i}\rceil}\,|\,i\in M\\}\\{\forall
x.(\pi_{1}\land\cdots\land\pi_{n}),(\Gamma_{i}\sigma)[y/x]\Rightarrow(\Delta_{i}\sigma)[y/x]\,|\,1\leqslant
i\leqslant
k\\}{\\{\pi_{1}[y/x]\land\cdots\land\pi_{n}[y/x],(\Gamma_{i}\sigma)[y/x]\Rightarrow(\Delta_{i}\sigma)[y/x]\,|\,1\leqslant
i\leqslant k\\}}$

which shows derivability of the axiom Onestep($\mathcal{R}$) as the top
sequent is readily seen to be derivable in $\mathcal{S}\mathcal{R}$.

For the converse direction, absorption of congruence is not required.

######  Theorem 49.

Suppose that
$\mathcal{S}\mathcal{R}\mathsf{Cut}\vdash\Gamma\Rightarrow\Delta$. Then
$\mathcal{H}\mathcal{R}\vdash\bigwedge\Gamma\to\bigvee\Delta$.

######  Proof 6.4.

It suffices to show that all the translations of the axioms and rules of
$\mathcal{S}\mathcal{R}$ are derivable in $\mathcal{H}\mathcal{R}$. We can
easily handle the cases of the axioms and rules for logical connectives of
first-order logic. The provability of the translation of $\mathsf{L=_{i}}$
follows from the provability of $x=y\to(\phi[x/w]\to\phi[y/w])$. As for
$\heartsuit\in\Lambda$, the provability of the translation of $\mathcal{S}(R)$
follows from Onestep($\mathcal{R}$) and Alpha.

As a corollary, we obtain (for the time being, in a calculus with cut) both
soundness and completeness of the sequent calculus.

######  Corollary 50.

Suppose that $\mathcal{R}$ is strongly one-step complete. Then
$\mathcal{S}\mathcal{R}\mathsf{Cut}\vdash\Gamma\Rightarrow\Delta$ iff
$\models\Gamma\Rightarrow\Delta$.

######  Proof 6.5.

By Theorems 48 and 49 in conjunction with soundness and completeness of
$\mathcal{H}\mathcal{R}$ (Theorem 9). The absorption of congruence was shown
in [PattinsonSchroder10, Proposition 5.12].

A paradigmatic example of a set of rules satisfying the assumptions of
Corollary 50 is $\mathsf{C}$ and its CPL translation $\mathcal{S}(\mathsf{C})$
from Example 6.1 above.

As we have seen in § 3, the assumption of _strongly_ one-step complete rule
sets limits available examples to “essentially neighbourhood-like” ones. This
is why we also gave a complete Hilbert-style axiomatisation also for _bounded_
operators (recall Definition 3.1).

Note that $k$-boundedness of $i$-th argument of Definition 3.1 implies in
particular that $\heartsuit$ is monotonic in the $i$-th argument. Examples of
bounded modalities include the standard $\Diamond$ of relational modal logic
interpreted over Kripke frames, graded modalities over multigraphs and we
refer to [SchroderPattinson10] for more examples. In the Hilbert-calculus,
boundedness was reflected syntactically by the axiom

$\axiom{BdPL}{}_{k,i}\,\forall\vec{y}.(x\heartsuit\lceil
y_{1}:\phi_{1}\rceil\dots\lceil y_{n}:\phi_{n}\rceil\leftrightarrow\exists
z_{1}\dots z_{k}.(x\heartsuit\lceil y_{1}:\phi_{1}\rceil\dots\lceil
y_{i-1}:\phi_{i-1}\rceil\\\ \qquad\lceil y_{i}:y_{i}=z_{1}\vee\dots\vee
y_{i}=z_{k}\rceil\lceil y_{i+1}:\phi_{i+1}\rceil\dots\lceil
y_{n}:\phi_{n}\rceil\wedge\bigwedge\limits_{j\leqslant
k}\phi_{i}[y_{i}/z_{j}]))$

where each $z_{i}$ is fresh for all the $y_{i}$s and $\phi_{i}$s. The
derivability predicate induced by extending the Hilbert calculus
$\mathcal{H}\mathcal{R}$ by the boundedness axiom above gives completeness
under weaker conditions.  We write
$\mathcal{B}\mathcal{H}\mathcal{R}\vdash\phi$ if $\phi$ is derivable in
$\mathcal{H}\mathcal{R}$ where additionally  is used for every operator that
is $k$-bounded in the $i$-th argument. Strictly speaking, the derivability
predicate $\mathcal{B}\mathcal{H}\mathcal{R}$ should include information about
precisely which operators are assumed to be $k$-bounded in the $i$-th
argument, but this will always be clear from the context. In the presence of
boundedness, completeness of the Hilbert-calculus has been established under
weaker conditions (see Theorem 9).

We can reflect boundedness in the sequent calculus by adding a paste rule,
similar in spirit to the paste rule of hybrid logic [BlackburnEA01, § 7] which
was generalised to a coalgebraic setting in [SchroderPattinson10]. In a
sequent setting, this rule takes the form

$\raise 11.0pt\hbox{${\hbox{$\displaystyle\displaystyle{\hbox{\hskip
186.46231pt\vbox{\hbox{\hskip-186.46231pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x\heartsuit{\lceil
x_{1}\\!:\\!\phi_{1}\rceil}\cdots{\lceil x_{i-1}\\!:\\!\phi_{i-1}\rceil}\lceil
y:\bigvee_{1\leqslant j\leqslant k}y=z_{j}\rceil{\lceil
x_{i+1}\\!:\\!\phi_{i+1}\rceil}\cdots{\lceil
x_{n}\\!:\\!\phi_{n}\rceil},$}\hskip
20.00003pt\hbox{\hskip-92.61148pt\hbox{\hbox{$\displaystyle\displaystyle\phi[z_{1}/y],...,\phi[z_{k}/y]\Rightarrow\Delta$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
z_{1},\dots,z_{k}\,\mathrm{fresh}$}}}}}}\vbox{\hbox{\hskip-92.61148pt\hbox{\hbox{$\displaystyle\displaystyle\phi[z_{1}/y],...,\phi[z_{k}/y]\Rightarrow\Delta$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
z_{1},\dots,z_{k}\,\mathrm{fresh}$}}}}\vbox{}}}}\over\hbox{\hskip
116.78175pt\vbox{\vbox{}\hbox{\hskip-116.78174pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x\heartsuit{\lceil
x_{1}\\!:\\!\phi_{1}\rceil}\cdots{\lceil x_{i-1}\\!:\\!\phi_{i-1}\rceil}\lceil
y:\phi\rceil{\lceil x_{i+1}\\!:\\!\phi_{i+1}\rceil}\cdots{\lceil
x_{n}\\!:\\!\phi_{n}\rceil}\Rightarrow\Delta$}}}}}}$}}\hbox{\hbox{}\hbox
to0.0pt{$\;\hbox{\small\small{\mbox{$\mathsf{\mathsf{Paste}^{k}_{i}}$}}}$\hss}}$},$

where $z_{1}$, …, $z_{k}$ are pairwise distinct fresh variables. Additional
use of the above paste-rule in the system $\mathcal{S}\mathcal{R}$ is denoted
by $\mathcal{B}\mathcal{S}\mathcal{R}$, that is, we write
$\mathcal{B}\mathcal{S}\mathcal{R}\vdash\Gamma\Rightarrow\Delta$ if
$\Gamma\Rightarrow\Delta$ is derivable in $\mathcal{S}\mathcal{R}$ where
$\mathsf{Paste}^{k}_{i}$ may additionally be applied for every modality that
is $k$-bounded in the $i$-th argument.

When $\mathcal{R}$ absorbs congruence and monotonicity of all operators that
are $k$-bounded in the $i$-th argument, we note that Lemmas 46 and 47 hold
also for $\mathcal{B}\mathcal{S}\mathcal{R}$.

######  Theorem 53.

Suppose that $\mathcal{R}$ absorbs congruence and monotonicity in the $i$-th
argument of every operator that is $k$-bounded in the $i$-th argument. Then
$\mathcal{B}\mathcal{H}\mathcal{R}\vdash\phi$ implies that
$\mathcal{B}\mathcal{S}\mathcal{R}\mathsf{Cut}\vdash\Rightarrow\phi$.

######  Proof 6.6.

First of all, if $\mathcal{R}$ absorbs monotonicity in the $i$-th argument of
$\heartsuit\in\Lambda$, the rule

$\Sigma,z\heartsuit\boldsymbol{\lceil x:\phi\rceil}\Rightarrow
z\heartsuit\lceil x_{1}:\phi_{1}\rceil\dots\lceil
x_{i-1}:\phi_{i-1}\rceil\lceil x_{i}:\psi\rceil\lceil
x_{i+1}:\phi_{i+1}\rceil\dots\lceil
x_{n}:\phi_{n}\rceil,\Theta\Sigma,\phi_{i}[y/x_{i}]\Rightarrow\psi[y/x],\Theta$

(where $y$ is fresh in the conclusion) is admissible in
$\mathcal{B}\mathcal{S}\mathcal{R}$ (and
$\mathcal{B}\mathcal{S}\mathcal{R}\mathsf{Cut}$). Almost all the arguments are
the same as the proof of Theorem 48, except that we need to show the
provability of

The reverse direction of Theorem 53 is established analogously to Theorem 49
and again absorption properties are not needed.

######  Theorem 57.

$\mathcal{B}\mathcal{S}\mathcal{R}\mathsf{Cut}\vdash\Gamma\Rightarrow\Delta$
only if
$\mathcal{B}\mathcal{H}\mathcal{R}\vdash\bigwedge\Gamma\to\bigvee\Delta$.

######  Proof 6.7.

The only difference from the proof of Theorem 48 is to need to care about the
translation of $\mathsf{Paste}$. However, we can easily establish this by the
axiom $\mathrm{BDLP}$.

As in the non-bounded case we obtain semantic soundness and completeness, but
under weaker coherence conditions.

######  Corollary 58.

Suppose that $\mathcal{R}$ is strongly finitary one-step complete. Then
$\mathcal{B}\mathcal{S}\mathcal{R}\mathsf{Cut}\vdash\Gamma\Rightarrow\Delta$
iff $\models\Gamma\Rightarrow\Delta$.

######  Proof 6.8.

By Theorems 53 and 57 in conjunction with soundness and completeness of
$\mathcal{B}\mathcal{H}\mathcal{R}$ (Theorem 9). Note that absorption of
congruence and monotonicity follows from (strong, finitary) one-step
completeness as in [PattinsonSchroder10, Proposition 5.12].

A canonical example of a rule set satisfying the assumptions of the above
corollary can be obtained by taking $\mathsf{K}$ of Example 6.1 and extending
it with $\mathsf{Paste}^{k}_{i}$ for $i=k=n=1$.

###  6.2. Admissibility of Cut

When we try to prove the admissibility of $\mathsf{Cut}$ in first-order logic
(or $\mathcal{S}\mathcal{R}$), we encounter difficulties with the rules of
contraction. That is, the following derivation:

$\mathcal{D}={\Gamma,\Sigma\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow\Delta,\phi\Gamma\Rightarrow\Delta,\phi,\phi\mathcal{D}^{\prime}\phi,\Sigma\Rightarrow\Theta\mathcal{D}^{\prime\prime},}$

may be transformed into:

$\Gamma,\Sigma\Rightarrow\Delta,\Theta\Gamma,\Sigma,\Sigma\Rightarrow\Delta,\Theta,\Theta\lx@proof@logical@and\Gamma,\Sigma\Rightarrow\Delta,\Theta,\phi\lx@proof@logical@and{\Gamma\Rightarrow\Delta,\phi,\phi\mathcal{D}^{\prime}}\phi,\Sigma\Rightarrow\Theta\mathcal{D}^{\prime\prime}\phi,\Sigma\Rightarrow\Theta\mathcal{D}^{\prime\prime},$

but this derivation does not provide us with a reduction in terms of the
number of sequents above the application of $\mathsf{Cut}$ in $\mathcal{D}$.
This is why Gentzen introduced the following generalized form of
$\mathsf{Cut}$:

$\Gamma,\Sigma\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow\Delta,\phi^{m}\phi^{n},\Sigma\Rightarrow\Theta$

where $n$, $m\geqslant 1$ and $\phi^{k}$ stands for $k$ copies of $\phi$ and
“$Mcut$” is a shorthand of “multi-cut” (sometimes also called “mix”). Since
$\mathsf{Cut}$ is a special case of the new rule of $\mathsf{Mcut}$, it
suffices for us to prove the admissibility of $\mathsf{Mcut}$ in a given
sequent system to obtain the admissibility of $\mathsf{Cut}$ in the system.

Moreover, we note that _a priori_ we cannot expect that an application of
$\mathsf{Mcut}$ between two instances of modal rules can be moved up without
changing the conclusion: the set $\mathcal{R}$ of one-step rules can possibly
consist of a single rule, and an application of $\mathsf{Mcut}$ between this
rule and itself may not be derivable. We therefore need to impose an
additional requirement to deal with this case.

Let $\mathbb{S}$ be a finite set of sequents. The set of all sequents that can
be derived from premises in $\mathbb{S}$ using (only) one application of
$\mathsf{Mcut}$ is denoted by $\mathsf{MCut}(\mathbb{S})$. A rule set
$\mathcal{R}$ _absorbs multicut_ , if for all pairs $(R_{1},R_{2})$ of rules
in $\mathcal{R}$:

$\Gamma_{R_{1}}\Rightarrow\Delta_{R_{1}},(\heartsuit\vec{\boldsymbol{p}}\,)^{m}\lx@proof@logical@and\Gamma_{11}\Rightarrow\Delta_{11}\cdots\Gamma_{1r_{1}}\Rightarrow\Delta_{1r_{1}}\quad(\heartsuit\vec{\boldsymbol{p}}\,)^{n},\Gamma_{R_{2}}\Rightarrow\Delta_{R_{2}}\lx@proof@logical@and\Gamma_{21}\Rightarrow\Delta_{21}\cdots\Gamma_{2r_{2}}\Rightarrow\Delta_{2r_{2}}$

there is a rule $R$ =
$\Gamma_{1}\Rightarrow\Delta_{1},\cdots,\Gamma_{k}\Rightarrow\Delta_{k}/\Gamma_{R}\Rightarrow\Delta_{R}\in\mathcal{R}$
such that:

$\mathsf{MCut}(\Gamma_{11}\Rightarrow\Delta_{11},\ldots,\Gamma_{1r_{1}}\Rightarrow\Delta_{1r_{1}},\Gamma_{21}\Rightarrow\Delta_{21},\ldots,\Gamma_{2r_{2}}\Rightarrow\Delta_{2r_{2}})\rhd\\{\Gamma_{1}\Rightarrow\Delta_{1},\ldots,\Gamma_{k}\Rightarrow\Delta_{k}\\}$

and
$\Gamma_{R}\Rightarrow\Delta_{R}\rhd\Gamma_{R_{1}},\Gamma_{R_{2}}\Rightarrow\Delta_{R_{1}},\Delta_{R_{2}}$.

######  Lemma 59.

If $\mathcal{S}\mathcal{R}\vdash\Gamma\Rightarrow\Delta$ and $y$ is fresh in
$\Gamma$ and $\Delta$, then
$\mathcal{S}\mathcal{R}\vdash\Gamma[y/x]\Rightarrow\Delta[y/x]$ with the same
height of derivation.

######  Lemma 60 (Hauptsatz).

Let $\mathcal{D}$ be a derivation in the system $\mathcal{S}\mathcal{R}$
extended with $\mathsf{Mcut}$ in the following form:

${\Gamma,\Sigma\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow\Delta,\phi^{m}\phi^{n},\Sigma\Rightarrow\Theta,}$

where $\mathcal{D}_{\texttt{L}}$ and $\mathcal{D}_{\texttt{R}}$ contain no
application of $\mathsf{Mcut}$, the last rule of $\mathcal{D}$ is the only
application of $\mathsf{Mcut}$ in $\mathcal{D}$. Then
$\Gamma,\Sigma\Rightarrow\Delta,\Theta$ is derivable in
$\mathcal{S}\mathcal{R}$.

######  Proof 6.9.

First of all, we introduce some terminology used only in this proof. Let
$\mathcal{D}$ be the derivation in question. We say that $\phi$ is a cut
formula of $\mathcal{D}$, and we define the complexity
$\texttt{c}(\mathcal{D})$ as the complexity of the cut formula $\phi$, i.e.,
the length or the number of connectives including the logical and modal
connectives. Moreover, we define $\texttt{w}(\mathcal{D})$ as the total number
of sequents in $\mathcal{D}_{\texttt{L}}$ and $\mathcal{D}_{\texttt{R}}$. Our
proof of the statement of the claim is shown by the double induction on
$(\texttt{c}(\mathcal{D}),\texttt{w}(\mathcal{D}))$ (note that
$\texttt{c}(\mathcal{D})\geqslant 0$ and $\texttt{w}(\mathcal{D})\geqslant
2$). Let us denote the last applied rule (or axiom, possibly) of a derivation
$\mathcal{E}$ by $\texttt{rule}(\mathcal{E})$. We divide our argument into the
following (exhaustive) cases:

  1. (1)

One of $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is an axiom.

  2. (2)

One of $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is a structural rule.

  3. (3)

One of $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is a logical rule or a modal rule
and the cut formula is not principal in the rule.

  4. (4)

Both $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ are logical rules for the same
logical connective and the cut formula is principal in each of the rules.

  5. (5)

Both $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ are modal rules and the cut formula
is principal in each of the rules.

  6. (6)

One of $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is an equality rule.

Let us check each case one by one.

  1. (1)

One of $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is an axiom: We have four cases
since it is impossible that $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is
$\mathsf{L\bot}$ or $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is
$\mathsf{R=}$. Firstly, when $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is
$\mathsf{Ax}$, let the derivation be

$\phi,\Sigma\Rightarrow\Theta\lx@proof@logical@and\phi\Rightarrow\phi\phi^{n},\Sigma\Rightarrow\Theta.$

When $n$ = $1$, we already obtain the derivability of
$\phi,\Sigma\Rightarrow\Theta$ in $\mathcal{S}\mathcal{R}$. When $n\geqslant
2$, $\phi,\Sigma\Rightarrow\Theta$ is obtained from
$\phi^{n},\Sigma\Rightarrow\Theta$ by finitely many applications of
$\mathsf{LC}$.

Secondly, when $\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is $\mathsf{Ax}$, the
argument is similar to the previous case where
$\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is $\mathsf{Ax}$.

Thirdly, when $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is $\mathsf{R=}$, we
need to look at what the last rule $\texttt{rule}(\mathcal{D}_{\texttt{R}})$
is, where $\mathcal{D}$ is of the following form:

${\Sigma\Rightarrow\Theta\lx@proof@logical@and\Rightarrow
x=x(x=x)^{n},\Sigma\Rightarrow\Theta.}$

If $\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is an axiom, then it should be
$\mathsf{Ax}$ and we have already checked this case in our second case of this
item. Otherwise, $\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is a structural
rule, a logical rule, a modal rule or an equality rule. These cases will be
discussed below (especially (2), (3) and (6)), so we leave them out for now.
It is, however, noted that the cut formula $x=x$ is not principal in the case
(3).

Fourthly, when $\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is $\mathsf{L\bot}$,
then we need to look at the last rule
$\texttt{rule}(\mathcal{D}_{\texttt{L}})$, where $\mathcal{D}$ is

${\Gamma\Rightarrow\Delta\lx@proof@logical@and\Gamma\Rightarrow\Delta,\bot^{m}\bot\Rightarrow}.$

If $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is an axiom, it should be
$\mathsf{Ax}$ and we have already checked such case in the first case of this
item. Otherwise, $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ must be a
structural rule, a logical rule, an modal rule or an equality rule. Again
these cases will be discussed below (especially (2), (3) and (6), where it is
noted that the cut formula $\bot$ is not principal in the case (3)), so we
leave them out for now.

  2. (2)

One of $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is a structural rule: all arguments
for this case are standard, so we deal only with the case where
$\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is $\mathsf{RC}$, i.e.,
$\mathcal{D}$ is of the following form:

${\Gamma,\Sigma\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow\Delta,\phi^{m}\Gamma\Rightarrow\Theta,\phi^{m+1}\phi^{n},\Sigma\Rightarrow\Theta,}$

since multicut plays an essential role. This derivation is transformed into:

$\Gamma,\Sigma\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow\Delta,\phi^{m+1}\phi^{n},\Sigma\Rightarrow\Theta$

where the application of $\mathsf{Mcut}$ is eliminable since the complexity of
the derivation is the same as $\texttt{c}(\mathcal{D})$ and the weight of the
derivation is smaller than $\texttt{w}(\mathcal{D})$.

  3. (3)

One of $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is a logical rule or a modal rule
and the cut formula is not principal in the rule: Our argument for logical
rules are standard, so we focus on the case where one of the rules is a modal
rule $\mathcal{S}(R)$. Let $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is
$\mathcal{S}(R)$. Then our derivation $\mathcal{D}$ is of the following form:

$z\heartsuit_{n+1}\boldsymbol{\lceil
x\\!:\\!\phi_{n+1}\rceil},\dots,z\heartsuit_{n+m}\boldsymbol{\lceil
x\\!:\\!\phi_{n+m}\rceil},\Theta^{\prime},\Theta\Sigma,\Sigma^{\prime},z\heartsuit_{1}\boldsymbol{\lceil
x\\!:\\!\phi_{1}\rceil},\dots,z\heartsuit_{n}\boldsymbol{\lceil
x\\!:\\!\phi_{n}\rceil}\Rightarrow\lx@proof@logical@and
z\heartsuit_{n+1}\boldsymbol{\lceil
x\\!:\\!\phi_{n+1}\rceil},\dots,z\heartsuit_{n+m}\boldsymbol{\lceil
x\\!:\\!\phi_{n+m}\rceil},\Theta^{\prime},\phi^{m}\Sigma^{\prime},z\heartsuit_{1}\boldsymbol{\lceil
x\\!:\\!\phi_{1}\rceil},\dots,z\heartsuit_{n}\boldsymbol{\lceil
x\\!:\\!\phi_{n}\rceil}\Rightarrow\Sigma^{\prime},(\Gamma_{1}\sigma)[y/x]\Rightarrow(\Delta_{1}\sigma)[y/x],\Theta^{\prime},\phi^{m}\cdots\Sigma^{\prime},(\Gamma_{k}\sigma)[y/x]\Rightarrow(\Delta_{k}\sigma)[y/x],\Theta^{\prime},\phi^{m}\phi^{n},\Sigma\Rightarrow\Theta$

where $\mathbf{\dagger}_{y}$ in the application of $\mathcal{S}(R)$ means that
$y$ is fresh in the conclusion. For each $\mathcal{D}_{\texttt{L}_{i}}$, we
apply height-preserving substitution $[z/y]$ for a fresh variable $z$ in the
conclusion of $\mathcal{D}$ and we obtain the following derivation:

$\Sigma,\Sigma^{\prime},(\Gamma_{i}\sigma)[z/x]\Rightarrow(\Delta_{i}\sigma)[z/x],\Theta^{\prime},\Theta\lx@proof@logical@and\Sigma^{\prime},(\Gamma_{i}\sigma)[z/x]\Rightarrow(\Delta_{i}\sigma)[z/x],\Theta^{\prime},\phi^{m}\phi^{n},\Sigma\Rightarrow\Theta.$

We can eliminate the last application of $\mathsf{Mcut}$ since the complexity
of the derivation is the same as $\texttt{c}(\mathcal{D})$ and the weight of
the derivation is smaller than $\texttt{w}(\mathcal{D})$. Finally we apply the
same rule $\mathcal{S}(R)$ to obtain the desired conclusion. When
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ be $\mathcal{S}(R)$, the argument is
similar to the case just discussed.

  4. (4)

Both $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ are logical rules for the same
logical connective and the cut formula is principal in each of the rules: We
have two cases, i.e., two cases where the cut formula is of the form
$\phi\to\psi$ or of the form $\forall x.\phi$. Here we only deal with the case
where the cut formula is of the form $\forall x.\phi$. Then the derivation
$\mathcal{D}$ is of the following form:

${\Gamma,\Sigma\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow\Delta,(\forall
x.\phi)^{m}\Gamma\Rightarrow\Delta,(\forall x.\phi)^{m-1},\phi[y/x](\forall
x.\phi)^{n},\Sigma\Rightarrow\Theta\phi[z/x],(\forall
x.\phi)^{n-1},\Sigma\Rightarrow\Theta.}$

With the help of our height-preserving substitution, we can consider a
multicut between $\mathcal{D}_{\texttt{L}}^{\prime}$ and
$\mathcal{D}_{\texttt{R}}$:

$\Gamma,\Sigma\Rightarrow\Delta,\Theta,\phi[z/x]\lx@proof@logical@and\Gamma\Rightarrow\Delta,(\forall
x.\phi)^{m-1},\phi[z/x](\forall x.\phi)^{n},\Sigma\Rightarrow\Theta,$

and then by induction hypothesis (the complexity of this derivation is the
same as $\mathcal{D}$ but the weight is smaller than the original
$\mathcal{D}$) we now know that
$\Gamma,\Sigma\Rightarrow\Delta,\Theta,\phi[z/x]$ is derivable in
$\mathcal{S}\mathcal{R}$ without multicuts by a derivation $\mathcal{E}_{1}$.
Let us also consider a multicut between $\mathcal{D}_{\texttt{L}}$ and
$\mathcal{D}_{\texttt{R}}^{\prime}$:

$\phi[z/x],\Gamma,\Sigma\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow\Delta,(\forall
x.\phi)^{m}\phi[z/x],(\forall x.\phi)^{n-1},\Sigma\Rightarrow\Theta,$

and then by induction hypothesis (the complexity of this derivation is the
same as $\mathcal{D}$ but the weight is smaller than the original
$\mathcal{D}$) we now know that
$\phi[z/x],\Gamma,\Sigma\Rightarrow\Delta,\Theta$ is derivable in
$\mathcal{S}\mathcal{R}$ without multicuts by a derivation $\mathcal{E}_{2}$.
Now let us take a cut between $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$:

$\Gamma,\Gamma,\Sigma,\Sigma\Rightarrow\Delta,\Delta,\Theta,\Theta\lx@proof@logical@and\Gamma,\Sigma\Rightarrow\Delta,\Theta,\phi[z/x]\phi[z/x],\Gamma,\Sigma\Rightarrow\Delta,\Theta$

and the conclusion of this derivation is derivable in $\mathcal{S}\mathcal{R}$
without multicuts by induction hypothesis because the complexity of this
derivation (i.e., the length of $\phi[z/x]$) is strictly smaller than
$\texttt{c}(\mathcal{D})$. Finally, finitely many applications of contraction
rules enables us to obtain the derivability of
$\Gamma,\Sigma\Rightarrow\Delta,\Theta$ in $\mathcal{S}\mathcal{R}$, as
desired.

  5. (5)

Both $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ are modal rules and the cut formula
is principal in each of the rules: Let
$\texttt{rule}(\mathcal{D}_{\texttt{L}})$ = $\mathcal{S}(R_{1})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ = $\mathcal{S}(R_{2})$ where we can
assume:

$R_{1}=\vbox{
$\heartsuit_{1}\vec{\boldsymbol{p}}_{1},\dots,\heartsuit_{a}\vec{\boldsymbol{p}}_{a}\Rightarrow\heartsuit_{a+1}\vec{\boldsymbol{q}}_{1},\dots,\heartsuit_{a+b}\vec{\boldsymbol{q}}_{b},(\heartsuit\vec{\boldsymbol{p}})^{n}\lx@proof@logical@and\Gamma_{11}\Rightarrow\Delta_{11}\cdots\Gamma_{1k}\Rightarrow\Delta_{1k}$},$
$R_{2}=\vbox{
$(\heartsuit\vec{\boldsymbol{p}})^{m},\spadesuit_{1}\vec{\boldsymbol{p}}_{1}^{\prime},\dots,\spadesuit_{c}\vec{\boldsymbol{p}}_{c}^{\prime}\Rightarrow\spadesuit_{c+1}\vec{\boldsymbol{q}}_{1}^{\prime},\dots,\spadesuit_{c+d}\vec{\boldsymbol{q}}_{d}^{\prime}\lx@proof@logical@and\Gamma_{21}\Rightarrow\Delta_{21}\cdots\Gamma_{2l}\Rightarrow\Delta_{2l}$
},$

because the cut formula is principal in both rules. In what follows, we assume
that all of $\vec{\boldsymbol{p}}_{i}$, $\vec{\boldsymbol{q}}_{j}$,
$\vec{\boldsymbol{p}}_{i}^{\prime}$, $\vec{\boldsymbol{q}}_{j}^{\prime}$ are
distinct. So $\mathcal{D}_{\texttt{L}}$ is of the following form:

$z\heartsuit_{a+1}\boldsymbol{\lceil
x_{a+1}\\!:\\!\phi_{a+1}\rceil},\dots,z\heartsuit_{a+b}\boldsymbol{\lceil
x_{a+b}\\!:\\!\phi_{a+b}\rceil},(z\heartsuit\boldsymbol{\lceil
x\\!:\\!\phi\rceil})^{m},\Theta_{1}\Sigma_{1},z\heartsuit_{1}\boldsymbol{\lceil
x_{1}\\!:\\!\phi_{1}\rceil},\dots,z\heartsuit_{a}\boldsymbol{\lceil
x_{a}\\!:\\!\phi_{a}\rceil}\Rightarrow\lx@proof@logical@and\Sigma_{1},\Gamma_{11}\sigma_{\boldsymbol{x}}^{y_{1}}\Rightarrow\Delta_{11}\sigma_{\boldsymbol{x}}^{y_{1}},\Theta_{1}\cdots\Sigma_{1},\Gamma_{1k}\sigma_{\boldsymbol{x}}^{y_{1}}\Rightarrow\Delta_{1k}\sigma_{\boldsymbol{x}}^{y_{1}},\Theta_{1}$

and $\mathcal{D}_{\texttt{R}}$ is of the following form:

$z\spadesuit_{c+1}\boldsymbol{\lceil
x_{c+1}\\!:\\!\psi_{c+1}\rceil},\dots,z\spadesuit_{c+d}\boldsymbol{\lceil
x_{c+d}\\!:\\!\psi_{c+d}\rceil},\Theta_{2}\Sigma_{2},(z\heartsuit\boldsymbol{\lceil
x\\!:\\!\phi\rceil})^{n},z\spadesuit_{1}\boldsymbol{\lceil
x_{1}\\!:\\!\psi_{1}\rceil},\dots,z\spadesuit_{c}\boldsymbol{\lceil
x_{c}\\!:\\!\psi_{c}\rceil}\Rightarrow\lx@proof@logical@and\Sigma_{2},\Gamma_{21}\tau_{\boldsymbol{x}}^{y_{2}}\Rightarrow\Delta_{21}\tau_{\boldsymbol{x}}^{y_{2}},\Theta_{2}\cdots\Sigma_{2},\Gamma_{2l}\tau_{\boldsymbol{x}}^{y_{2}}\Rightarrow\Delta_{2l}\tau_{\boldsymbol{x}}^{y_{2}},\Theta_{2}.$

We also note that the conclusion of $\mathcal{D}$ is:

$\displaystyle\Sigma_{1},\Sigma_{2},$
$\displaystyle\\{z\heartsuit_{i}\boldsymbol{\lceil
x_{i}\\!:\\!\phi_{i}\rceil}\\}_{1\leqslant i\leqslant
a},\\{z\spadesuit_{j}\boldsymbol{\lceil
x_{j}\\!:\\!\psi_{j}\rceil}\\}_{1\leqslant j\leqslant c}\Rightarrow$
$\displaystyle\quad\\{z\heartsuit_{a+i}\boldsymbol{\lceil
x_{a+i}\\!:\\!\phi_{a+i}\rceil}\\}_{1\leqslant i\leqslant
b},\\{z\spadesuit_{c+j}\boldsymbol{\lceil
x_{c+j}\\!:\\!\psi_{c+j}\rceil}\\}_{1\leqslant j\leqslant
d},\Theta_{1},\Theta_{2}.$

Let $y$ be a fresh variable not occurring in this conclusion. By height-
preserving substitution, we can obtain derivations
$\mathcal{D}^{\prime}_{\texttt{L}_{i}}[z/y_{1}]$ and
$\mathcal{D}^{\prime}_{\texttt{R}_{j}}[z/y_{2}]$ ($1\leqslant i\leqslant k$
and $1\leqslant j\leqslant l$). Since $\mathcal{R}$ absorbs multicut, we can
find a rule
$R=\Gamma_{1}\Rightarrow\Delta_{1},\cdots,\Gamma_{e}\Rightarrow\Delta_{e}/\Gamma_{R}\Rightarrow\Delta_{R}\in\mathcal{R}$
such that

     * ($\ast_{1}$)

$\mathsf{MCut}(\\{\Gamma_{1i}\Rightarrow\Delta_{1i}\\}_{1\leqslant i\leqslant
k},\\{\Gamma_{2j}\Rightarrow\Delta_{2j}\\}_{1\leqslant j\leqslant
l})\rhd\\{\Gamma_{1}\Rightarrow\Delta_{1},\ldots,\Gamma_{e}\Rightarrow\Delta_{e}\\}$
and

     * ($\ast_{2}$)

$\Gamma_{R}\Rightarrow\Delta_{R}\rhd\\{\heartsuit_{i}\vec{\boldsymbol{p}}_{i}\\}_{1\leqslant
i\leqslant
a},\\{\spadesuit_{j}\vec{\boldsymbol{p}}_{j}^{\prime}\\}_{1\leqslant
j\leqslant
c}\Rightarrow\\{\heartsuit_{a+i}\vec{\boldsymbol{q}}_{i}\\}_{1\leqslant
i\leqslant
b},\\{\spadesuit_{c+j}\vec{\boldsymbol{q}}_{j}^{\prime}\\}_{1\leqslant
j\leqslant d}$.

By the clause $(\ast_{1})$ and our derivations
$\mathcal{D}^{\prime}_{\texttt{L}_{i}}[z/y_{1}]$,
$\mathcal{D}^{\prime}_{\texttt{R}_{j}}[z/y_{2}]$, we now use the induction
hypothesis (the complexity is the same but the weight becomes smaller than
that of $\mathcal{D}$) and weakening rules to obtain the derivability in
$\mathcal{S}\mathcal{R}$ (without multicuts) of

$\Gamma_{i}\sigma\Rightarrow\Delta_{i}\sigma\quad(1\leqslant i\leqslant e)$

where $\sigma$ is a substitution which is the union of
$\sigma_{\boldsymbol{x}}^{y_{1}}$ and $\tau_{\boldsymbol{x}}^{y_{2}}$. It
follows from the rule $\mathcal{S}(R)$, the clause $(\ast_{2})$ and weakening
rules that the conclusion of $\mathcal{D}$ is derivable in
$\mathcal{S}\mathcal{R}$ without multicuts, as desired.

  6. (6)

One of $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ and
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is an equality rule: There are three
cases that we need to consider. In the first case,
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is $\mathsf{L=_{i}}$ where at least
one occurrence of the cut formulas is not principal in $\mathsf{L=_{i}}$ and
so the cut formula is of the form $x=y$. In the second case,
$\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is $\mathsf{L=_{i}}$ but all
occurrences of the cut formula are principal. In the third case,
$\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is $\mathsf{L=_{i}}$ and all
occurrences of the cut formula are principal. Since our argument for the third
case is almost similar to the one for the second case, we focus on the first
and the second cases in what follows.

Firstly, consider the case when $\texttt{rule}(\mathcal{D}_{\texttt{R}})$ is
$\mathsf{L=_{i}}$ and at least one occurrence of the cut formulas is not
principal in $\mathsf{L=_{i}}$. Without loss of generality, we assume that $i$
= 1. Then our derivation $\mathcal{D}$ is of the following form:

${\Gamma,\Sigma\Rightarrow\Delta,\Theta\lx@proof@logical@and\Gamma\Rightarrow\Delta,(x=y)^{m}x=y,\phi^{\prime}_{1}[y/w],\ldots,\phi^{\prime}_{n-1}[y/w],\Sigma^{\prime}[y/w]\Rightarrow\Theta^{\prime}[y/w]x=y,\phi^{\prime}_{1}[x/w],\ldots,\phi^{\prime}_{n-1}[x/w],\Sigma^{\prime}[x/w]\Rightarrow\Theta^{\prime}[x/w]}$

where $\Sigma^{\prime}[y/w]$ = $\Sigma$, $\Theta^{\prime}[y/w]$ = $\Theta$,
$\phi_{i}^{\prime}[y/w]$ is $x=y$ and so
$x=y,\phi^{\prime}_{1}[y/w],\ldots,\phi^{\prime}_{n-1}[y/w]$ is the same as
$(x=y)^{n}$. In this case we need to check what is the last rule
$\texttt{rule}(\mathcal{D}_{\texttt{L}})$. If
$\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is $\mathsf{Ax}$ (it cannot be
$\mathsf{L\bot}$), or a structural rule, or a logical or modal rule, we can
use the same argument in the items (1), (2), (3). If
$\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is an equality rule
$\mathsf{L=_{i}}$, then our argument is the same as in the second case below.
The remaining case is $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ is an axiom
$\mathsf{R=}$. Then our derivation above $\mathcal{D}$ has the following form:

${\Sigma\Rightarrow\Theta\lx@proof@logical@and\Rightarrow
x=xx=x,\phi^{\prime}_{1}[x/w],\ldots,\phi^{\prime}_{n-1}[x/w],\Sigma^{\prime}[x/w]\Rightarrow\Theta^{\prime}[x/w]x=x,\phi^{\prime}_{1}[x/w],\ldots,\phi^{\prime}_{n-1}[x/w],\Sigma^{\prime}[x/w]\Rightarrow\Theta^{\prime}[x/w].}$

Then this derivation is transformed into:

$\Sigma\Rightarrow\Theta\lx@proof@logical@and\Rightarrow
x=xx=x,\phi^{\prime}_{1}[x/w],\ldots,\phi^{\prime}_{n-1}[x/w],\Sigma^{\prime}[x/w]\Rightarrow\Theta^{\prime}[x/w]$

and this last application of multicut is eliminable since the complexity is
the same as that of $\mathcal{D}$ but the weight becomes smaller.

Secondly, let $\texttt{rule}(\mathcal{D}_{\texttt{L}})$ be $\mathsf{L=_{i}}$
and assume that all occurrences of the cut formula are principal. In this case
the derivation $\mathcal{D}$ is of the following form:

${x=y,\Gamma^{\prime},\Sigma\Rightarrow\Delta,\Theta\lx@proof@logical@and
x=y,\Gamma^{\prime\prime}[y/w]\Rightarrow\Delta^{\prime\prime}[y/w],\phi_{1}^{\prime}[y/w],\ldots,\phi_{m}^{\prime}[y/w]x=y,\Gamma^{\prime\prime}[x/w]\Rightarrow\Delta^{\prime\prime}[x/w],\phi_{1}^{\prime}[x/w],\ldots,\phi_{m}^{\prime}[x/w]\phi^{n},\Sigma\Rightarrow\Theta}$

where $\Gamma^{\prime\prime}[y/w]$ = $\Gamma^{\prime}$, $\Delta^{\prime}[y/w]$
= $\Delta$ and $\phi_{i}^{\prime}[y/w]$ = $\phi$ ($1\leqslant i\leqslant m$).
Before transforming this derivation into a multicut-free derivation, we remark
that $\phi_{i}^{\prime}[x/w][y/x]$ = $\phi_{i}^{\prime}[y/w][y/x]$ =
$\phi[y/x]$, $\Gamma^{\prime\prime}[x/w][y/x]$ =
$\Gamma^{\prime\prime}[y/w][y/x]$ = $\Gamma^{\prime}[y/x]$,
$\Delta^{\prime}[x/w][y/x]$ = $\Delta^{\prime}[y/w][y/x]$ = $\Delta[y/x]$.
With the help of this remark, the derivation $\mathcal{D}$ is transformed
into:

$x=y,\Gamma^{\prime},\Sigma\Rightarrow\Delta,\Theta
x=y,x=y,\Gamma^{\prime},\Sigma\Rightarrow\Delta,\Theta
x=y,y=y,\Gamma^{\prime}[y/x],\Sigma[y/x]\Rightarrow\Delta[y/x],\Theta[y/x]y=y,\Gamma^{\prime}[y/x],\Sigma[y/x]\Rightarrow\Delta[y/x],\Theta[y/x]\lx@proof@logical@and
y=y,\Gamma^{\prime}[y/x]\Rightarrow\Delta[y/x],(\phi[y/x])^{m}(\phi[y/x])^{n},\Sigma[y/x]\Rightarrow\Theta[y/x]$

where we note that the first application of multicut is eliminable since the
complexity is the same as that of $\mathcal{D}$ but the weight is smaller than
that of $\mathcal{D}$ by height-preserving substitution $[y/x]$.

######  Theorem 61 (Cut Elimination).

Suppose that $\mathcal{R}$ absorbs multicut. Then the rule $\mathsf{Mcut}$ is
admissible in $\mathcal{S}\mathcal{R}$. Therefore, $\mathsf{Cut}$ is also
admissible in $\mathcal{S}\mathcal{R}$.

######  Proof 6.10.

Suppose that a sequent is derivable in the system $\mathcal{S}\mathcal{R}$
extended with $\mathsf{MCut}$. Let $\mathcal{E}$ be such a derivation. Then we
focus on one of the topmost applications of $\mathsf{MCut}$ to show that such
application of $\mathsf{MCut}$ is eliminable, i.e., we show that the
derivation whose last applied rule is such multicut can be replaced with a
multicut-free derivation of $\mathcal{S}\mathcal{R}$. This is done using Lemma
60. Once we eliminate one of the topmost applications of $\mathsf{MCut}$, we
repeat the same argument for the remaining topmost applications with the help
of Lemma 60 to get rid of all applications of $\mathsf{MCut}$ in the original
derivation $\mathcal{E}$.

In what follows, we introduce the notion of _absorption of contraction and
cut_ and show that jointly they provide a sufficient condition of absorption
of multicut.

Let $\mathbb{S}$ be a finite set of sequents. The set of sequents that can be
derived from premises $\mathbb{S}$ using (only) the _contraction rules_ is
denoted by $\mathsf{Con}(\mathbb{S})$. Similarly, the set of all sequents that
can be derived from premises in $\mathbb{S}$ using (only) one application of
the _cut rule_ is denoted by $\mathsf{Cut}(\mathbb{S})$. A rule set
$\mathcal{R}$ _absorbs contraction_ if, for all rules $R$ =
$\Gamma_{1}\Rightarrow\Delta_{1},\cdots,\Gamma_{k}\Rightarrow\Delta_{k}/\Gamma_{R}\Rightarrow\Delta_{R}\in\mathcal{R}$
and all
$\Gamma^{\prime}\Rightarrow\Delta^{\prime}\in\mathsf{Con}(\Gamma_{R}\Rightarrow\Delta_{R})$
there exists a rule
$S=\Sigma_{1}\Rightarrow\Theta_{1},\cdots,\Sigma_{l}\Rightarrow\Theta_{l}/\Gamma_{S}\Rightarrow\Delta_{S}\in\mathcal{R}$
such that

$\mathsf{Con}(\\{\Gamma_{1}\Rightarrow\Delta_{1},\ldots,\Gamma_{k}\Rightarrow\Delta_{k}\\})\rhd\\{\Sigma_{1}\Rightarrow\Theta_{1},\ldots,\Sigma_{l}\Rightarrow\Theta_{l}\\}$

and
$\Gamma_{S}\Rightarrow\Delta_{S}\rhd\Gamma^{\prime}\Rightarrow\Delta^{\prime}$.
A rule set $\mathcal{R}$ _absorbs cut_ , if for all pairs $(R_{1},R_{2})$ of
rules in $\mathcal{R}$:

$\Gamma_{R_{1}}\Rightarrow\Delta_{R_{1}},\heartsuit\vec{\boldsymbol{p}}\lx@proof@logical@and\Gamma_{11}\Rightarrow\Delta_{11}\cdots\Gamma_{1r_{1}}\Rightarrow\Delta_{1r_{1}}\quad\heartsuit\vec{\boldsymbol{p}},\Gamma_{R_{2}}\Rightarrow\Delta_{R_{2}}\lx@proof@logical@and\Gamma_{21}\Rightarrow\Delta_{21}\cdots\Gamma_{2r_{2}}\Rightarrow\Delta_{2r_{2}}$

there is a rule $R$ =
$\Gamma_{1}\Rightarrow\Delta_{1},\cdots,\Gamma_{k}\Rightarrow\Delta_{k}/\Gamma_{R}\Rightarrow\Delta_{R}\in\mathcal{R}$
such that:

$\mathsf{Cut}(\Gamma_{11}\Rightarrow\Delta_{11},\ldots,\Gamma_{1r_{1}}\Rightarrow\Delta_{1r_{1}},\Gamma_{21}\Rightarrow\Delta_{21},\ldots,\Gamma_{2r_{2}}\Rightarrow\Delta_{2r_{2}})\rhd\\{\Gamma_{1}\Rightarrow\Delta_{1},\ldots,\Gamma_{k}\Rightarrow\Delta_{k}\\}$

and
$\Gamma_{R}\Rightarrow\Delta_{R}\rhd\Gamma_{R_{1}},\Gamma_{R_{2}}\Rightarrow\Delta_{R_{1}},\Delta_{R_{2}}$.

Informally, absorption of cut and contraction of a rule set allows us to
replace an application of cut or contraction to the conclusions of rules in
$\mathcal{R}$ by a possibly different rule with possibly weaker premises and
stronger conclusion. While these definitions are purely syntactic, a semantic
characterisation has been given in [PattinsonSchroder10] in terms of _one-step
cut-free completeness_. For many $\Lambda$-structures including those for the
modal logic $K$ and the logic of (monotone) neighbourhood frames, one-step
cut-free complete rule sets are known. In particular, these rule sets satisfy
absorption of cut, contraction and congruence [PattinsonSchroder10, § 5].

######  Lemma 62.

If the rule set $\mathcal{R}$ absorbs contraction and cut then $\mathcal{R}$
also absorbs multicut.

By Theorem 61 and Lemma 62, we obtain the following.

######  Corollary 63.

Suppose that $\mathcal{R}$ absorbs contraction and cut. Then $\mathsf{Cut}$ is
also admissible in $\mathcal{S}\mathcal{R}$.

As an immediate corollary, we obtain completeness of the cut-free calculus
assuming that $\mathcal{R}$ is _strongly_ one-step complete:

######  Corollary 64.

Suppose that $\mathcal{R}$ is strongly one-step complete. Then
$\models\Gamma\Rightarrow\Delta$ iff
$\mathcal{S}\mathcal{R}\vdash\Gamma\Rightarrow\Delta$.

######  Proof 6.11.

This follows from Theorem 61 with the help of Proposition 5.11 and 5.12 of
[PattinsonSchroder10], the latter asserting precisely the absorption of cut
and congruence.

The situation is more complex in presence of bounded operators where
completeness of the Hilbert calculus is only guaranteed in presence of