#  Deducibility in the full Lambek calculus with weakening is HAck-complete

Vitor Greati  Revantha Ramanayake111The financial support of the CogniGron
research center, the Ubbo Emmius Funds (University of Groningen), and FWF
project P33548 is acknowledged.

###### Abstract

We show that the problem of deciding the consequence relation (deducibility)
for the full Lambek calculus with weakening ($\mathbf{FL}_{\mathbf{w}}$) is
complete for the class HAck of hyper-Ackermannian problems (i.e.,
$\mathbf{F}_{\omega^{\omega}}$ in the ordinal-indexed hierarchy of fast-
growing complexity classes). Provability was already known to be PSpace-
complete. We prove that deducibility is HAck-complete even for the
multiplicative fragment. Lower bounds are obtained via a novel reduction from
reachability in lossy channel systems. Upper bounds are obtained via
structural proof theory (forward proof search over sequent calculi) and well-
quasi-order theory (length theorems for Higman’s ordering on words over a
finite alphabet).

###### keywords:

substructural logics , hyper-Ackermannian problems , Lambek calculus ,
Higman’s Lemma , well-quasi-order theory , sequent calculi

††journal: arXiv

defn[thm]Definition theoremapx[thm]Theorem propositionapx[thm]Proposition
lemmaapx[thm]Lemma corollaryapx[thm]Corollary remarkapx[thm]Remark

[inst1]organization=Bernoulli Institute, University of Groningen,
country=Nijenborgh 4, NL-9747 AG Groningen, Netherlands

[inst2]organization=CogniGron, University of Groningen, country=Nijenborgh 4,
NL-9747 AG Groningen, Netherlands

##  1 Introduction

Substructural logics are obtained from intuitionistic and classical logic by
removing familiar structural properties like exchange (e), contraction (c) and
weakening (w), and extending with further axioms and language connectives. A
prominent example is the family of _linear logics_ where a propositional
substructural base is extended with modalities (“exponentials”) for weakening
and contraction. The absence of structural properties leads to highly
expressive and complex logics, and this is evident even in the most
fundamental of substructural logics (see Table 1), namely the extensions of
the full Lambek calculus $\mathbf{FL}$ by subsets of
$\\{\mathrm{(e),(c),(w)}\\}$. A significant gap in this table persisted at
$\mathbf{FL}_{\mathbf{w}}$ since the deducibility problem (provability of a
formula from a finite set of formulas) was, thus far, only known to be
decidable, a result obtained by Blok and van Alten [blokalten2005] via the
finite embeddability property for $\mathsf{FL_{\mathsf{w}}}$-algebras, the
algebraic semantics of $\mathbf{FL}_{\mathbf{w}}{}$. We fill this gap by
establishing completeness with respect to the fast-growing hyper-Ackermannian
complexity class HAck, placing $\mathbf{FL}_{\mathbf{w}}$ as the hardest for
deducibility among the decidable basic substructural logics (taking the crown
from $\mathbf{FL}_{\mathbf{e}\mathbf{c}}{}$, where deducibility has
Ackermannian complexity). Let $\mathbf{FL}_{\mathbf{w}}^{\Sigma}$ denote the
restriction of $\mathbf{FL}_{\mathbf{w}}$ to connectives in $\Sigma$.

[Main theorem] For
$\\{\otimes,{\setminus},0,1\\}\subseteq\Sigma\subseteq\Sigma_{\mathbf{FL}}$,
deducibility in $\mathbf{FL}_{\mathbf{w}}^{\Sigma}$ is HAck-complete. In
particular, $\mathbf{FL}_{\mathbf{w}}{}$ and its multiplicative fragment
$\mathbf{L}_{\mathbf{w}}{}$ are HAck-complete.

Logic | Deducibility | Provability
---|---|---
$\mathbf{FL}{}$ |  Undecidable [Jipsen2002] |  PSpace-complete [horcik2011]
$\mathbf{FL}_{\mathbf{e}}{}$ |  Undecidable [lincoln1992] |  PSpace-complete [horcik2011]
$\mathbf{FL}_{\mathbf{e}\mathbf{c}}{}$ |  Ack-complete [urquhart1999] |  Ack-complete [urquhart1999]
$\mathbf{L}_{\mathbf{e}\mathbf{c}}$ |  2-ExpTime-complete [schmitz2011] |  2-ExpTime-complete [schmitz2011]
$\mathbf{FL}_{\mathbf{e}\mathbf{w}}{}$ |  Tower-complete [tanaka2022] |  PSpace-complete [horcik2011]
$\mathbf{FL}_{\mathbf{c}}{}$ |  Undecidable [horcik2016] |  Undecidable [horcik2016]
$\mathbf{FL}_{\mathbf{w}}{}$ |  Decidable [blokalten2005]. Complexity: this paper |  PSpace-complete [horcik2011]
$\mathbf{L}_{\mathbf{w}}{}$ |  Decidable [galatosono2010]. Complexity: this paper |  PSpace [horcik2011]
Table 1: The computational status of the basic substructural logics.

The above statement references Schmitz’s ordinal-indexed _fast-growing
complexity classes_ $\\{\mathbf{F}_{\alpha}\\}_{\alpha}$ [schmitz2016hierar].
Important members of this family are $\mathbf{F}_{2}$, problems solvable in
time expressed by an elementary function (such as polynomial and exponential);
$\mathbf{F}_{3}$, the first class of non-elementary problems, known as Tower;
$\mathbf{F}_{\omega}$, the first class of non-primitive recursive problems,
known as Ack (short for ‘Ackermann’); and $\mathbf{F}_{\omega^{\omega}}$, the
first class of non-multiply recursive problems. The complexity of the latter
cannot be expressed by a function defined by multiple nested recursion
[roszapeter1967, §10], and it is known as HAck (‘hyper-Ackermann’).

#### An overview of the lower bound argument

Inspired by Urquhart’s [urquhart1999] lower bound for
$\mathbf{FL}_{\mathbf{e}\mathbf{c}}{}$ where _acceptance_ for expansive
additive counter machines is reduced to deducibility, we reduce _reachability_
for _lossy channel systems_ (LCS) to deducibility in
$\mathbf{FL}_{\mathbf{w}}{}$.

An LCS is a computational model whose configurations are tuples
$(q,u_{1},\ldots,u_{n})$ where $q$ is the state and $u_{k}$ is the
$k^{\text{th}}$ channel’s contents i.e., some word over a finite alphabet
$\mathtt{M}$. Its instructions take the following form: _read_ letter
$\mathtt{a}$ from the front of channel $k$ in state $q_{i}$, remove it and
transit to state $q_{j}$; _write_ letter $\mathtt{a}$ to the back of channel
$k$ in state $q_{i}$ and transit to state $q_{j}$; perform a _lossy_ step by
deleting some letters from any channel (the state remains unchanged). Chambart
and Schnoebelen [chambart2008] show that deciding reachability of a
configuration $v$ from a configuration $u$ is HAck-complete.

We code the set $\mathtt{I}$ of instructions of an LCS $\mathcal{L}$ as a
finite set $\mathcal{T}(\mathcal{L})$ of sequents, and simulate read and write
instructions by cuts with these sequents, and lossy steps by left weakening.
For instance, reachability of $(q_{2},\mathtt{a},\mathtt{b})$ from
$(q_{1},\mathtt{a}\mathtt{a},\mathtt{b})$ in $\mathcal{L}$ is coded as
deducibility of the following sequent from $\mathcal{T}(\mathcal{L})$:

${Q_{1},\\#^{s}_{1},A,A,\\#^{e}_{1},\\#^{s}_{2},B,\\#^{e}_{2}}\Rightarrow{Q_{2}\otimes(\\#^{s}_{1}\otimes(A\otimes(\\#^{e}_{1}\otimes(\\#^{s}_{2}\otimes(B\otimes\\#^{e}_{2})))))}$

Reading upwards from the endsequent, the following deduction in
$\mathbf{FL}_{\mathbf{w}}{}$ simulates an instruction
$(q_{i},c_{1},\mathtt{a},?,q_{j})\in\mathtt{I}$; i.e., read $\mathtt{a}$ from
the front of channel $c_{1}$ in state $q_{i}$, remove it, then transit to
$q_{j}$.

sequent in $\mathcal{T}(\mathcal{L})$ coding instruction
${Q_{i},\\#^{s}_{1},A}\Rightarrow{Q_{j}\otimes\\#^{s}_{1}}$ $\cdots$
${Q_{j},\\#^{s}_{1},B,C,\\#^{e}_{1}}\Rightarrow{v}$ $\mathrm{({L}{\otimes})}$
${Q_{j}\otimes\\#^{s}_{1},B,C,\\#^{e}_{1}}\Rightarrow{v}$ (cut)
${Q_{i},\\#^{s}_{1},A,B,C,\\#^{e}_{1}}\Rightarrow{v}$

Every computation in the LCS is shown to correspond to a deduction of its
reachability encoding. The converse direction is far more challenging,
requiring a careful analysis of deductions in $\mathbf{FL}_{\mathbf{w}}{}$.
The starting point is a cut-elimination style argument that establishes a
normal form (of “standard deductions”) where the left premise of every cut is
an element of the theory. The computation is read off the standard deduction,
starting at the endsequent.

#### The upper bound argument

We define a forward proof procedure extending the construction in
Balasubramanian et al. [BalLanRam21LICS]. The idea is to start from the set
$D_{0}$ of initial sequent instances and form an increasing chain
$D_{0}\subset D_{1}\subset\ldots$ of finite sets of deducible sequents (each
step corresponds to limited weakening and then a single rule application),
taking care that each $D_{i}$ contains only minimal elements under the Higman
ordering on words (omit words that can be obtained from another by inserting
letters); the ordering is a well-quasi-order (wqo) [higman1952] so the chain
must be finite. By construction, the bad sequence underlying the chain is
controlled (no element in $D_{i+1}$ is much larger than some element in
$D_{i}$), and the complexity is dominated by the maximum length of a
controlled bad sequence. This is a function in HAck as shown by Schmitz and
Schnoebelen [schmitz2011]. The argument applies to infinitely-many structural
rule extensions of $\mathbf{FL}_{\mathbf{w}}{}$.

#### Contributions

We show that (1) sequent-deducibility in fragments of
$\mathbf{FL}_{\mathbf{w}}$ containing $\otimes$ is HAck-hard and that (2)
deducibility for any $\mathcal{N}_{2}$-analytic structural rule extension
[CiaGalTer17] of any fragment of $\mathbf{FL}_{\mathbf{w}}$ is in HAck. Our
main theorem follows from (1) and (2). Algebraizability of
$\mathbf{FL}_{\mathbf{w}}$ implies that (3) the word problem and the
quasiequational theory of the variety of integral zero-bounded full Lambek
algebras are HAck-complete.

##  2 Noncommutative substructural logics with weakening

Let $\Sigma$ be a propositional signature and fix a countable set
$\mathcal{P}$ of _propositional variables_. Let
$\mathrm{Fm}_{\Sigma}(\mathcal{P})$ denote the set of _formulas_ over $\Sigma$
generated by $\mathcal{P}$. We consider subsignatures of
$\Sigma_{\mathbf{FL}}:=\\{0,1,\top,\bot,\otimes,\land,\lor,{/},{\setminus}\\}$,
where $0,1,\top$ and $\bot$ are constants and the other connectives are
binary. A subsignature is specified as
$\Sigma_{\mathbf{FL}}^{\star_{1}\cdots\star_{k}}:=\\{\star_{1},\ldots,\star_{k}\\}\subseteq\Sigma_{\mathbf{FL}}$.
For example,
$\Sigma_{\mathbf{FL}}^{\otimes{\setminus}}=\\{\otimes,{\setminus}\\}$.
Sequences (or lists) of formulas will be written without delimiters, with
commas separating the formulas. We write
$\bigotimes{\varphi_{1},\ldots,\varphi_{m}}$ as abbreviation for
$\varphi_{1}\otimes(\varphi_{2}\otimes(\ldots(\varphi_{m-1}\otimes\varphi_{m})\ldots))$,
where $m\geq 1$ and $\varphi_{1},\ldots,\varphi_{m}$ is a list of formulas. If
the constant $1$ is present in the language, we allow $m=0$ (empty fusion),
the result being $1$.

A _sequent over $\mathrm{Fm}_{\Sigma}(\mathcal{P})$_ is an expression
${\Gamma}\Rightarrow{\Pi}$, where $\Gamma$ is a finite sequence of formulas
and $\Pi$ is an empty sequence or a sequence with a single formula. Given a
set $\mathcal{T}$ of sequents, let $\mathsf{subf}(\mathcal{T})$ denote the set
of subformulas of the formulas appearing in it. We assume familiarity with the
sequent calculus (see e.g., [GalJipKowOno07, Sec. 2.1.3]): a _sequent calculus
$\mathbf{S}$ over $\mathrm{Fm}_{\Sigma}(\mathcal{P})$_ is a collection of
schematic sequent rules. _Instantiations_ of their schematic variables lead to
_rule instances_. _Derivations_ in $\mathbf{S}$ are finite rooted trees
labelled with sequents over $\mathrm{Fm}_{\Sigma}(\mathcal{P})$ such that a
node and its children are the conclusion and premises of a rule instance. For
a finite set $\mathcal{T}$ of sequents, a _$\mathcal{T}$ -deduction_ in
$\mathbf{S}$ is a derivation in which every leaf is a rule with no premises
(_axiom_ or _initial sequent_) or a sequent in $\mathcal{T}$. A _proof_ in
$\mathbf{S}$ is a $\varnothing$-deduction in $\mathbf{S}$. Any
$\mathbf{S}^{\prime}\subseteq\mathbf{S}$ is called a _subcalculus_ of
$\mathbf{S}$, and any $\mathbf{S}^{\prime\prime}\supseteq\mathbf{S}$ is a
_rule extension_ of $\mathbf{S}$. _Structural rule extensions_ are extensions
by _structural rules_ (rules without logical connectives).

Subcalculi of the sequent calculus $\mathbf{FL}_{\mathbf{w}}$ displayed in
Fig. 1 (_full Lambek calculus with weakening_) are induced by a subsignature
of $\Sigma_{\mathbf{FL}}$ as follows. Let
$\mathbf{FL}_{\mathbf{w}}^{\star_{1}\cdots\star_{k}}$ be the sequent calculus
consisting of rules that mention no connective (i.e., rule $\mathrm{(id)}$ and
structural rules), or that mentions a connective in
$\\{\star_{1},\ldots,\star_{k}\\}$. For instance,
$\mathbf{FL}_{\mathbf{w}}^{\otimes{\setminus}}$ is the calculus over
$\mathrm{Fm}_{\Sigma_{\mathbf{FL}}^{\otimes{\setminus}}}(\mathcal{P})$
consisting of the axioms, all structural rules and the rules mentioning
$\otimes$ and ${\setminus}$.

A sequent calculus $\mathbf{S}$ over $\mathrm{Fm}_{\Sigma}(\mathcal{P})$
canonically determines two _consequence relations_ , one over sequents and
another over formulas. The _sequent-deduction relation_
$\vdash_{{\mathbf{S}}\mathsf{\Rightarrow}}$ is such that, for all finite sets
$\mathcal{T}\cup\\{s\\}$ of sequents over $\mathrm{Fm}_{\Sigma}(\mathcal{P})$,
$\mathcal{T}\vdash_{{\mathbf{S}}\mathsf{\Rightarrow}}s$ iff there is a
$\mathcal{T}$-deduction of $s$ in $\mathbf{S}$. The _formula-deduction
relation_ $\vdash_{\mathbf{S}}$ is such that, for all finite sets
$G\cup\\{\varphi\\}$ of formulas over $\mathrm{Fm}_{\Sigma}(\mathcal{P})$,
$G\vdash_{\mathbf{S}}\varphi$ iff there is a
$\\{{}\Rightarrow{\psi}\mid\psi\in G\\}$-deduction of ${}\Rightarrow{\varphi}$
in $\mathbf{S}$. Given a sequent calculus $\mathbf{S}$, the problem of
deciding $\vdash_{{\mathbf{S}}\mathsf{\Rightarrow}}$ is called _sequent-
deducibility_ and the problem of deciding $\vdash_{\mathbf{S}}$ is called
_formula-deducibility_ or simply _deducibility_. We know that
$\vdash_{\mathbf{FL}_{\mathbf{w}}}$ is the consequence relation of the full
Lambek logic with weakening (see [GalJipKowOno07, 2.1.4] for the Hilbert-
calculus presentation and residuated lattices semantics of these logics). The
reader is also referred to [GalJipKowOno07, 2.1.4] for the notion of
_axiomatic extensions_ of $\vdash_{\mathbf{FL}_{\mathbf{w}}}$.

The following lemma says that $\vdash_{{\mathbf{S}}\mathsf{\Rightarrow}}$
reduces to $\vdash_{\mathbf{S}}$ when $\mathbf{S}$ is a subcalculus of
$\mathbf{FL}_{\mathbf{w}}$ containing the rules for $\otimes,{\setminus},0$
and $1$. For that, consider the translation ${(\cdot)}^{\to}$ of sequents over
$\mathrm{Fm}_{\Sigma}(\mathcal{P})$ into formulas over
$\mathrm{Fm}_{\Sigma\cup\\{0,1,\otimes,{\setminus}\\}}(\mathcal{P})$ defined
${({\Gamma}\Rightarrow{\Pi})}^{\to}:=\bigotimes\Gamma{\setminus}\Pi^{\star}$,
where $\Pi^{\star}$ is $\varphi$ if $\Pi=\varphi$ and $0$ if $\Pi$ is empty.

Let $\Sigma\supseteq\\{\otimes,{\setminus},0,1\\}$ and
$\mathbf{S}:=\mathbf{FL}_{\mathbf{w}}^{\Sigma}$. For all finite sets of
sequents $\mathcal{T}$ and sequents $s$ over the language of $\mathbf{S}$,
$\mathcal{T}\vdash_{{\mathbf{S}}\mathsf{\Rightarrow}}s\text{ iff
}\\{{t}^{\to}\mid t\in\mathcal{T}\\}\vdash_{\mathbf{S}}{s}^{\to}.$

###### Proof.

From left to right, let $\delta$ be a deduction witnessing
$\mathcal{T}\vdash_{{\mathbf{S}}\mathsf{\Rightarrow}}s$. We show how to
convert $\delta$ into a witness of $\\{{t}^{\to}\mid
t\in\mathcal{T}\\}\vdash_{\mathbf{S}}{s}^{\to}$ by structural induction. In
the base case, $s$ is either the result of an axiomatic rule or an element of
$\mathcal{T}$. To translate $t\in\mathcal{T}$ into ${t}^{\to}$, repeatedly use
the rules $\mathrm{({L}{\otimes})}$ and $\mathrm{({R}{{\setminus}})}$, and
$\mathrm{({L}{1})}$ and $\mathrm{({R}{0})}$ if required. In the inductive
step, assume ${\Gamma}\Rightarrow{\Pi}$ was derived by an application of a
$k$-ary rule $\mathsf{r}$, whose premises are the sequents
${\Gamma_{1}}\Rightarrow{\Pi_{1}},\ldots,{\Gamma_{k}}\Rightarrow{\Pi_{k}}$.
Note first that the rule  ${}\Rightarrow{\bigotimes\Gamma{\setminus}\Pi}$ (FS)
${\Gamma}\Rightarrow{\Pi}$ is derivable in presence of cut. By IH, the
sequents
${}\Rightarrow{\bigotimes\Gamma_{1}{\setminus}\Pi_{1}^{\star}},\ldots,{}\Rightarrow{\bigotimes\Gamma_{k}{\setminus}\Pi_{k}^{\star}}$
are provable from $\mathcal{T}^{\to}$. Apply to these premises the derived
rule $\mathrm{(FS)}$ thus obtaining the premises
${\Gamma_{1}}\Rightarrow{\Pi_{1}^{\star}},\ldots,{\Gamma_{k}}\Rightarrow{\Pi_{k}^{\star}}$
(maybe cuts with ${}\Rightarrow{1}$ will be necessary to recover empty
antecedents). Use cuts with ${0}\Rightarrow{}$ whenever necessary to obtain
from those the premises
${\Gamma_{1}}\Rightarrow{\Pi_{1}},\ldots,{\Gamma_{k}}\Rightarrow{\Pi_{k}}$.
Apply the same rule $\mathsf{r}$ to the latter, obtaining
${\Gamma}\Rightarrow{\Pi}$, from which
${}\Rightarrow{\bigotimes\Gamma{\setminus}\Pi^{\star}}$ is easily derivable
(if $\Gamma$ is empty, use $\mathrm{({L}{1})}$), and we are done.

From right to left, first transform all the leaves with translated sequents
from $\mathcal{T}$ into trees with leaves being either instances of axioms or
the sequents themselves. This is easy to do using rules
$\mathrm{({R}{{\setminus}})}$, $\mathrm{({L}{\otimes})}$, $\mathrm{({L}{1})}$
and $\mathrm{({R}{0})}$. Then it is enough to transform the root ${s}^{\to}$
into $s$ using $\mathrm{(FS)}$ as we did in the converse direction. ∎

(id) ${p}\Rightarrow{p}$ |  $\mathrm{({R}{1})}$ ${}\Rightarrow{1}$
---|---

${\Gamma,\Delta}\Rightarrow{\Pi}$ $\mathrm{(lw)}$ ${\Gamma,\varphi,\Delta}\Rightarrow{\Pi}$ |  ${\Theta}\Rightarrow{\varphi}$ ${\Gamma,\varphi,\Delta}\Rightarrow{\Pi}$ (cut) ${\Gamma,\Theta,\Delta}\Rightarrow{\Pi}$
---|---

${\Gamma}\Rightarrow{}$ $\mathrm{({R}{0})}$ ${\Gamma}\Rightarrow{0}$ |  ${\Gamma,\varphi,\psi,\Delta}\Rightarrow{\Pi}$ $\mathrm{({L}{\otimes})}$ ${\Gamma,\varphi\otimes\psi,\Delta}\Rightarrow{\Pi}$
---|---

${\Gamma}\Rightarrow{\varphi}$ ${\Delta}\Rightarrow{\psi}$ $\mathrm{({R}{\otimes})}$ ${\Gamma,\Delta}\Rightarrow{\varphi\otimes\psi}$ |  ${\Gamma}\Rightarrow{\varphi_{i}}$ $\mathrm{({R}{\lor})}$ ${\Gamma}\Rightarrow{\varphi_{1}\lor\varphi_{2}}$
---|---

${\Gamma,\varphi_{i},\Delta}\Rightarrow{\Pi}$ $\mathrm{({L}{\land})}$ ${\Gamma,\varphi_{1}\land\varphi_{2},\Delta}\Rightarrow{\Pi}$ |  ${\Gamma}\Rightarrow{\varphi}$ ${\Delta,\psi,\Theta}\Rightarrow{\Pi}$ $\mathrm{({L}{{/}})}$ ${\Delta,\psi{/}\varphi,\Gamma,\Theta}\Rightarrow{\Pi}$
---|---

${\Gamma,\varphi}\Rightarrow{\psi}$ $\mathrm{({R}{{/}})}$ ${\Gamma}\Rightarrow{\psi{/}\varphi}$ |  ${\varphi,\Gamma}\Rightarrow{\psi}$ $\mathrm{({R}{{\setminus}})}$ ${\Gamma}\Rightarrow{\varphi{\setminus}\psi}$
---|---

Figure 1: The sequent calculus $\mathbf{FL}_{\mathbf{w}}$.

Every $\varnothing$-deduction (i.e., every proof) in
$\mathbf{FL}_{\mathbf{w}}^{\Sigma}$ can be converted to a proof without cuts
(by cut elimination [GalJipKowOno07, 4.1.1]), so these calculi satisfy the
_subformula property_ (every formula that occurs in the proof is a subformula
of the endsequent). However, not all cuts can be eliminated from a
$\mathcal{T}$-deduction. Still, for suitable $\mathcal{T}$ identified below,
the applications of cut can be restricted to obtain a generalized subformula
property.

A sequent is said to be _regular_ if its antecedent contains only
propositional variables and the succedent is not empty. A _regular theory_ is
a finite collection of regular sequents. For a regular theory $\mathcal{T}$, a
_standard cut_ (over $\mathcal{T}$) has as left premise a leaf that is a
sequent from $\mathcal{T}$. A _standard deduction_ (from $\mathcal{T}$) is one
in which all cuts are standard. We write
$\mathcal{T}\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\Sigma}}\mathsf{\Rightarrow}}^{\mathsf{std}}{\Gamma}\Rightarrow{\varphi}$
to denote that ${\Gamma}\Rightarrow{\varphi}$ has a standard deduction from
$\mathcal{T}$ in $\mathbf{FL}_{\mathbf{w}}^{\Sigma}$.

Let $\Sigma\subseteq\Sigma_{\mathbf{FL}}$. For a regular theory $\mathcal{T}$
and sequent $s$,
$\mathcal{T}\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\Sigma}}\mathsf{\Rightarrow}}s$
iff
$\mathcal{T}\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\Sigma}}\mathsf{\Rightarrow}}^{\mathsf{std}}s$.
Moreover, every formula in a standard deduction in
$\mathbf{FL}_{\mathbf{w}}^{\Sigma}$ is in
$\mathsf{subf}(\mathcal{T}\cup\\{s\\})$.

###### Proof.

We establish the claim for $\Sigma=\Sigma_{\mathbf{FL}}$. The reader will
observe that removing rules means less cases to be checked, and thus the
argument here applies to any $\Sigma\subseteq\Sigma_{\mathbf{FL}}$. Let us
call the instantiation of the schematic-variable $\varphi$ in an instance of
the $\mathrm{(cut)}$ rule (cf. Fig. 1) as the _cut formula_ of that
instantiation.

For first assertion, the argument is based on the usual cut-elimination
procedure for $\mathbf{FL}_{\mathbf{w}}$ [GalJipKowOno07, 4.1.1]; the
difference is that we now have to deal with cuts with a premise in
$\mathcal{T}$. We repeatedly eliminate topmost non-standard cuts, by primary
induction on the grade of the cut (the length of the cut formula), and
secondary induction on the cut-height (the sum of the number of sequents
appearing in the proofs of the premises of the cut).

Consider a topmost non-standard cut with cut-height $2$ (note that $<2$ is not
possible). The premises of the cut are instances of axiomatic rules or
elements from $\mathcal{T}$. If no element from $\mathcal{T}$ appears as a
premise, the cut is eliminated in the usual way as for
$\mathbf{FL}_{\mathbf{w}}$. If the left premise is from $\mathcal{T}$, nothing
needs to be done since we admit standard cuts. If the right premise is from
$\mathcal{T}$, the left premise can only be an instance either of
$\mathrm{(id)}$ or $\mathrm{({L}{\bot})}$; i.e., the cut has one of these
forms:

$\mathrm{(id)}$ ${p}\Rightarrow{p}$ $\mathcal{T}$
${\Gamma_{1},p,\Gamma_{2}}\Rightarrow{\varphi}$ $\mathrm{(cut)}$
${\Gamma_{1},p,\Gamma_{2}}\Rightarrow{\varphi}$ $\mathrm{(\bot L)}$
${\Delta_{1},\bot,\Delta_{2}}\Rightarrow{p}$ $\mathcal{T}$
${\Gamma_{1},p,\Gamma_{2}}\Rightarrow{\varphi}$ $\mathrm{(cut)}$
${\Gamma_{1},\Delta_{1},\bot,\Delta_{2},\Gamma_{2}}\Rightarrow{\varphi}$

The cut above left is clearly eliminable since the second premise matches the
conclusion; the cut above right is replaced by an instance of
$\mathrm{({L}{\bot})}$.

Inductive step. Assume the cut has cut-height $\geq 3$. If neither of the
premises of cut are from $\mathcal{T}$, the usual cut-reduction steps apply
[GalJipKowOno07, 4.1.1]. Else, if the topmost cut is standard, nothing needs
to be done since we admit such cuts. The remaining case is that the right
premise is from $\mathcal{T}$ and the left premise is from some other rule. It
follows that the topmost non-standard cut occurs as follows.

$\delta_{1}$ ${\Gamma}\Rightarrow{p}$ $\mathcal{T}$
${\Delta_{1},p,\Delta_{2}}\Rightarrow{\Pi}$ $\mathrm{(cut)}$
${\Delta_{1},\Gamma,\Delta_{2}}\Rightarrow{\Pi}$

Since the cut-height is $\geq 3$, we have that the left premise is not an
instance of an axiomatic rule. Consider the last rule in $\delta_{1}$. We
transform each case so the non-standard cut is replaced with a cut that is
smaller under the induction measure. We indicate the transformations with
$\rightsquigarrow$. Since the cut formula is a propositional variable (this is
forced by the right premise being from the regular theory $\mathcal{T}$), the
last rule in $\delta_{1}$ cannot be a right-introduction rule. We provide some
representative cases.

  * 1.

The left premise of the cut under consideration is the conclusion of a
standard cut:

$\mathcal{T}$ ${\Theta}\Rightarrow{\varphi}$ $\delta_{1}$
${\Gamma_{1},\varphi,\Gamma_{2}}\Rightarrow{p}$ $\mathrm{(cut)}$
${\Gamma_{1},\Theta,\Gamma_{2}}\Rightarrow{p}$ $\mathcal{T}$
${\Delta_{1},p,\Delta_{2}}\Rightarrow{\Pi}$ $\mathrm{(cut)}$
${\Delta_{1},\Gamma_{1},\Theta,\Gamma_{2},\Delta_{2}}\Rightarrow{\Pi}$

$\rightsquigarrow$

$\mathcal{T}$ ${\Theta}\Rightarrow{\varphi}$ $\delta_{1}$
${\Gamma_{1},\varphi,\Gamma_{2}}\Rightarrow{p}$ $\mathcal{T}$
${\Delta_{1},p,\Delta_{2}}\Rightarrow{\Pi}$ $\mathrm{(cut)}$
${\Delta_{1},\Gamma_{1},\varphi,\Gamma_{2},\Delta_{2}}\Rightarrow{p}$
$\mathrm{(cut)}$
${\Delta_{1},\Gamma_{1},\Theta,\Gamma_{2},\Delta_{2}}\Rightarrow{\Pi}$

  * 2.

$\mathrm{(L\otimes)}$

$\delta_{2}$ ${\Gamma_{1},\varphi_{1},\varphi_{2},\Gamma_{2}}\Rightarrow{p}$
$\mathrm{(L\otimes)}$
${\Gamma_{1},\varphi_{1}\otimes\varphi_{2},\Gamma_{2}}\Rightarrow{p}$
$\mathcal{T}$ ${\Delta_{1},p,\Delta_{2}}\Rightarrow{\Pi}$ $\mathrm{(cut)}$
${\Delta_{1},\Gamma_{1},\varphi_{1}\otimes\varphi_{2},\Gamma_{2},\Delta_{2}}\Rightarrow{\Pi}$

$\rightsquigarrow$

$\delta_{2}$ ${\Gamma_{1},\varphi_{1},\varphi_{2},\Gamma_{2}}\Rightarrow{p}$
$\mathcal{T}$ ${\Delta_{1},p,\Delta_{2}}\Rightarrow{\Pi}$ $\mathrm{(cut)}$
${\Delta_{1},\Gamma_{1},\varphi_{1},\varphi_{2},\Gamma_{2},\Delta_{2}}\Rightarrow{\Pi}$
$\mathrm{(L\otimes)}$
${\Delta_{1},\Gamma_{1},\varphi_{1}\otimes\varphi_{2},\Gamma_{2},\Delta_{2}}\Rightarrow{\Pi}$

The second assertion follows by structural induction on standard deductions.
The base case is obvious. Inductive step. The claim is immediate for a logical
rule, $\mathrm{(lw)}$, and $\mathrm{(rw)}$, by the induction hypothesis
applied to the deduction concluding the premise, and since every formula in
the premise must be a subformula of a formula in the conclusion. It remains to
check the case of a standard cut.

$\mathcal{T}$ ${\Delta}\Rightarrow{\psi}$ $\delta_{1}$
${\Gamma_{1},\psi,\Gamma_{2}}\Rightarrow{\varphi}$ cut
${\Gamma_{1},\Delta,\Gamma_{2}}\Rightarrow{\varphi}$

The claim follows since $\psi$ is a formula present in one of the sequents in
$\mathcal{T}$. ∎

The next lemma is a direct consequence of Lem. 2 and tells us that sequent-
deducibility in ${\mathbf{FL}_{\mathbf{w}}^{\Sigma^{\prime}}}$ reduces to the
same problem over an expanded signature
$\Sigma_{\mathbf{FL}}\supseteq\Sigma\supseteq\Sigma^{\prime}$. In other words,
$\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\Sigma}}\mathsf{\Rightarrow}}$ is a
_conservative expansion_ of
$\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\Sigma^{\prime}}}\mathsf{\Rightarrow}}$.

Let $\Sigma^{\prime}\subseteq\Sigma\subseteq\Sigma_{\mathbf{FL}}$. If
$\mathcal{T}\cup\\{s\\}$ are sequents over
$\mathrm{Fm}_{\Sigma^{\prime}}(\mathcal{P})$, then
$\mathcal{T}\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\Sigma^{\prime}}}\mathsf{\Rightarrow}}s$
iff
$\mathcal{T}\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\Sigma}}\mathsf{\Rightarrow}}s.$

###### Proof.

The nontrivial direction is right-to-left, so suppose that
$\mathcal{T}\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\Sigma}}\mathsf{\Rightarrow}}s$
is witnessed by a deduction $\delta$. Obtain a standard deduction
$\delta^{\prime}$ from $\delta$ by Lem. 2. The new proof will have sequents
over $\mathrm{Fm}_{\Sigma^{\prime}}(\mathcal{P})$ only (by the subformula
property proved also in Lem. 2), and thus must be a deduction in
$\mathbf{FL}_{\mathbf{w}}^{\Sigma^{\prime}}$.∎

##  3 Hyper-Ackermannian lower bounds

We obtain hyper-Ackermannian lower bounds for the sequent-deducibility problem
in $\Sigma$-fragments of ${\mathbf{FL}_{\mathbf{w}}}$ where
$\otimes\in\Sigma$, via a reduction from the reachability problem in lossy
channel systems. The result extends to the problem of deducibility if $\Sigma$
also contains ${\setminus}$ (or ${/}$), $0$ and $1$, in view of Lem. 2. We
begin by introducing lossy channel systems and their reachability problem, and
then show how to encode it into sequent-deducibility in
${\mathbf{FL}_{\mathbf{w}}^{\otimes}}$.

###  3.1 Lossy channel systems

A channel system is a computational model with unbounded FIFO channels
(queues), defined as follows.

A _channel system_ (CS) is a structure
$\mathcal{L}:=\left\langle{\mathtt{Q},\mathtt{C},\mathtt{M},\mathtt{I}}\right\rangle$,
where

  1. 1.

$\mathtt{Q}:=\left\\{{q_{1},\ldots,q_{m}}\right\\}$ is a finite set of
_states_ ;

  2. 2.

$\mathtt{C}:=\left\\{{c_{1},\ldots,c_{n}}\right\\}$ is a finite set of
_channels_ ;

  3. 3.

$\mathtt{M}:=\left\\{{\mathtt{a}_{1},\ldots,\mathtt{a}_{k}}\right\\}$ is a
finite _message alphabet_ ; and

  4. 4.

$\mathtt{I}\subseteq\mathtt{Q}\times\mathtt{C}\times\mathtt{M}\times\\{!,?\\}\times\mathtt{Q}$
is a finite set of _instructions_.

We denote by $\mathsf{Conf}(\mathcal{L})$ the set
$\mathtt{Q}\times(\mathtt{M}^{\ast})^{n}$ of _configurations_ of
$\mathcal{L}$, where $\mathtt{M}^{\ast}$ is the set of all finite sequences of
elements in $\mathtt{M}$.

The _perfect steps_ of a CS $\mathcal{L}$ are given by a binary relation
$\to_{\mathcal{L}\;\mathsf{perf}}\;\subseteq\mathsf{Conf}(\mathcal{L})\times\mathsf{Conf}(\mathcal{L})$
such that
$\left(q_{i},u_{1},\ldots,u_{r},\ldots,u_{n}\right)\to_{\mathcal{L}\;\mathsf{perf}}\left(q_{j},u_{1},\ldots,v_{r},\ldots,u_{n}\right)$
if either

  1. 1.

$u_{r}=\mathtt{a}_{p}v_{r}$ and
$\left(q_{i},c_{r},\mathtt{a}_{p},?,q_{j}\right)\in\mathtt{I}$ (read and
remove $\mathtt{a}_{p}$ from the _front_ of channel $c_{r}$ and change state
from $q_{i}$ to $q_{j}$)

  2. 2.

$v_{r}=u_{r}\mathtt{a}_{p}$ and
$\left(q_{i},c_{r},\mathtt{a}_{p},!,q_{j}\right)\in\mathtt{I}$ (write
$\mathtt{a}_{p}$ at the _back_ of channel $c_{r}$ and change state from
$q_{i}$ to $q_{j}$).

Let $\to_{\mathcal{L}\;\mathsf{perf}}^{?}$ and
$\to_{\mathcal{L}\;\mathsf{perf}}^{!}$ denote the perfect steps given by items
1 and 2 respectively. Also let $\to_{\mathcal{L}\;\mathsf{perf}}^{\ast}$
denote the reflexive and transitive closure of
$\to_{\mathcal{L}\;\mathsf{perf}}$.

Clearly, $u\to_{\mathcal{L}\;\mathsf{perf}}^{\ast}v$ iff there is a finite
sequence $w_{1},\ldots,w_{\eta}$ ($\eta\geq 1$) of configurations such that
$u=w_{1}$, $v=w_{\eta}$ and $w_{i}\to_{\mathcal{L}\;\mathsf{perf}}w_{i+1}$ for
each $i$ ($1\leq i<\eta$). This sequence is called a _perfect computation in
$\mathcal{L}$_ of length $\eta$ and it witnesses that $u$ _reaches_ $v$ in
$\mathcal{L}$.

Reachability (as well as many other verification problems for CSs) is
undecidable [brand1983], but adding lossy behaviour makes it decidable. This
behaviour is introduced in the operational semantics of a CS as follows.

The _lossy semantics_ of a CS $\mathcal{L}$ is given by a relation
$\to_{\mathcal{L}\;\mathsf{lossy}}\;\subseteq\mathsf{Conf}(\mathcal{L})\times\mathsf{Conf}(\mathcal{L})$
that extends $\to_{\mathcal{L}\;\mathsf{perf}}$ with all transitions (called
_lossy steps_) of the form
$\left(q_{i},u_{1},\ldots,u_{r},\ldots,u_{n}\right)\to_{\mathcal{L}\;\mathsf{lossy}}^{l}\left(q_{i},u_{1},\ldots,v_{r},\ldots,u_{n}\right)$
such that $u_{r}=w_{1}\mathtt{a}_{p}w_{2}$ and $v_{r}=w_{1}w_{2}$. Let
$\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}$ be the reflexive and transitive
closure of $\to_{\mathcal{L}\;\mathsf{lossy}}$. A channel system with a lossy
semantics is called a _lossy channel system (LCS)_. Intuitively, in an LCS the
lossy steps permit any channel to lose a message (a symbol) from any position
at any moment without changing the state. No instruction in the machine is
required for this. The relation $\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}$
induces a notion of _lossy computation in $\mathcal{L}$_ and reachability is
defined analogously to perfect computations with
$\to_{\mathcal{L}\;\mathsf{perf}}^{\ast}$. Since a step can be either read,
write, or lossy, we use $\to_{\mathcal{L}\;\mathsf{lossy}}^{?}$,
$\to_{\mathcal{L}\;\mathsf{lossy}}^{!}$ or
$\to_{\mathcal{L}\;\mathsf{lossy}}^{l}$ to indicate precisely which step was
performed in a lossy computation.

[Reachability problem in LCSs] Given a LCS $\mathcal{L}$ and configurations
$u,v\in\mathsf{Conf}(\mathcal{L})$, does
$u\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}v$?

The relation $\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}$ has an equivalent
definition in the literature [schnoebelen2002, Sec. 2] as
$u\rightsquigarrow_{\mathcal{L}}^{\ast}v$ if, and only if, there are
$u^{\prime},v^{\prime}\in\mathsf{Conf}(\mathcal{L})$ such that
$u\to_{\mathcal{L}\;\mathsf{lossy}}^{l\ast}u^{\prime}\to_{\mathcal{L}\;\mathsf{perf}}v^{\prime}\to_{\mathcal{L}\;\mathsf{lossy}}^{l\ast}v$
(the $\ast$ denotes the reflexive transitive closure). That is, messages may
be lost before and after performing a perfect step. It can be shown that
$\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}\;=\;\to_{\mathcal{L}\;\mathsf{lossy}}^{l\ast}\circ\to_{\mathcal{L}\;\mathsf{perf}}\circ\to_{\mathcal{L}\;\mathsf{lossy}}^{l\ast}\;=\;\rightsquigarrow_{\mathcal{L}}^{\ast}$.
The latter relation is shown [chambart2008, App. A] to have no impact on the
complexity of reachability compared to the “write-lossy” mechanism employed in
the proof of Thm. 3.1 [chambart2008] stated below.

[[chambart2008, Thm. 5.5, Obs. 6.1, App. A]] Reachability in LCSs is HAck-
complete.

###  3.2 Encoding reachability in LCSs into sequent-deducibility

We code each instruction of a lossy channel system into a sequent. The
collection of these sequents is the _theory_ associated to the system.

For an LCS
$\mathcal{L}=\left\langle{\mathtt{Q},\mathtt{C},\mathtt{M},\mathtt{I}}\right\rangle$,
define these sets of propositional variables:

  1. 1.

$\mathsf{Q}:=\\{Q_{i}\mid q_{i}\in\mathtt{Q}\\}$ (state variables)

  2. 2.

$\\#:=\\{\\#^{s}_{i}\mid c_{i}\in\mathtt{C}\\}\cup\\{\\#^{e}_{i}\mid
c_{i}\in\mathtt{C}\\}$ (channel markers)

  3. 3.

$\mathsf{M}:=\\{P_{a}\mid a\in\mathtt{M}\\}$ (alphabet variables)

Moreover, define
$\mathsf{Props}(\mathcal{L}):=\mathsf{Q}\cup\\#\cup\mathsf{M}$.

[Theory of an LCS] Given an LCS
$\mathcal{L}=\left\langle{\mathtt{Q},\mathtt{C},\mathtt{M},\mathtt{I}}\right\rangle$,
the _theory of $\mathcal{L}$_, denoted by $\mathcal{T}(\mathcal{L})$, is
defined as the union of the following finite sets of sequents:

  1. 1.

$\mathcal{T}(\mathcal{L})^{!}:=\\{{\\#^{e}_{l},Q_{i}}\Rightarrow{P_{a}\otimes(\\#^{e}_{l}\otimes
Q_{j})}\mid\left(q_{i},c_{l},a,!,q_{j}\right)\in\mathtt{I}\\}$;

  2. 2.

$\mathcal{T}(\mathcal{L})^{?}:=\\{{\\#^{s}_{l},P_{a},Q_{i}}\Rightarrow{\\#^{s}_{l}\otimes
Q_{j}}\mid\left(q_{i},c_{l},a,?,q_{j}\right)\in\mathtt{I}\\}$;

  3. 3.

$\mathcal{T}(\mathcal{L})^{\mathtt{Q}}:=\bigcup\limits_{\begin{subarray}{c}Q\in\mathsf{Q}\\\
R\in\mathsf{Props}(\mathcal{L}){\setminus}\mathsf{Q}\end{subarray}}\\{{R,Q}\Rightarrow{Q\otimes
R}\\}\cup\\{{Q,R}\Rightarrow{R\otimes Q}\\}$.

Note that $\mathcal{T}(\mathcal{L})$ is a regular theory in the sense of Def.
2.

Recall that
$\bigotimes{\varphi_{1},\ldots,\varphi_{m}}:=\varphi_{1}\otimes(\varphi_{2}\otimes(\ldots(\varphi_{m-1}\otimes\varphi_{m})\ldots))$,
where $m\geq 1$ and $\varphi_{1},\ldots,\varphi_{m}$ is a sequence of
formulas. We now translate a reachability instance in a fixed LCS
$\mathcal{L}=\left\langle{\mathtt{Q},\mathtt{C},\mathtt{M},\mathtt{I}}\right\rangle$
to a sequent-deducibility instance in $\mathbf{FL}_{\mathbf{w}}^{\otimes}$. We
begin by coding a configuration as a sequence.

Given $u:=\left(q_{i},u_{1},\ldots,u_{n}\right)\in\mathsf{Conf}(\mathcal{L})$,
define the sequence
$E(u):={Q_{i},\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}$,
where, for $u_{i}=a_{1}\cdots a_{k_{i}}\in\mathtt{M}^{\ast}$, $U_{i}$ is the
sequence $P_{a_{1}},\ldots,P_{a_{k_{i}}}$ of propositional variables.

For $u:=\left(q_{i},u_{1},\ldots,u_{n}\right)$,
$v:=\left(q_{j},v_{1},\ldots,v_{n}\right)\in\mathsf{Conf}(\mathcal{L})$,
define the sequent

$S_{{u}\rightarrow{v}}:={E(u)}\Rightarrow{\bigotimes E(v)}.$

Define also $S_{{u}\rightarrow{v}}^{\bowtie}$ as the set of sequents of the
above form where the occurrence of $Q_{i}$ in the antecedent may appear in any
position (i.e., not necessarily at the front as in $E(u)$).

We note that sequents in standard deductions in
$\mathbf{FL}_{\mathbf{w}}^{\otimes}$ from a regular theory have a nonempty
succedent coming from the observation that every leaf has this property:

Let $\mathcal{T}$ be a regular theory. It is never the case that
$\mathcal{T}\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\otimes}}\mathsf{\Rightarrow}}^{\mathsf{std}}{\Gamma}\Rightarrow{}$.

###### Proof.

It follows because no axiomatic rule has conclusion with empty succedent and
no other rule allows to derive a sequent with empty succedent from one with
nonempty succedent. ∎

The flattening $[\varphi]$ is the sequence of propositional variables obtained
from a formula $\varphi$ by replacing ‘$\otimes$’ with ‘,’. E.g.,
$[p\otimes((q\otimes s)\otimes r)]=p,q,s,r$. The flattening $[\Gamma]$ of a
sequence $\Gamma$ of formulas is the concatenation of the flattening of the
formulas in $\Gamma$ in the order they appear in the sequence. Let $\\#\Delta$
denote the subsequence of $\Delta$ having only variables from the set $\\#$
(that is, only channel markers). The _$\mathsf{Q}$ -free subsequence_ of a
sequence of propositional variables is obtained by deleting all occurrences of
state variables.

The following lemmas express that in standard deductions from a regular
theory, in various situations, propositional variables occurring positively
must also occur negatively. They abstract what is needed for the right-to-left
direction of Lem. 3.2 below. The proofs are by structural induction on
standard deductions.

Let $\Gamma$ be a sequence of formulas, none having a state variable. If
$\mathcal{T}(\mathcal{L})\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\otimes}}\mathsf{\Rightarrow}}^{\mathsf{std}}{\Gamma}\Rightarrow{\varphi}$,
then the $\mathsf{Q}$-free subsequence of $[\varphi]$ is a subsequence of
$[\Gamma]$.

###### Proof.

Structural induction on a standard deduction witnessing
$\mathcal{T}(\mathcal{L})\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\otimes}}\mathsf{\Rightarrow}}{\Gamma}\Rightarrow{\varphi}$.
_Base case_. For elements from $\mathcal{T}(\mathcal{L})$ it holds vacuously
since each sequent contains a state variable in the antecedent; for an
identity sequent the claim is immediate. _Inductive step_. Suppose that the
last rule instance applied is $\mathrm{\mathrm{(lw)}}$,
$\mathrm{({R}{\otimes})}$ or $\mathrm{({L}{\otimes})}$. Applying the IH to its
premise(s), we have that the $\mathsf{Q}$-free subsequence of $[\varphi]$ is a
subsequence of the flattening of the premise antecedent(s), and hence also of
$[\Gamma]$. The last rule instance cannot be a standard cut as the antecedent
of each element in $\mathcal{T}(\mathcal{L})$ contain a state variable hence
$\Gamma$ would contains a state variable, contradicting the hypotheses. The
rule $\mathrm{(rw)}$ cannot occur due to Lem. 3.2. ∎

Let $\Gamma$ be a sequence of formulas, $u\in\mathsf{Conf}(\mathcal{L})$ and
$L$ a nonempty subsequence of $E(u)$. Then
$\mathcal{T}(\mathcal{L})\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\otimes}}\mathsf{\Rightarrow}}^{\mathsf{std}}{\Gamma}\Rightarrow{\bigotimes
L}$ implies that the variables in $\\#L$ appear at least once in $[\Gamma]$.

###### Proof.

Induction on the structure of a standard deduction witnessing
$\mathcal{T}(\mathcal{L})\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\otimes}}\mathsf{\Rightarrow}}{\Gamma}\Rightarrow{\bigotimes
L}$. _Base case._ Straightforward: identity sequent ${p}\Rightarrow{p}$
(trivial) and an element from $\mathcal{T}(\mathcal{L})$ (by inspection, it
contains no channel variables or the same channel variable occurs in the
antecedent and succedent). _Inductive step_. Consider the last rule instance
in the standard deduction. For $\mathrm{({R}{\otimes})}$,
$\mathrm{({L}{\otimes})}$ and $\mathrm{\mathrm{(lw)}}$, we have by IH that
each variable in $\\#L$ appears in $[\Gamma^{\prime}]$ for the antecedent
$\Gamma^{\prime}$ of some premise of the rule instance. Those variables will
be carried to the conclusion antecedent. If the last rule applied is a
standard cut, its right premise has the form
${\Gamma_{1},\varphi,\Gamma_{2}}\Rightarrow{\bigotimes L}$ where $\varphi$ is
the cut formula. By IH, every variable in $\\#L$ appears in
$[\Gamma_{1},\varphi,\Gamma_{2}]$. Moreover, since the left premise is from
$\mathcal{T}(\mathcal{L})$, any channel variable occurring in the cut formula
will occur in its antecedent, and hence also in $[\Gamma]$. The case of
$\mathrm{(rw)}$ does not need to be considered in view of Lem. 3.2. ∎

Let $\Gamma$ be a sequence of formulas and $\varphi$ be a formula. If
$\mathcal{T}(\mathcal{L})\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\otimes}}\mathsf{\Rightarrow}}^{\mathsf{std}}{\Gamma}\Rightarrow{Q_{i}\otimes\varphi}$
or
$\mathcal{T}(\mathcal{L})\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\otimes}}\mathsf{\Rightarrow}}^{\mathsf{std}}{\Gamma}\Rightarrow{Q_{i}}$,
then $[\Gamma]$ must contain a state variable.

###### Proof.

Structural induction on a derivation witnessing
$\mathcal{T}(\mathcal{L})\vdash_{{\mathbf{SL_{w}^{\cdot}}}\mathsf{\Rightarrow}}{\Gamma}\Rightarrow{Q_{i}\otimes\varphi}$.
_Base case_. The case of an initial sequent is trivial, and the antecedent of
any sequent from $\mathcal{T}(\mathcal{L})$ contains a state variable.
_Inductive step_. Suppose that the last rule is $\mathrm{({R}{\otimes})}$. The
left premise has $Q_{i}$ as succedent, and hence by IH, its antecedent will
contain a state variable that is carried down to the conclusion. The argument
is analogous for $\mathrm{\mathrm{(lw)}}$ and $\mathrm{({L}{\otimes})}$. If
the last rule instance is a standard cut, its left premise is a sequent in
$\mathcal{T}(\mathcal{L})$. As already observed, the antecedent of such a
sequent contains a state variable and that will be carried down to the
conclusion. The case of $\mathrm{(rw)}$ does not need to be considered in view
of Lem. 3.2.

The case of
$\mathcal{T}(\mathcal{L})\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\otimes}}\mathsf{\Rightarrow}}{\Gamma}\Rightarrow{Q_{i}}$
is similar. ∎

We are ready to reduce reachability in lossy channel systems to sequent-
deducibility.

For all LCS $\mathcal{L}$, given $u,v\in\mathsf{Conf}(\mathcal{L})$,
$u\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}v\text{ iff
}\mathcal{T}(\mathcal{L})\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\otimes}}\mathsf{\Rightarrow}}^{\mathsf{std}}s$
for some $s\in S_{{u}\rightarrow{v}}^{\bowtie}$. In the left-to-right
direction, we work by induction on the length $k\geq 1$ of a computation
witnessing $u\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}v$. _Base case._ If
$k=1$, $u=v$, and $S_{{u}\rightarrow{v}}$ is provable by $\mathrm{(id)}$ and
$\mathrm{({R}{\otimes})}$. _Inductive step_. The computation decomposes as
$u\to_{\mathcal{L}\;\mathsf{lossy}}^{\sigma}v^{\prime}\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}v$
with length $k+1$. As $v^{\prime}\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}v$ is
witnessed by a computation of length $k$, IH yields
$\mathcal{T}(\mathcal{L})\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\otimes}}\mathsf{\Rightarrow}}s^{\prime}$
for some $s^{\prime}\in S_{{v^{\prime}}\rightarrow{v}}^{\bowtie}$. We extend
the latter deduction downwards to $s$, using a case analysis on $\sigma$ to
determine the form of $s^{\prime}$ and $s$:

  1. 1.

if $\sigma=\,?$, by effect of
$\left(q_{i},c_{l},a,?,q_{j}\right)\in\mathtt{I}$: then
$u_{l}=av^{\prime}_{l}$, all the other channels have the same content, and the
state transits from $q_{i}$ to $q_{j}$. Thus $s^{\prime}$ has the following
form, possibly following repeated standard cuts with sequents in
$\mathcal{T}(\mathcal{L})^{\mathtt{Q}}$.

${\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,\\#^{s}_{l-1},U_{l-1},\\#^{e}_{l-1},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\\#^{s}_{l},Q_{j}},V^{\prime}_{l},\\#^{e}_{l},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$

Apply $\mathrm{({L}{\otimes})}$ and a standard cut with
${\\#^{s}_{l},P_{a},Q_{i}}\Rightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\\#^{s}_{l}\otimes
Q_{j}}}$ to obtain $s$.

  2. 2.

if $\sigma=l$: the state is unchanged, and
$v_{l}^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{1}z_{2}}$,
for
$u={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{1}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}a}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}z_{2}}$.
Thus $s^{\prime}$ has the following form, possibly following repeated standard
cuts with sequents in $\mathcal{T}(\mathcal{L})^{\mathtt{Q}}$.

${Q_{j},\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,\\#^{s}_{l},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}Z_{1},Z_{2}},\\#^{e}_{l},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$

By $\mathrm{\mathrm{(lw)}}$
${Q_{j},\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,\\#^{s}_{l},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}Z_{1},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P_{a}},Z_{2}},\\#^{e}_{l},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$

  3. 3.

if $\sigma=\,!$, by effect of
$\left(q_{i},c_{l},a,!,q_{j}\right)\in\mathtt{I}$: by definition of this step,
$v^{\prime}_{l}=u_{l}a$, the content in other channels of $u$ and $v^{\prime}$
is unchanged, and the state transits from $q_{i}$ to $q_{j}$. Thus
$s^{\prime}$ has the following form modulo the position of $Q_{j}$. In any
case, the $s^{\prime}$ can be moved to the displayed position through repeated
standard cuts with sequents in $\mathcal{T}(\mathcal{L})^{\mathtt{Q}}$.

${\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,\\#^{s}_{l},U_{l},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P_{a},\\#^{e}_{l},Q_{j}},\\#^{s}_{l+1},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$

It suffices now to apply $\mathrm{({L}{\otimes})}$ twice and a standard cut
with
${\\#^{e}_{l},Q_{i}}\Rightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P_{a}\otimes\\#^{e}_{l}\otimes
Q_{j}}}$ to obtain the sequent $s$:
${\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,\\#^{s}_{l},U_{l},{\\#^{e}_{l},Q_{j}},\\#^{s}_{l+1},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$.

For the right-to-left direction, we establish property
$\mathcal{P}(\delta):=$: “for all $u,v\in\mathsf{Conf}(\mathcal{L})$, if
$\delta$ is a standard deduction witnessing
$\mathcal{T}(\mathcal{L})\vdash_{{\mathbf{FL}_{\mathbf{w}}^{\otimes}}\mathsf{\Rightarrow}}s$
for some $s\in S_{{u}\rightarrow{v}}^{\bowtie}$, then
$u\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}v$”. Induction on the structure of
$\delta$.

_Base case_. No initial sequent nor any sequent from
$\mathcal{T}(\mathcal{L})$ is an image of an encoding of a configuration since
it does not contain any pair $\\{\\#^{s}_{i},\\#^{e}_{i}\\}$ of channel
markers.

_Inductive step_. Let $u=(q_{i},u_{1},\ldots,u_{n})$ and
$v=(q_{j},v_{1},\ldots,v_{n})$. By cases on the last rule applied in $\delta$.
It cannot be $\mathrm{({L}{\otimes})}$ since the antecedent of $s$ is a
sequence of propositional variables. Then it could be:

  1. 1.

$\mathrm{(rw)}$: Not possible by Lem. 3.2 since $\delta$ is a standard
deduction.

  2. 2.

$\mathrm{({R}{\otimes})}$: Write $s$ as
${\Gamma_{1},\Gamma_{2}}\Rightarrow{Q_{j}\otimes\varphi_{2}}$. The premises
then are ${\Gamma_{1}}\Rightarrow{Q_{j}}$ and
${\Gamma_{2}}\Rightarrow{\varphi_{2}}$. By Lem. 3.2, $\Gamma_{1}$ must have a
formula with a state variable, and thus $\Gamma_{2}$ lacks a state variable.
If $\Gamma_{1}$ contained anything more, it must contain a channel marker. By
Lem. 3.2, $\Gamma_{2}$ must contain all the channel markers to fulfil the
requirement that $[\varphi_{2}]$ must be a subsequence of $[\Gamma_{2}]$.
Hence $\Gamma_{1}$ is the singleton sequence $Q_{l}$. Now, for
${Q_{l}}\Rightarrow{Q_{j}}$ to be provable, we must have $l=j$. Also,
$[\varphi_{2}]$ a subsequence of $[\Gamma_{2}]$ implies that the channel
portions in the succedent are subsequences of the corresponding ones in the
antecedent. Thus, $u$ can reach $v$ by losing messages. Observe: the IH is not
employed.

  3. 3.

$\mathrm{(lw)}$: We claim that the weakening introduces a variable into the
channel portion. This suffices since the premise would then be the image of a
configuration that, by IH, reaches $v$, and is itself reachable from $u$ by a
lossy step. To establish the claim, first note that the sequents involved in
an application of $\mathrm{(lw)}$ have the same succedent, in this case
$\bigotimes E(v)$. Let $\Gamma^{\prime}$ be the premise antecedent. By Lem.
3.2, we have that all channel variables appear in $\Gamma^{\prime}$. Since
these symbols appear only once in conclusion antecedent, weakening could not
have introduced them. If the weakening introduced the state variable, then
$\Gamma^{\prime}$ would have no state variables; that is impossible due to
Lem. 3.2 since the succedent does contain a state variable. The remaining
possibility is that weakening introduced a variable in the channel portion, so
the claim is proved.

  4. 4.

Standard cut with a sequent in $\mathcal{T}(\mathcal{L})^{?}$: The deduction
has the form

$\mathcal{T}(\mathcal{L})^{?}$
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\\#^{s}_{l},P_{a},Q_{i}}}\Rightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\\#^{s}_{l}\otimes
Q_{p}}}}$ $\delta_{1}$
${\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\\#^{s}_{l}\otimes
Q_{p}},U_{l},\\#^{e}_{l},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$ $\mathrm{(cut)}$
${\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\\#^{s}_{l},P_{a},Q_{i}},U_{l},\\#^{e}_{l},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$

Consider the last rule in $\delta_{1}$. It cannot be a (standard) cut as that
would have introduced a state variable on its own (i.e., unfused) into the
conclusion. If it was $\mathrm{({R}{\otimes})}$ then the left premise has the
form ${\Gamma_{1}}\Rightarrow{Q_{j}}$ and the second premise has the form
${\Gamma_{2}}\Rightarrow{\varphi_{2}}$. By Lem. 3.2,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\\#^{s}_{l}\otimes
Q_{p}}\in\Gamma_{1}$, and thus $\Gamma_{2}$ consists only of propositional
variables. Since $\\#^{s}_{l}$ is not in $\Gamma_{2}$ but $\varphi_{2}$
contains all channel markers, Lem. 3.2 gives a contradiction. So
$\mathrm{({R}{\otimes})}$ was not the last rule applied. Neither can it be
$\mathrm{(rw)}$ due to Lem. 3.2.

We are left with two alternatives for the last rule in $\delta_{1}$:
$\mathrm{(lw)}$ and $\mathrm{({L}{\otimes})}$. If $\mathrm{(lw)}$, arguing as
in the previous item, the introduced variable must be in the channel portion
by Lem. 3.2 and Lem. 3.2. Iterating the entire argument up to this point
(implicit induction), after multiple applications of $\mathrm{(lw)}$ we must
ultimately encounter $\mathrm{({L}{\otimes})}$ (we have ruled out all the
other possibilities). The situation is therefore the following.

$\mathcal{T}(\mathcal{L})^{?}$
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\\#^{s}_{l},P_{a},Q_{i}}}\Rightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\\#^{s}_{l}\otimes
Q_{p}}}}$ $\delta_{1}^{\prime}$
${\\#^{s}_{1},U^{\prime}_{1},\\#^{e}_{1},\ldots,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\\#^{s}_{l},Q_{p}},U^{\prime}_{l},\\#^{e}_{l},\ldots,\\#^{s}_{n},U^{\prime}_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$ $\mathrm{({L}{\otimes})}$
${\\#^{s}_{1},U^{\prime}_{1},\\#^{e}_{1},\ldots,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\\#^{s}_{l}\otimes
Q_{p}}},U^{\prime}_{l},\\#^{e}_{l},\ldots,\\#^{s}_{n},U^{\prime}_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$ $\mathrm{(lw)}^{\ast}$
${\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\\#^{s}_{l}\otimes
Q_{p}}},U_{l},\\#^{e}_{l},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$ $\mathrm{(cut)}$
${\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\\#^{s}_{l},P_{a},Q_{i}},U_{l},\\#^{e}_{l},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$

From the IH, we obtain that
$\left(q_{p},u^{\prime}_{1},\ldots,u^{\prime}_{l},\ldots,u^{\prime}_{n}\right)\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}v$.
Since
$\left(q_{i},u_{1},\ldots,au_{l},\ldots,u_{n}\right)\to_{\mathcal{L}\;\mathsf{lossy}}^{?}\left(q_{p},u_{1},\ldots,u_{l},\ldots,u_{n}\right)\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}\left(q_{p},u^{\prime}_{1},\ldots,u^{\prime}_{l},\ldots,u^{\prime}_{n}\right)$,
we are done.

  5. 5.

Standard cut with a sequent in $\mathcal{T}(\mathcal{L})^{!}$: In this case
the deduction has the form

$\mathcal{T}(\mathcal{L})^{!}$
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\\#^{e}_{l},Q_{i}}}\Rightarrow{{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P_{a}\otimes\\#^{e}_{l}\otimes
Q_{p}}}}$ $\delta_{1}$
${\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,\\#^{s}_{l},U_{l},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P_{a}\otimes\\#^{e}_{l}\otimes
Q_{p}},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes E(v)}$
$\mathrm{(cut)}$
${\\#^{s}_{1},U_{1},\\#^{e}_{1},\ldots,\\#^{s}_{l},U_{l},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\\#^{e}_{l},Q_{i}},\ldots,\\#^{s}_{n},U_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$

Consider the last rules in $\delta_{1}$. Arguing as in the
$\mathcal{T}(\mathcal{L})^{?}$ case, it is a sequence of $\mathrm{(lw)}$ rules
introducing variables in channel portions, then $\mathrm{({L}{\otimes})}$. The
latter premise is

${\\#^{s}_{1},U^{\prime}_{1},\\#^{e}_{1},\ldots,\\#^{s}_{l},U^{\prime}_{l},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P_{a},\\#^{e}_{l}\otimes
Q_{p}},\ldots,\\#^{s}_{n},U^{\prime}_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$

Since no state variable occurs by itself in the antecedent, the above sequent
was not derived by a (standard) cut. Nor was it by $\mathrm{({R}{\otimes})}$,
since its left premise would contain $\\#^{e}_{l}\otimes Q_{p}$ hence
depriving the right premise antecedent of $\\#^{e}_{l}$ leading to a
contradiction with Lem. 3.2. Nor was it $\mathrm{(rw)}$ due to Lem. 3.2. Hence
we encounter once again a sequence of $\mathrm{(lw)}$ rules followed by an
application of $\mathrm{({L}{\otimes})}$, resulting in the sequent

${\\#^{s}_{1},U^{\prime\prime}_{1},\\#^{e}_{1},\ldots,\\#^{s}_{l},U^{\prime\prime}_{l},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}P_{a},\\#^{e}_{l},Q_{p}},\ldots,\\#^{s}_{n},U^{\prime\prime}_{n},\\#^{e}_{n}}\Rightarrow{\bigotimes
E(v)}$

By IH, we obtain that
$\left(q_{p},u^{\prime\prime}_{1},\ldots,u^{\prime\prime}_{l}a,\ldots,u^{\prime\prime}_{n}\right)\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}v$.
Since
$\left(q_{i},u_{1},\ldots,u_{l},\ldots,u_{n}\right)\to_{\mathcal{L}\;\mathsf{lossy}}^{!}\left(q_{p},u_{1},\ldots,u_{l}a,\ldots,u_{n}\right)\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}\left(q_{p},u^{\prime\prime}_{1},\ldots,u^{\prime\prime}_{l}a,\ldots,u^{\prime\prime}_{n}\right)$,
we conclude $u\to_{\mathcal{L}\;\mathsf{lossy}}^{\ast}v$.

  6. 6.

Standard cut with ${Q_{i},R}\Rightarrow{R\otimes
Q_{i}}\in\mathcal{T}(\mathcal{L})^{\mathtt{Q}}$ (sequent
${R,Q_{i}}\Rightarrow{Q_{i}\otimes R}$ is similar):

$\mathcal{T}(\mathcal{L})^{\mathtt{Q}}$
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}Q_{i},R}}\Rightarrow{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}R\otimes
Q_{i}}}$ $\delta_{1}$
${\Gamma_{1},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}R\otimes
Q_{i}},\Gamma_{2}}\Rightarrow{\bigotimes E(v)}$ $\mathrm{(cut)}$
${\Gamma_{1},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}Q_{i},R},\Gamma_{2}}\Rightarrow{\bigotimes
E(v)}$

As in the previous cases, the last rule applied in $\delta_{1}$ could not have
been a standard cut nor $\mathrm{(rw)}$. Suppose it is
$\mathrm{({R}{\otimes})}$. Writing the endsequent of $\delta_{1}$ as
${\Gamma_{3},\Gamma_{4}}\Rightarrow{Q_{j}\otimes\varphi_{2}}$, the left
premise would have the form ${\Gamma_{3}}\Rightarrow{Q_{i}}$ where
$\Gamma_{3}$ must contain $R\otimes Q_{i}$ (Lem. 3.2) and hence also
$\Gamma_{1}$. If $\Gamma_{1}$ is non-empty then it must contain a channel
marker and hence in the right premise ${\Gamma_{4}}\Rightarrow{\varphi_{2}}$,
the $\Gamma_{4}$ would lack a channel marker contradicting Lem. 3.2. If
$\Gamma_{1}$ is empty then $R$ must be a channel marker and once again
$\Gamma_{4}$ would lack a channel marker leading to a contradiction. Therefore
the rule is not $\mathrm{({R}{\otimes})}$.

The remaining possibility is a sequence of $\mathrm{(lw)}$ followed by
$\mathrm{({L}{\otimes})}$. The premise of the latter is in the image of an
encoding, thus the IH applies and we are done.

Let $\Sigma\subseteq\Sigma_{\mathbf{FL}}$. If $\otimes\in\Sigma$, then
sequent-deducibility in $\mathbf{FL}_{\mathbf{w}}^{\Sigma}$ is HAck-hard.
Moreover, if $\\{\otimes,{\setminus},0,1\\}\subseteq\Sigma$, then deducibility
is HAck-hard.

###### Proof.

The first assertion follows from Lem. 3.2, plus the fact that the reduction
established there is polynomial-time, and Lem. 2. The second one follows from
the first and Lem. 2. ∎

##  4 Hyper-Ackermannian upper bounds

We give an algorithm to decide the relation
$\vdash_{{\mathbf{S}}\mathsf{\Rightarrow}}$ for regular theories, for a
sequent calculus $\mathbf{S}$ containing the rule $\mathrm{(lw)}$ and
satisfying a generalized subformula property as defined below. In what
follows, given a finite $\Omega\subseteq\mathrm{Fm}_{\Sigma}(\mathcal{P})$, an
_$\Omega$ -sequent_ is a sequent in which only formulas in $\Omega$ appear.

A sequent calculus that is a structural rule extension of
$\mathbf{FL}_{\mathbf{w}}^{\Sigma}$ ($\Sigma\subseteq\Sigma_{\mathbf{FL}}$) is
called _amenable_ provided it satisfies the _generalized subformula property_
: for every regular theory $\mathcal{T}$, it is the case that
$\mathcal{T}\vdash_{{\mathbf{S}}\mathsf{\Rightarrow}}s$ iff there is a
$\mathcal{T}$-deduction of $s$ where only
$\mathsf{subf}(\mathcal{T}\cup\\{s\\})$-sequents appear (such a deduction is
called _analytic_). $\mathbf{FL}_{\mathbf{w}}^{\Sigma}$ is amenable for any
$\Sigma\subseteq\Sigma_{\mathbf{FL}}$; Lem. 2 gives the generalized subformula
property. Indeed, any _analytic structural rule_ extension of an amenable
calculus is amenable (see results for the substructural hierarchy, Ciabattoni
et al. [CiaGalTer17]).

###  4.1 Just enough on well-quasi-order theory

A _quasi-ordered set (qo-set)_ is a structure
$\mathbf{W}:=\left\langle{W,\preccurlyeq_{\mathbf{W}}}\right\rangle$, where
$W$ is a set and $\preccurlyeq_{\mathbf{W}}\,\subseteq W\times W$ is reflexive
and transitive (a _quasi order_ , for short). Abusing notation, we write
$a\in\mathbf{W}$ for $a\in W$. We denote by $\mathbb{N}$ the set of natural
numbers; by $\mathbb{N}^{+}$ the set $\mathbb{N}{\setminus}\\{0\\}$; and,
given $\ell\in\mathbb{N}\cup\\{\omega\\}$, we write $\mathbb{N}_{<{\ell}}$ for
the set $\\{a\in\mathbb{N}\mid a<\ell\\}$. Given a qo-set $\mathbf{W}$, a _bad
sequence over $\mathbf{W}$_ (of length $\ell$) is a sequence
$(a_{i})_{i\in\mathbb{N}_{<{\ell}}}$ of elements of $\mathbf{W}$ such that,
for all $i<j$, $a_{i}\not\preccurlyeq_{\mathbf{W}}a_{j}$. A qo-set
$\mathbf{W}$ is a _well-quasi-ordered set (wqo-set)_ if every bad sequence
over it is finite (see [higman1952, Sec. 2] for equivalent definitions).
Examples include $\mathbb{N}^{k}$ under component-wise ordering (Dickson’s
Lemma [dickson1913]), and sequences under the subword embedding ordering:

[Higman’s Lemma [higman1952]] For any finite set $\Omega$,
$\left\langle{\Omega^{\ast},\preccurlyeq_{\ast}}\right\rangle$ is a wqo,
where, recall, $\Omega^{\ast}$ is the set of all finite sequences of elements
from $\Omega$ and $w_{1}\preccurlyeq_{\ast}w_{2}$ iff $w_{1}$ is obtainable
from $w_{2}$ by deleting some elements.

Bad sequences over a wqo, though finite, do not in general have a maximum
length. For example, $(1,0),(0,k),(0,k-1),\ldots,(0,0)$ is a bad sequence on
$\mathbb{N}^{2}$ under the component-wise ordering with length $k+2$ for every
$k\in\mathbb{N}$. Nevertheless, a maximum length can be ensured by limiting
the size of each element in the sequence to some (fixed) function of the size
of the preceding element. To achieve this, the wqo is enriched with more
structure. A _normed(well-)quasi-ordered set (n(w)qo-set)_ [schmitz2012notes]
is a structure
$\mathbf{W}:=\left\langle{W,\preccurlyeq_{\mathbf{W}},{\llbracket}{\cdot}{\rrbracket}_{\mathbf{W}}}\right\rangle$,
where $\left\langle{W,\preccurlyeq_{\mathbf{W}}}\right\rangle$ is a (w)qo-set
and ${\llbracket}{\cdot}{\rrbracket}_{\mathbf{W}}:W\to\mathbb{N}$ is a _proper
norm_ , meaning that, for all $n\in\mathbb{N}$, $\left\\{{a\in
W:{\llbracket}{a}{\rrbracket}_{\mathbf{W}}<n}\right\\}$ is finite. It is easy
to check that the following is a nwqo.

Given a finite set $\Omega$, let
$\boldsymbol{\mathbf{\Omega}}^{\ast}:=\left\langle{\Omega^{\ast},\preccurlyeq_{\ast},{\llbracket}{\cdot}{\rrbracket}_{\ast}}\right\rangle$,
where ${\llbracket}{w}{\rrbracket}_{\ast}$ is the length of $w$ (and
$\left\langle{\Omega^{\ast},\preccurlyeq_{\ast}}\right\rangle$ is as in Thm.
4.1).

Indeed, the _disjoint sum_ of these nwqos, defined below, is also an nwqo
[schmitz2012notes].

Given a finite set $\Omega$ and $m\in\mathbb{N}$, let
$m\cdot\boldsymbol{\mathbf{\Omega}}^{\ast}:=\left\langle{m\cdot\Omega^{\ast},\preccurlyeq_{m\cdot\boldsymbol{\mathbf{\Omega}}^{\ast}},{\llbracket}{\cdot}{\rrbracket}_{m\cdot\boldsymbol{\mathbf{\Omega}}^{\ast}}}\right\rangle$.
Here, $m\cdot\Omega^{\ast}:=\\{1,\ldots,m\\}\times\Omega^{\ast}$ is the
disjoint sum of $m$ copies of $\Omega^{\ast}$, and
$(i,w_{1})\preccurlyeq_{m\cdot\boldsymbol{\mathbf{\Omega}}^{\ast}}(j,w_{2})$
iff $i=j$ and $w_{1}\preccurlyeq_{\ast}w_{2}$. Also, define
${\llbracket}{(i,w)}{\rrbracket}_{m\cdot\boldsymbol{\mathbf{\Omega}}^{\ast}}:={\llbracket}{w}{\rrbracket}_{\ast}$.

A _control function_ is a mapping $g:\mathbb{N}\to\mathbb{N}$ that is strictly
increasing (for all $a,b\in\mathbb{N}$, if $a<b$, then $g(a)<g(b)$) and
strictly inflationary ($a<g(a)$ for all $a\in\mathbb{N}$).

For an nwqo-set $\mathbf{W}$, control function $g$, and _initial parameter_
$t\in\mathbb{N}$, a _$(g,t)$ -controlled bad sequence over $\mathbf{W}$_ is a
bad sequence $a_{0},\ldots,a_{\ell-1}$ over $\mathbf{W}$ where
${\llbracket}{a_{i}}{\rrbracket}_{\mathbf{W}}<g^{i}(t)$ for all $0\leq
i<\ell$. The $(g,t)$-controlled bad sequences have a maximum length
[figueira2011] using König’s Lemma. Denote by $L_{\mathbf{W}}^{g}(t)$ the
maximum length of a $(g,t)$-controlled bad sequence over $\mathbf{W}$. We call
$L_{\mathbf{W}}^{g}:\mathbb{N}\to\mathbb{N}$ the _length function_ of
$\mathbf{W}$ (for $g$). Bounds for $(g,t)$-controlled bad sequences over
$\mathbf{W}$ reduce to finding bounds for $L_{\mathbf{W}}^{g}$ (‘ _length
theorems_ ’), expressed in terms of the ordinal-indexed _extended Grzegorczyk
hierarchy_ $\\{\mathfrak{F}_{\alpha}\\}_{\alpha}$, from which the hierarchy
$\\{\mathbf{F}_{\alpha}\\}_{\alpha}$ of _fast-growing complexity classes_ are
defined (the reader is referred to [schmitz2016hierar, Sec. 2] for detailed
definitions). What matters here is that to classify a problem in
$\mathbf{F}_{\alpha}$, it suffices to show that the complexity of every
instance is upper bounded by a function in $\mathfrak{F}_{\beta}$ for some
$\beta<\alpha$. Schmitz and Schnoebelen obtained the following length theorem
for Higman’s lemma.

[[schmitz2011, Thm. 5.3]] For any finite set $\Omega$, $m\in\mathbb{N}$, and
primitive recursive control function $g$, the length function
$L_{m\cdot\boldsymbol{\mathbf{\Omega}}^{\ast}}^{g}$ is upper bounded by a
function in $\mathfrak{F}_{\omega^{|{\Omega}|-1}}$.

A reflection is a map between nqo-sets that preserves bad sequences. Hence,
its existence implies the reverse transfer of the wqo-property and upper
bounding of length theorem. In the next subsection, we obtain a length theorem
for a nwqo over sequents in this way.

[Reflection] Let
$\mathbf{W}_{1}:=\left\langle{W_{1},\preccurlyeq_{1},{\llbracket}{\cdot}{\rrbracket}_{1}}\right\rangle$
and
$\mathbf{W}_{2}:=\left\langle{W_{2},\preccurlyeq_{2},{\llbracket}{\cdot}{\rrbracket}_{2}}\right\rangle$
be nqo-sets. A _reflection_ between $\mathbf{W}_{1}$ and $\mathbf{W}_{2}$ is a
mapping $f:W_{1}\to W_{2}$ such that, for all $a,b\in W_{1}$, $\text{if
}f(a)\preccurlyeq_{2}f(b),\text{then }a\preccurlyeq_{1}b$ and, for all $a\in
W_{1}$,
${\llbracket}{f(a)}{\rrbracket}_{2}\leq{\llbracket}{a}{\rrbracket}_{1}.$ We
write $\mathbf{W}_{1}{\;\hookrightarrow^{f}\;}\mathbf{W}_{2}$ (sometimes
omitting the superscript $f$).

[[schmitz2011, p. 446]] Whenever
$\mathbf{W}_{1}{\;\hookrightarrow\;}\mathbf{W}_{2}$, if $\mathbf{W}_{2}$ is a
nwqo, then so is $\mathbf{W}_{1}$; and if $g$ is a control function, then
$L_{\mathbf{W}_{1}}^{g}(t)\leq L_{\mathbf{W}_{2}}^{g}(t)$ for all
$t\in\mathbb{N}$.

###  4.2 A well-quasi-order over sequents based on weakening

Observe that the antecedent of the premise of the left-weakening rule
$\mathrm{(lw)}$ is obtainable from the antecedent of the conclusion by
deleting letters, and the succedents are identical. This motivates an nwqo
over sequents, for which we obtain a length theorem via a reflection into a
disjoint sum of Higman’s orderings. In what follows, let $\Sigma$ be an
arbitrary signature.

For finite $\Omega\subseteq\mathrm{Fm}_{\Sigma}(\mathcal{P})$, let
$\mathbf{W}_{\Sigma}(\Omega):=\left\langle{\mathsf{Seq}_{\Sigma}(\Omega),\rightsquigarrow_{\Sigma}^{\Omega},{\llbracket}{\cdot}{\rrbracket}}\right\rangle$,
where

  * 1.

$\mathsf{Seq}_{\Sigma}(\Omega)$ is the set of all $\Omega$-sequents over
$\mathrm{Fm}_{\Sigma}(\mathcal{P})$;

  * 2.

$\rightsquigarrow_{\Sigma}^{\Omega}\;\subseteq\mathsf{Seq}_{\Sigma}(\Omega)\times\mathsf{Seq}_{\Sigma}(\Omega)$
is such that $s_{1}\rightsquigarrow_{\Sigma}^{\Omega}s_{2}$ iff $s_{2}$ is
obtained by successive applications of $\mathrm{(lw)}$ starting from $s_{1}$;

  * 3.

${\llbracket}{\cdot}{\rrbracket}:\mathsf{Seq}_{\Sigma}(\Omega)\to\mathbb{N}$
is such that
${\llbracket}{{\Gamma}\Rightarrow{\Pi}}{\rrbracket}:={|}\Gamma{|}$ (i.e., the
length of the antecedent).

For all finite $\Omega\subseteq\mathrm{Fm}_{\Sigma}(\mathcal{P})$,
$\mathbf{W}_{\Sigma}(\Omega)$ is a nwqo; and if $g$ is primitive recursive,
then $L_{\mathbf{W}_{\Sigma}(\Omega)}^{g}$ is upper bounded by a function in
$\mathfrak{F}_{\omega^{|{\Omega}|-1}}$.

###### Proof.

Fix an enumeration $\varphi_{1},\ldots,\varphi_{m}$ of the formulas in
$\Omega$. Then the mapping
$f:\mathsf{Seq}_{\Sigma}(\Omega)\to(|{\Omega}|+1)\cdot\Omega^{\ast}$ such that
$f({\Gamma}\Rightarrow{}):=(0,\Gamma)$ and
$f({\Gamma}\Rightarrow{\varphi_{j}}):=(j,\Gamma)$ is a reflection; hence the
result follows from Thm. 4.1 and Lem. 4.1. ∎

###  4.3 Decision procedure for amenable sequent calculi

Fix an amenable sequent calculus $\mathbf{S}$ (see Def. 4) over a signature
$\Sigma$.

For $\mathcal{X}$ a formula, a sequent, or a sequent rule, let
$\langle{\mathcal{X}}\rangle$ be the length of the written representation of
$\mathcal{X}$. If $X$ is a finite set of formulas, of sequents, or of sequent
rules, let $\left\langle{X}\right\rangle:=\sum_{\mathcal{X}\in
X}\langle{\mathcal{X}}\rangle$ and
$\left\langle{}_{\mathsf{max}}\,{X}\right\rangle:=\max_{\mathcal{X}\in
X}\langle{\mathcal{X}}\rangle$. In particular,
$\left\langle{}_{\mathsf{max}}\,{\mathbf{S}}\right\rangle:=\max_{\mathsf{r}\in\mathbf{S}}\langle{\mathsf{r}}\rangle$
i.e., the largest among the representation lengths of the rules in the
calculus. The construction in this subsection extends the commutative setting
that appears in Balasubramanian et al. [BalLanRam21LICS]. For a finite set $D$
of sequents, define ${\llbracket_{{\mathsf{max}}}}{D}{\rrbracket}:=\max_{s\in
D}{\llbracket}{s}{\rrbracket}$ (${\llbracket}{s}{\rrbracket}$ is the length of
the antecedent of $s$, see Def. 4.2).

Let $\Omega$ be a finite set of formulas closed under subformulas and
$\mathcal{T}$ be a regular theory containing only $\Omega$-sequents. Define
$D_{0}$ as the set of minimal elements with respect to
$\rightsquigarrow_{\Sigma}^{\Omega}$ (i.e., not obtainable from another
element by repeated $\mathrm{(lw)}$) from the following finite set: the union
of $\mathcal{T}$ with the set of all instances of initial sequents in
$\mathbf{S}$ that satisfy the following:

  1. a)

formula-variables are instantiated to elements of $\Omega$;

  2. b)

succedent-variables are instantiated to an element in $\Omega$ or as empty;

  3. c)

sequence-variables are instantiated to the empty sequence.

Define $D_{i+1}:=D_{i}\cup\partial D_{i}$ ($i\geq 0$), where $\partial D_{i}$
is the set of $\Omega$-sequents $s$ satisfying:

  1. 1.

$s_{1}\cdots s_{k}/s$ is a rule instance of $\mathbf{S}$ such that, for all
$1\leq j\leq k$, there is ${s_{j}}{{}^{\prime}}\in D_{i}$ with
${s_{j}}{{}^{\prime}}\rightsquigarrow_{\Sigma}^{\Omega}~{}{s_{j}}$;

  2. 2.

the antecedent of $s$ has length
$\leq(\langle{\mathbf{S}}\rangle{\llbracket_{{\mathsf{max}}}}{D_{i}}{\rrbracket})\cdot\langle{\mathbf{S}}\rangle$;

  3. 3.

there is no $s^{\prime}\in D_{i}$ such that
$s^{\prime}\rightsquigarrow_{\Sigma}^{\Omega}s$.

The above construction yields a chain $D_{0}\subseteq D_{1}\subseteq\ldots$ of
sets of sequents. The following shows that the chain stabilizes at a finite
index. Indeed, if that were not the case, Def. 4.3 (3) forces the existence of
an infinite bad sequence $(s_{i})_{i<\omega}$ from $s_{i}\in D_{i}\setminus
D_{i-1}$ ($i<\omega$), and that is impossible.

$D_{i+1}$ is computable from $D_{i}$ and there is $N\in\mathbb{N}$ such that
$D_{N}=D_{N+i}$ for all $i\geq 0$.

###### Proof.

Each $D_{i}$ is computable because (a) there are only finitely-many rules in
$\mathbf{S}$, (b) finitely-many formulas in $\Omega$, (c) Def. 4.3 (2)
restricts the length of antecedents (thus there are only finitely-many rule
instances to consider), and (d) the relation
$\rightsquigarrow_{\Sigma}^{\Omega}$ is computable.

If there is some $N$ such that $D_{N}=D_{N+1}$ then, by the construction of
these sets, $D_{N}=D_{N+i}$ for every $i\geq 0$. Suppose that no such $N$
exists. It follows that $D_{0}\subset D_{1}\subset D_{2}\subset\ldots$. Choose
any $s_{i}\in D_{i}\setminus D_{i-1}$ for each $i\in\mathbb{N}$. By Def. 4.3
(3), $(s_{i})_{i<\omega}$ is an infinite bad sequence over
$\mathbf{W}_{\Sigma}(\Omega)$, contradicting that the latter is a wqo (Thm.
4.2). ∎

We now establish (Thm. 4.3) that every deducible sequent is obtainable by
weakening from a sequent at the stabilization point. First, a technical lemma.

If ${s^{\prime}}\rightsquigarrow_{\Sigma}^{\Omega}s$ with $s={L_{1}\cdots
L_{m}}\Rightarrow{\Pi}$, then there are sequences
$L^{\prime}_{1},\ldots,L^{\prime}_{m}$ such that
$s^{\prime}={L^{\prime}_{1}\cdots L^{\prime}_{m}}\Rightarrow{\Pi}$ and
$L^{\prime}_{i}\preccurlyeq_{\ast}L_{i}$ for all $1\leq i\leq m$.

###### Proof.

By induction on a deduction $\delta$ witnessing
${s^{\prime}}\rightsquigarrow_{\Sigma}^{\Omega}{L_{1}\cdots
L_{m}}\Rightarrow{\Pi}$. If it has a single node, the involved sequents are
the same, so take $L^{\prime}_{i}:=L_{i}$. In the inductive step, assume
$s={L_{1}\cdots L^{1}_{i}\varphi L^{2}_{i}\cdots L_{m}}\Rightarrow{\Pi}$ was
obtained by weakening from $s^{\prime\prime}={L_{1}\cdots
L^{1}_{i}L^{2}_{i}\cdots L_{m}}\Rightarrow{\Pi}$, where
$L_{i}=L^{1}_{i}L^{2}_{i}$. Then, by the (IH),
$s^{\prime}={L^{\prime}_{1}\cdots L^{\prime}_{i}\cdots
L^{\prime}_{m}}\Rightarrow{\Pi}$ with $L^{\prime}_{j}\preccurlyeq_{\ast}L_{j}$
for all $1\leq j\leq m$. In particular,
$L^{\prime}_{i}\preccurlyeq_{\ast}L_{i}^{1}L_{i}^{2}\preccurlyeq_{\ast}L_{i}^{1}\varphi
L_{i}^{2}$, and we are done. ∎

Let $\mathcal{T}\cup\\{s\\}$ be a finite set of $\Omega$-sequents such that
$\mathcal{T}$ is a regular theory (as in Def. 4.3). Then
$\mathcal{T}\vdash_{{\mathbf{S}}\mathsf{\Rightarrow}}s$ iff there is
$M\in\mathbb{N}$ such that $s^{\prime}\rightsquigarrow_{\Sigma}^{\Omega}s$ for
some $s^{\prime}\in D_{M}$.

###### Proof.

The left-to-right direction is the non-trivial one. Since $\mathbf{S}$ is
amenable, $\mathcal{T}\vdash_{{\mathbf{S}}\mathsf{\Rightarrow}}s$ is witnessed
by an analytic deduction $\delta$. We argue by induction on the structure of
$\delta$.

Base case. Then $\delta$ is a single node, so the node is a sequent in
$\mathcal{T}$ or an instance of an initial sequent. So $s$ is in $D_{0}$, or
$s$ is obtainable from the node by applications of $\mathrm{(lw)}$.

Inductive step. The last rule instance in $\delta$ is an instance $s_{1}\cdots
s_{k}/s$ of $\mathsf{r}$. Since each $s_{i}$ is an $\Omega$-sequent by virtue
of the deduction being analytic, by applying IH for each $1\leq i\leq k$,
there is $N_{i}\in\mathbb{N}$ with
${s^{\prime}_{i}}\rightsquigarrow_{\Sigma}^{\Omega}s_{i}$ for some
${s^{\prime}_{i}}\in D_{N_{i}}$. Let $M:=\max_{i}N_{i}$, which gives us
$s^{\prime}_{i}\in D_{M}$ for all $1\leq i\leq k$. Hence Def. 4.3 (1) is
satisfied for $s$. The situation is the following.

$\quad\qquad s^{\prime}_{1}\in D_{M}$ $\rightsquigarrow_{\Sigma}^{\Omega}$
$s_{1}$ $\;\cdots$ $\rightsquigarrow_{\Sigma}^{\Omega}$ $\;\cdots$
$\quad\qquad s^{\prime}_{k}\in D_{M}$ $\rightsquigarrow_{\Sigma}^{\Omega}$
$s_{k}$ $\mathsf{r}$ $s$

We now show by cases that there is $s^{\prime}\in D_{M+1}$ such that
$s^{\prime}\rightsquigarrow_{\Sigma}^{\Omega}s$.

If Def. 4.3 (2) is satisfied, then $s\in D_{M+1}$, or (due to Def. 4.3 (3))
there is some $s^{\prime}\in D_{M+1}$ such that
$s^{\prime}\rightsquigarrow_{\Sigma}^{\Omega}s$. In either case we are done,
so assume that Def. 4.3 (2) fails. Thus $s$ has antecedent of length
$>(\langle{\mathbf{S}}\rangle{\llbracket_{{\mathsf{max}}}}{D_{M}}{\rrbracket})\cdot\langle{\mathbf{S}}\rangle$.
Thus there are sequence-variables $\Gamma_{1},\ldots,\Gamma_{m}$ ($m>0$) in
the conclusion of $\mathsf{r}$ instantiated with sequences of length
$>\langle{\mathbf{S}}\rangle{\llbracket_{{\mathsf{max}}}}{D_{M}}{\rrbracket}$
(if $m=0$ then the antecedent would be instantiations of formula-variables and
hence its length would be
$\leq\langle{\mathbf{S}}\rangle{\llbracket_{{\mathsf{max}}}}{D_{0}}{\rrbracket}$).
Assume wlog that $\Gamma_{1},\ldots,\Gamma_{m^{\prime}}$ with $m^{\prime}\leq
m$ appear in the premises of $\mathsf{r}$, while the other variables appear
exclusively in the conclusion.

Write $s_{i}={L_{i1}\cdots L_{iu_{i}}}\Rightarrow{\Pi_{i}}$ and
$s_{i}^{\prime}={L_{i1}^{\prime}\cdots
L^{\prime}_{i{u_{i}}}}\Rightarrow{\Pi_{i}}$ where each $L_{i}$ is an
instantiation of a sequence-variable or a singleton sequence of a formula,
such that $L^{\prime}_{ij}\preccurlyeq_{\ast}L_{ij}$ for each $1\leq j\leq
u_{i}$ (the existence of such sequences is guaranteed by Lem. 4.3). The length
of $L_{i1}^{\prime}\cdots L_{iu_{i}}^{\prime}$ is
$\leq{\llbracket_{{\mathsf{max}}}}{D_{M}}{\rrbracket}$ by the fact that
$s_{i}^{\prime}\in D_{M}$, hence each $L_{ij}^{\prime}$ has length
$\leq{\llbracket_{{\mathsf{max}}}}{D_{M}}{\rrbracket}$.

We construct a new instance $I^{\prime}$ of $\mathsf{r}$, with premises
$s^{\prime\prime}_{i}$ instead of $s_{i}$, and a conclusion $s^{\prime}$ whose
antecedent has size satisfying Def. 4.3(2), and
$s^{\prime}\rightsquigarrow_{\Sigma}^{\Omega}s$:

$\quad\qquad s^{\prime}_{1}\in D_{M}$ $\rightsquigarrow_{\Sigma}^{\Omega}$
$s^{\prime\prime}_{1}$ $\;\cdots$ $\rightsquigarrow_{\Sigma}^{\Omega}$
$\;\cdots$ $\quad\qquad s^{\prime}_{k}\in D_{M}$
$\rightsquigarrow_{\Sigma}^{\Omega}$ $s^{\prime\prime}_{k}$ $\mathsf{r}$
$s^{\prime}$ (smaller than $s$)

Construct $I^{\prime}$ by consideration of where each $\Gamma_{j}$ ($1\leq
j\leq m^{\prime}$) occurs. For $\Gamma_{j}$ occurring in a single premise,
instantiate it with the sequence $L^{\prime}_{jl}$ instead of the $L_{jl}$
that was used before.

For each $\Gamma_{j}$ ($1\leq j\leq m^{\prime}$) occurring in multiple
premises, we need a single instantiation that can be used for each occurrence
(reflecting the fact that we are dealing with additive rules here). Without
loss of generality, assume that $s_{1},\ldots,s_{l}$ are all the premises
where $\Gamma_{j}$ occurs. Assume that $\Gamma_{j}$ was instantiated with the
sequence $L$. Let $L_{1{j_{1}}},\ldots,L_{l{j_{l}}}$ be the sequences in these
premises that instantiate $\Gamma_{j}$ (each is equal to $L$). We want a
subsequence of $L$ reachable by weakening from each
$L^{\prime}_{1{j_{1}}},\ldots,L^{\prime}_{l{j_{l}}}$ (these need not be
identical): start with $L$ and cross off each of the sequences
$L^{\prime}_{1{j_{1}}},\ldots,L^{\prime}_{l{j_{l}}}$ (letter by letter,
respecting the order). Use the sequence crossed-off to instantiate
$\Gamma_{j}$. It has size $\leq
k\cdot{\llbracket_{{\mathsf{max}}}}{D_{M}}{\rrbracket}<\langle{\mathbf{S}}\rangle\cdot{\llbracket_{{\mathsf{max}}}}{D_{M}}{\rrbracket}$.

Finally, for sequence-variables that appear only in the conclusion of the
rule, i.e., $\Gamma_{m^{\prime}+1},\ldots,\Gamma_{m}$, instantiate each of
these with the empty sequence.

The new instantiation $I^{\prime}$ has premises $s^{\prime\prime}_{i}$ where
$s^{\prime}_{i}\rightsquigarrow_{\Sigma}^{\Omega}s^{\prime\prime}_{i}$ for
each $1\leq i\leq k$, and its conclusion is
$s^{\prime}\rightsquigarrow_{\Sigma}^{\Omega}s$ since the instantiation of
each $\Gamma_{j}$ is a subsequence of the original instantiation. Moreover,
the number of variables in the conclusion of $\mathsf{r}$ is
$<\langle{\mathbf{S}}\rangle$ and each variable instantiation under
$I^{\prime}$ has size
$<\langle{\mathbf{S}}\rangle{\llbracket_{{\mathsf{max}}}}{D_{M}}{\rrbracket}$.
Hence it follows that $s^{\prime}\in D_{M+1}$ or there is some
$s^{\prime}_{0}\in D_{M}$ with
$s^{\prime}_{0}\rightsquigarrow_{\Sigma}^{\Omega}s^{\prime}$. In either case,
the claim is proved.∎

###  4.4 Complexity analysis

The fast-growing complexity classes are closed under exponentiation so the
distinction between space and time (also determinism and non-determinism) is
unimportant [schmitz2016hierar]. We undertake a space analysis of the
algorithm based on Thm. 4.3 and Thm. 4.3. It suffices to write down each
$D_{i}$ in turn at the same location, computing each rule instance in turn;
when the stabilization index $D_{N}$ is reached, check whether
$s^{\prime}\rightsquigarrow_{\Sigma}^{\Omega}s$ for some $s^{\prime}\in
D_{N}$. Each $D_{i}\subseteq D_{N}$, and writing down a rule instance takes
space bounded by the size of an element from
$D_{N}^{\langle{\mathbf{S}}\rangle}\times D_{N}$. So the space requirements
are an elementary function in $|{D_{N}}|$ and the size of an element from
$D_{N}$. We upper bound each of these.

Let $\mathcal{T}$ be a regular theory, $s$ be a sequent and
$\Omega:=\mathsf{subf}(\mathcal{T}\cup\\{s\\})$.

  1. 1.

$|{\Omega}|\leq\langle{s}\rangle+\left\langle{\mathcal{T}}\right\rangle$;

  2. 2.

if $s^{\prime}\in D_{i}$ then
${\llbracket}{s^{\prime}}{\rrbracket}<(\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle^{2i+1}$,
and
${\llbracket_{{\mathsf{max}}}}{D_{i}}{\rrbracket}<(\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle^{2i+1}$;

  3. 3.

if $s^{\prime}\in D_{i}$ then
$\langle{s^{\prime}}\rangle<4(\left\langle{\mathcal{T}}\right\rangle+\langle{s}\rangle)^{2}\langle{\mathbf{S}}\rangle^{2N+1}$;

  4. 4.

for all $i\geq 0$,
$|{D_{i}}|<E(\left\langle{\mathcal{T}}\right\rangle+\langle{s}\rangle,N)$ for
$E$ an elementary function (i.e., in $\mathfrak{F}_{2}$).

###### Proof.

  1. 1.

It is easy to see by structural induction that
$|{\mathsf{subf}(\varphi)}|\leq\langle{\varphi}\rangle$ for all formulas
$\varphi$. Then, for any sequent
$t:={\psi_{1},\ldots,\psi_{m}}\Rightarrow{\Pi}$, we have
$|{\mathsf{subf}(t)}|\leq|{\mathsf{subf}(\Pi)}|+\sum_{i=1}^{m}|{\mathsf{subf}(\psi_{i})}|\leq\langle{\Pi}\rangle+\sum_{i=1}^{m}\langle{\psi_{i}}\rangle\leq\langle{t}\rangle$.
The result then follows because
$|{\Omega}|\leq|{\mathsf{subf}(s)}|+\sum_{t\in\mathcal{T}}|{\mathsf{subf}(t)}|\leq\langle{s}\rangle+\left\langle{\mathcal{T}}\right\rangle$.

  2. 2.

By induction on $i\geq 0$. Note that if $s^{\prime}\in D_{0}$, since $D_{0}$
is a subset of the union of $\mathcal{T}$ and instantiations from $\Omega$ of
initial sequents in $\mathbf{S}$,
${\llbracket}{s^{\prime}}{\rrbracket}<{\llbracket_{{\mathsf{max}}}}{\mathcal{T}}{\rrbracket}+\langle{\mathbf{S}}\rangle\leq({\llbracket_{{\mathsf{max}}}}{\mathcal{T}}{\rrbracket}+1)\langle{\mathbf{S}}\rangle\leq(\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle$.
Inductive step: if $s^{\prime}\in D_{i+1}$, then
${\llbracket}{s^{\prime}}{\rrbracket}<\langle{\mathbf{S}}\rangle^{2}{\llbracket_{{\mathsf{max}}}}{D_{i}}{\rrbracket}<\langle{\mathbf{S}}\rangle^{2}(\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle^{2i+1}=(\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle^{2(i+1)+1}$.

Since ${\llbracket_{{\mathsf{max}}}}{D}{\rrbracket}=\max_{s\in
D}{\llbracket}{s}{\rrbracket}$, it follows that
${\llbracket_{{\mathsf{max}}}}{D_{i}}{\rrbracket}<(\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle^{2i+1}$.

  3. 3.

It is enough to observe that $\langle{s^{\prime}}\rangle$ is upper bounded by
the sum of the sizes of each formula in the antecedent, plus 1 for each comma,
plus 1 to account for the sequent symbol, plus the size of the succedent. This
gives us
$\langle{s^{\prime}}\rangle\leq{\llbracket}{s^{\prime}}{\rrbracket}\langle{\Omega}\rangle+{\llbracket}{s^{\prime}}{\rrbracket}+1+\langle{\Omega}\rangle\leq
4({\llbracket}{s^{\prime}}{\rrbracket}+1)\langle{\Omega}\rangle$. From the
previous items, the latter is $\leq
4((\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle^{2N+1}+1)(\langle{s}\rangle+\left\langle{\mathcal{T}}\right\rangle)\leq
4((\left\langle{\mathcal{T}}\right\rangle+\langle{s}\rangle)\langle{\mathbf{S}}\rangle^{2N+1})(\langle{s}\rangle+\left\langle{\mathcal{T}}\right\rangle)$
where we have used that $\langle{s}\rangle\geq 2$ and
$\langle{\mathbf{S}}\rangle\geq 1$.

  4. 4.

Let $\eta,\rho\in\mathbb{N}$. Then define $\big{[}\begin{smallmatrix}{\eta}\\\
{\rho}\end{smallmatrix}\big{]}_{\mathsf{seq}}:=(\sum_{l=0}^{\rho}\eta^{l})\cdot(\eta+1)\leq(\eta+1)^{\rho+1}\cdot(\eta+1)$,
the number of distinct sequents over $\eta$ formulas and having norm
$\leq\rho$. Note that
$|{D_{0}}|\leq\big{[}\begin{smallmatrix}{\langle{s}\rangle+\left\langle{\mathcal{T}}\right\rangle}\\\
{\langle{s}\rangle+\left\langle{\mathcal{T}}\right\rangle}\end{smallmatrix}\big{]}_{\mathsf{seq}}$
and $|{D_{i+1}}|\leq\big{[}\begin{smallmatrix}{|{\Omega}|}\\\
{\langle{\mathbf{S}}\rangle^{2}{\llbracket_{{\mathsf{max}}}}{D_{i}}{\rrbracket}}\end{smallmatrix}\big{]}_{\mathsf{seq}}<\big{[}\begin{smallmatrix}{\langle{s}\rangle+\left\langle{\mathcal{T}}\right\rangle}\\\
{\langle{\mathbf{S}}\rangle^{2}(\left\langle{\mathcal{T}+1)}\right\rangle\langle{\mathbf{S}}\rangle^{2N+1}}\end{smallmatrix}\big{]}_{\mathsf{seq}}\leq\big{[}\begin{smallmatrix}{\langle{s}\rangle+\left\langle{\mathcal{T}}\right\rangle}\\\
{\langle{\mathbf{S}}\rangle^{2}(\langle{s}\rangle+\left\langle{\mathcal{T}}\right\rangle)\langle{\mathbf{S}}\rangle^{2N+1}}\end{smallmatrix}\big{]}_{\mathsf{seq}}$.
Thus, for all $i\geq 0$,
$|{D_{i}}|<E(\langle{s}\rangle+\left\langle{\mathcal{T}}\right\rangle,N)$ for
$E$ an elementary function (i.e. in $\mathfrak{F}_{2}$).∎

Deciding whether $\mathcal{T}\vdash_{{\mathbf{S}}\mathsf{\Rightarrow}}s$ for a
regular theory $\mathcal{T}$ is in HAck.

###### Proof.

Lem. 4.4 (4) shows that
$|{D_{N}}|<E_{1}(\left\langle{\mathcal{T}}\right\rangle+\langle{s}\rangle,N)$,
for an elementary function $E_{1}$. Also, Lem. 4.4 (3) shows that that
$s^{\prime}\in D_{N}$ implies that its size $\langle{s^{\prime}}\rangle$ is
bounded by
$E_{2}(\left\langle{\mathcal{T}}\right\rangle+\langle{s}\rangle,N)$, for an
elementary function $E_{2}$. It remains to upper bound $N$, and it is this
that forces the fast-growing complexity. Let
$\Omega:=\mathsf{subf}(\mathcal{T}\cup\\{s\\})$. In the proof of Thm. 4.3, we
extracted a bad sequence $(s_{i})_{i\leq N}$ over
$\mathbf{W}_{\Sigma}(\Omega)$ from the chain of sets
$D_{0}\subset\ldots\subset D_{N}$ by choosing any $s_{i}\in D_{i}\setminus
D_{i-1}$. We claim that this bad sequence is $(g,n)$-controlled for the
control function $g(x):=\langle{\mathbf{S}}\rangle^{2}x$ and
$n:=(\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle$,
allowing us to conclude that $N\leq L_{\mathbf{W}_{\Sigma}(\Omega)}^{g}(n)\leq
L_{\mathbf{W}_{\Sigma}(\Omega)}^{g}((\left\langle{\mathcal{T}}\right\rangle+\langle{s}\rangle)\langle{\mathbf{S}}\rangle)$.
By induction on $i$. _Base case_ : $s_{0}\in D_{0}$, so Lem. 4.4(2) yields
${\llbracket}{s_{0}}{\rrbracket}<(\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle$.
_Inductive step_ :
${\llbracket}{s_{i+1}}{\rrbracket}<(\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle^{2(i+1)+1}=\langle{\mathbf{S}}\rangle^{2}(\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle^{2i+1}=\langle{\mathbf{S}}\rangle^{2}g^{i}(\left\langle{\mathcal{T}}\right\rangle+1)\langle{\mathbf{S}}\rangle)=g^{i+1}(n)$,
so we are done. So the space to run the algorithm is a composition of
elementary functions with a function in $\mathfrak{F}_{\omega^{|{\Omega}|-1}}$
by Thm. 4.2, thus it is bounded by a function in
$\mathfrak{F}_{\omega^{|{\Omega}|-1}}$. So, for this particular $|{\Omega}|$,
the problem is in $\mathbf{F}_{\omega^{|{\Omega}|}}$. As $\Omega$ varies with
the input, we wish to eliminate its dependence. Upper bounding over all
$\Omega$, we have that the problem is in
$\mathbf{F}_{\omega^{\omega}}=\textsc{HAck}$. ∎

Any subcalculus of $\mathbf{FL}_{\mathbf{w}}$ containing $\mathrm{(lw)}$ has
deducibility in HAck. This holds in particular for
$\mathbf{FL}_{\mathbf{w}}^{\Sigma}$ for any
$\Sigma\subseteq\Sigma_{\mathbf{FL}}$.

##  5 Final considerations

Combining Sec. 3 and Sec. 4, we finally obtain the promised result:

Theorem 1 (Main theorem)._For
$\\{\otimes,{\setminus},0,1\\}\subseteq\Sigma\subseteq\Sigma_{\mathbf{FL}}$,
deducibility in $\mathbf{FL}_{\mathbf{w}}^{\Sigma}$ is HAck-complete. In
particular, $\mathbf{FL}_{\mathbf{w}}{}$ and its multiplicative fragment
$\mathbf{L}_{\mathbf{w}}{}$ are HAck-complete. _

#### Complexity of the word problem in integral FL-algebras

Let $\mathsf{V}$ be an equational class of algebras (a _variety_) over a
signature $\Sigma$. The _word problem of $\mathsf{V}$_ [GalJipKowOno07, Sec.
4.4.2] asks whether, given fixed finite sets of variables $X$ (generators) and
equations $E$ over $\mathrm{Fm}_{\Sigma}(X)$, the quasiequation
$\&E{\implies}e$ is valid in $\mathsf{V}$, where $e$ is an equation over
$\mathrm{Fm}_{\Sigma}(X)$. Note that deciding this problem allows for one
algorithm per pair $(X,E)$, as opposed to deciding the _quasiequational theory
of $\mathsf{V}$_, which asks for a single algorithm that applies to every
$(X,E)$. In view of the algebraizability of
$\vdash_{\mathbf{FL}_{\mathbf{w}}{}}$ [GalJipKowOno07, Sec. 2.6] w.r.t. the
variety of integral zero-bounded FL-algebras $\mathsf{FL_{w}}$, our results
imply that the word problem and the quasiequational theory of
$\mathsf{FL_{w}}$ are HAck-complete. In fact, because
$\mathsf{Props}(\mathcal{L})$ (cf. Def. 3.2) is a finite set of generators and
${\mathcal{T}(\mathcal{L})}^{\to}$ (cf. Def. 3.2) is a finite set of formulas
over $\mathrm{Fm}_{\Sigma_{\mathbf{FL}}}(\mathsf{Props}(\mathcal{L}))$, we
have that the word problem in this variety is HAck-hard. The quasiequational
theory is in HAck in view of the proof search procedure in the previous
section. Since the word problem reduces to the quasiequational theory, we
obtain that both problems are HAck-complete. This also applies to integral FL-
algebras and integral residuated lattices since the constant $0$ does not play
any essential role in the arguments.

#### Non-existence of deduction theorem

Our lower bounds imply that fragments of $\mathbf{FL}_{\mathbf{w}}$ covered by
Thm. 3.2 have no deduction theorem (DT); else deducibility would reduce to
provability, yet provability in these logics is PSpace.

#### Upper bound for axiomatic extensions

The obtained upper-bounds apply to deducibility for $\mathcal{N}_{2}$-analytic
structural rule extensions of $\mathbf{FL}_{\mathbf{w}}$, and to the
corresponding axiomatic extensions (refer to the substructural hierarchy
[CiaGalTer17]).

#### Undecidability of deducibility in $\mathbf{FL}$

The encoding in Sec. 3.2 offers a new proof of the undecidability of the
deducibility problem in $\mathbf{FL}$ (remove lossiness; reachability in
channel systems is undecidable). This might be useful to prove undecidability
of deducibility in some axiomatic extensions of $\mathbf{FL}$.

## References

  * [1] W. J. Blok, C. J. V. Alten, On the finite embeddability property for residuated ordered groupoids, Transactions of the American Mathematical Society 357 (10) (2005) 4141–4157.
  * [2] P. Jipsen, C. Tsinakis, A Survey of Residuated Lattices, Springer US, Boston, MA, 2002, pp. 19–56.  doi:10.1007/978-1-4757-3627-4_3.
  * [3] R. Horčík, K. Terui, Disjunction property and complexity of substructural logics, Theoretical Computer Science 412 (31) (2011) 3992–4006.  doi:https://doi.org/10.1016/j.tcs.2011.04.004.
  * [4] P. Lincoln, J. Mitchell, A. Scedrov, N. Shankar, Decision problems for propositional linear logic, Annals of Pure and Applied Logic 56 (1) (1992) 239–311.  doi:https://doi.org/10.1016/0168-0072(92)90075-B.
  * [5] A. Urquhart, The complexity of decision procedures in relevance logic II, The Journal of Symbolic Logic 64 (4) (1999) 1774–1802.
  * [6] S. Schmitz, P. Schnoebelen, Multiply-recursive upper bounds with Higman’s Lemma, in: L. Aceto, M. Henzinger, J. Sgall (Eds.), Automata, Languages and Programming, Springer Berlin Heidelberg, Berlin, Heidelberg, 2011, pp. 441–452.
  * [7] H. Tanaka, Tower-complete problems in contraction-free substructural logics, in: B. Klin, E. Pimentel (Eds.), 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland, Vol. 252 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, pp. 34:1–34:19.
  * [8] K. Chvalovský, R. Horčík, Full Lambek calculus with contraction is undecidable, The Journal of Symbolic Logic 81 (2) (2016) 524–540.
  * [9] N. Galatos, H. Ono, Cut elimination and strong separation for substructural logics: An algebraic approach, Annals of Pure and Applied Logic 161 (9) (2010) 1097–1133.  doi:10.1016/j.apal.2010.01.003.
  * [10] S. Schmitz, Complexity hierarchies beyond elementary, ACM Trans. Comput. Theory 8 (1) (feb 2016).  doi:10.1145/2858784.
  * [11] R. Péter, Recursive Functions, Academic Press, 1967.
  * [12] P. Chambart, P. Schnoebelen, The ordinal recursive complexity of lossy channel systems, in: 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 2008, pp. 205–216.  doi:10.1109/LICS.2008.47.
  * [13] A. R. Balasubramanian, T. Lang, R. Ramanayake, Decidability and complexity in weakening and contraction hypersequent substructural logics, in: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, IEEE, 2021, pp. 1–13.  doi:10.1109/LICS52264.2021.9470733.
  * [14] G. Higman, Ordering by divisibility in abstract algebras, Proceedings of the London Mathematical Society s3-2 (1) (1952) 326–336.  doi:https://doi.org/10.1112/plms/s3-2.1.326.
  * [15] A. Ciabattoni, N. Galatos, K. Terui, Algebraic proof theory: Hypersequents and hypercompletions, Ann. Pure Appl. Logic 168 (3) (2017) 693–737.  doi:10.1016/j.apal.2016.10.012.
  * [16] N. Galatos, P. Jipsen, T. Kowalski, H. Ono, Residuated lattices: an algebraic glimpse at substructural logics, Vol. 151 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2007.
  * [17] D. Brand, P. Zafiropulo, On communicating finite-state machines, J. ACM 30 (2) (1983) 323–342.  doi:10.1145/322374.322380.
  * [18] P. Schnoebelen, Verifying lossy channel systems has nonprimitive recursive complexity, Information Processing Letters 83 (5) (2002) 251–261.  doi:10.1016/S0020-0190(01)00337-4.
  * [19] L. E. Dickson, Finiteness of the odd perfect and primitive abundant numbers with $n$ distinct prime factors, American Journal of Mathematics 35 (4) (1913) 413–422.
  * [20] S. Schmitz, P. Schnoebelen, Algorithmic Aspects of WQO Theory, lecture (Aug. 2012).
  * [21] D. Figueira, S. Figueira, S. Schmitz, P. Schnoebelen, Ackermannian and primitive-recursive bounds with Dickson’s Lemma, in: Proceedings - Symposium on Logic in Computer Science, 2011, pp. 269–278.  doi:10.1109/LICS.2011.39.