Bouncing threads for infinitary and circular proofs

with title note

David Baelde

ENS Paris-Saclay

Amina Doumane

CNRS, LIP, ENS Lyon

Denis Kuperberg

CNRS, LIP, ENS Lyon

Alexis Saurin

CNRS, IRIF, Université Paris Diderot

We generalize the validity criterion for the infinitary proof system of the multiplicative additive linear logic with fixed points. Our criterion is designed to take into account axioms and cuts. We show that it is sound and enjoys the cut elimination property. We finally study its decidability properties, and prove that it is undecidable in general but becomes decidable under some restrictions.

<concept_desc>Software and its engineering General programming languages</concept_desc>
<concept_desc>Social and professional topics History of programming languages</concept_desc>

[500]Software and its engineering General programming languages
[300]Social and professional topics History of programming languages

§ INTRODUCTION

Infinitary (non-wellfounded) and circular proof systems have received much
attention in recent years.
Such proof systems allow non-wellfounded proof trees and impose some global
validity condition in order to ensure soundness. Typically, it requires that
every infinite branch is supported by some thread which traces some
formula in a bottom-up manner and witnesses infinitely many progress points of
a coinductive property.

Unfortunately, existing notions of validity impose a quite limited use of cuts
in non-wellfounded proofs and many proofs that could be accepted as valid
are rejected.
This paper introduces a new validity condition for ,
the infinitary proof system for multiplicative linear logic with fixed
points. This criterion generalizes the existing one, taking inspiration from
Geometry of Interaction, enriching the structure of threads and relaxing their
geometry: bouncing threads can leave the branch they validate and “bounce”
(i.e. change direction, moving upward but also downward along proof
branches) on axioms and cut rules.

We define a new bouncing validity condition in the multiplicative
fragment and show that the obtained proofs enjoy cut elimination.
This new validity condition is undecidable but can be decomposed into an
infinite hierarchy of decidable conditions. Moreover, it naturally extends
to a validity condition ensuring cut elimination for the multiplicative
and additive fragment.
en rajoutant quelques citations le paragraphe ci dessus est suffisant pour faire une intro

Organization of the contributions.
In Section <ref> we recall the basic definitions for the non-wellfounded proof system .
We then define, in <ref> the cut-elimination procedure. In <ref>, we introduce our new bouncing validity
condition, and show in <ref> that it guarantees soundness of the system and productivity of the cut-elimination procedure. We finally study in <ref> the decidability of our criterion in the multiplicative case.

§ INTRODUCTION

-  add reference to Mints continuous cut elimination

- take examples into account

- develop motivation
Fixed point theory has proved to be a valuable tool in computer
science, in particular for reasoning formally about software systems.

It is pervasive in programming language semantics,
concurrency, automata theory and software verification techniques.

In the setting of fixed-point logics, infinitary (ie. non-wellfounded) and circular
proof systems <cit.> have received much
attention in recent years.
Such proof systems allow non-wellfounded proof trees and impose some global
validity condition in order to ensure soundness. Typically, it requires that
every infinite branch is supported by some thread tracing some
formula in a bottom-up manner and witnessing infinitely many progress points of
a coinductive property.

[inline]Fixed points are also present in most programming languages as
recursive types. More interestingly, the Curry-Howard correspondence,
which allows to view proofs as programs and formulas as types,
has been extended in various ways to encompass fixed point types,
e.g. in System F extended with least and greatest fixed point
types <cit.>,
in Coq's calculus of (co)inductive constructions <cit.>,
and in typing disciplines for functional reactive programming
based on the linear-time $\mu$-calculus <cit.>.

On the programming side of the Curry-Howard correspondence,
fixed-point formulas correspond to inductive and coinductive types:
one finds programming languages equipped with
(co)recursion constructs whose typing naturally reflects the Kozen-Park
(co)induction rules <cit.>.
Writing programs in these systems may be difficult, as it involves
coming up with complex (co)invariants. These difficulties are only
partially lifted through the use of guarded
(co)recursion or sized types <cit.>
in Coq or Agda respectively.
Furthermore, (co)recursion involves a suspended computation which makes it
difficult to analyze the behavior of a program.
As an alternative, one could naturally consider infinitary (or circular)
programs, equipped with a global validity condition ensuring that
they behave well – in particular that they are terminating, or productive
for inhabitants of coinductive types.
There is surprisingly little work following this approach[
We note the work of Hyvernat <cit.> whose use of
size-change termination can be seen as a form of validity checking.
It would be interesting to

precisely compare it with our style of circular
proof systems.
], and
foundations are missing.

This lack of studies can be understood from the fact that the aforementioned
infinitary proof systems for fixed point logics are all cut-free; hence,
the role of the validity condition in (syntactic) cut-elimination remains
unclear from these works. This shortcoming has been addressed first by Santocanale
and Fortier: in <cit.> they consider an infinitary sequent
calculus for purely additive logic, featuring cuts and an extended
notion of validity, and they show that cuts can be eliminated from valid
proofs – in that setting, cut-elimination is not terminating but productive,
and converges to a (valid) cut-free derivation.
A key insight of this work is that the same validity condition that ensures
soundness in infinitary proof systems also ensures the productivity of
The result has been generalized later to the multiplicative and additive linear
logic, at the cost of a more complex argument, by Baelde, Doumane and Saurin

Through these syntactic cut-elimination results, infinitary proofs for
the multiplicative-additive $\mu$-calculus are given a computational
content, which is an important first step towards an interesting Curry-Howard
correspondence for that logic.

Unfortunately, existing notions of validity impose a quite limited use of cuts
in non-wellfounded proofs and many proofs that could be accepted as valid
are rejected.
In particular, this prevents writing circular proofs in a compositional manner, as exemplified in the following (supported by Figure <ref>):

\begin{prooftree}
\vspace{1cm}
\Hypo{\begin{array}{c}
\end{array}}
\Infer{1}[\rax]{N \vdash N}
\Hypo{%\star}
\orig{introa}S \vdash S}
\Infer{2}[\rotimesr]{N,S\vdash N\tensor S}
\Infer{1}[\rotimesl]{N \tensor S\vdash N\tensor S}
%  \Hypo{Succ}
%  \Infer{1}{N\tensor S\vdash N\tensor S}
%  \Infer{2}[\rcut]{N\tensor S\vdash N\tensor S}
\Infer{1}[\rnul]{S\vdash N\tensor S}
\Infer{1}[\rnur]{S\vdash S}
\Infer{1}[\rweaknatl]{N, S\vdash S}
\Infer{1}[\rotimesl]{N \tensor S\vdash S}
\Infer{1}[\rnul]{
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (introb) {\ensuremath{}};
\draw [->,>=latex] (introa.north) .. controls +(130:4.8cm) and +(180:1.5cm) .. (introb.west);
\end{tikzpicture}~ S\vdash S
\end{prooftree}
&  \qquad
\begin{prooftree}
\Infer{0}[\rax]{N \vdash N}
\Hypo{
\orig{introc}S \vdash S}
\Infer{2}[\rotimesr]{N,S\vdash N\tensor S}
\Infer{1}[\rotimesl]{N \tensor S\vdash \underline{N\tensor S}}
%    \Hypo{Succ}
%    \Infer{1}{N\tensor S\vdash N\tensor S}
%    \Hypo{Succ}
\Hypo{\scalebox{.8}{\fbox{\begin{prooftree}\Infer{0}[\rax]{N\vdash N}
\Infer{1}[\roplusrr, \rmur]{N\vdash N}
\Infer{0}[\rax]{S\vdash S}
\Infer{2}[\rotimesl,\rotimesr]{\underline{N\tensor S}\vdash N\tensor S}
\end{prooftree}}}}
\Infer{2}[\rcut]{N\tensor S\vdash N\tensor S}
\Infer{1}[\rnul]{S\vdash N\tensor S}
\Infer{1}[\rnur]{S\vdash S}
\Infer{1}[\rweaknatl]{N, S\vdash S}
\Infer{1}[\rotimesl]{N \tensor S\vdash S}
\Infer{1}[\rnul]{
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (introd) {\ensuremath{}};
\draw [->,>=latex] (introc.north) .. controls +(150:5.8cm) and +(160:4.5cm) .. (introd.west);
\end{tikzpicture}~S\vdash S}

\end{prooftree}
\end{array}$}
Example of a valid and an invalid circular pre-proof.

Consider formulas $N =\mu X. 1 \oplus X$ and $S = \nu Y. N\otimes Y$ respectively encoding natural numbers and streams of natural numbers in .
Figure <ref> presents two circular derivation trees, in the two-sided version of sequent calculus[We follow this convention for the example in order to exhibit more clearly the computational interpretation, even though the rest of the paper will be developed in the one-sided sequent calculus which is more concise.]. The computational interpretation of left-hand derivation is that of a function from streams of nats to streams of nats which drops its elements in odd position, keeping half of its elements only[Notice that natural numbers are erasable and duplicable as inputs in , hence the use of the $\rweaknatl$ admissible rule.].
The rightmost proof has a slightly different computational interpretation: it drops one element every two but also increments the element it keeps in the output streams. This is achieved by using a cut with a proof precisely doing this increment (depicted in the box).
Although the leftmost proof is valid, the rightmost one is not for the validity condition introduced in <cit.>: indeed, the cut that is introduced belongs to a cycle and as a result, no valid thread inhabits the infinite branch.

These examples correspond (at a somehow informal level) to the Coq coinductive terms drop and incdrop of Fig. <ref>.

CoInductive Stream := Cons : nat -> Stream -> Stream.
CoFixpoint drop (s : Stream) : Stream := match s with
| Cons a (Cons b s') => Cons b (drop s') end.
Definition hdinc (s: Stream) : Stream := match s with
| Cons a s' => Cons (S a) s' end.
CoFixpoint incdrop (s : Stream) : Stream := match s with
| Cons a (Cons b s') => hdinc (Cons a (incdrop s')) end.
CoInductive BStream := BCons : bool -> BStream -> BStream.
Definition neghd (s: BStream) : BStream := match s with
| BCons a s' => BCons (negb a) s' end.
Definition k := 3.
CoFixpoint filter1everyk (m : nat) (s : BStream) : BStream :=
match (m,s) with
| (0,BCons a s') => BCons a (filter1everyk k s')
| (S m',BCons a s') => neghd (filter1everyk m' s')  end.

Guarded and non-guarded examples of coinductive definitions.

The present paper contributes to a line of research aiming at
providing and analyzing the computational content of circular
and non-wellfounded proofs, and improving their compositionality
of circular proofs.
From the Curry-Howard perspective, considering more relaxed validity
criteria is an interesting and important challenge as it affords a more
flexible way in constructing
circular proofs that, through the lense of Curry-Howard, more
flexibility to write valid programs on coinductive types.

Indeed, while our previous cut-elimination result <cit.>
is a significant step it goes only half-way due to
strong restrictions on the use of cuts along non-wellfounded
branches (or cycles in proofs) as described above.
We  introduce here a new validity condition for ,
the infinitary proof system for multiplicative additive linear logic with fixed
points. Taking inspiration from Geometry of Interaction <cit.>,  this criterion generalizes the existing one by enriching the structure of threads and relaxing their
geometry: bouncing threads can leave the branch they validate and “bounce”
(i.e. change direction, moving upward but also downward along proof
branches) on axioms and cut rules.

We define a new bouncing validity condition in the multiplicative
fragment and show that the obtained proofs enjoy cut elimination and soundness.
This new validity condition is undecidable but can be decomposed into an
infinite hierarchy of decidable conditions, via a parameter called “height”. Moreover, it naturally extends
to a validity condition ensuring cut elimination for the multiplicative
and additive fragment.

The following example illustrates with a simpler example the intuitive idea
behind validation by  bouncing threads: it is not valid according to straight threads since its only infinite branch conains no infinite thread at all. On the other hand, one can trace the unfolding of the coinductive by following formulas $\nu X.X$ upwards and formulas $\mu X.X$ downwards while changing directions and moving from a formula to its dual when entering axioms and cuts, as represented on the portion of the proof that is represented. Indeed, after reducing twice the cut in each repetition of the cycle,
it yields a cut-free proof which is validated by a straight thread, which can be viewed as the “straightened” version of the above mentioned bouncing thread:

$\pi_0 =  \begin{prooftree}
\Infer{0}[\rax]{\vdash \tikzmark{ad3}\nu X.X, \mu X.X\tikzmark{ad4}}
\Infer{1}[\rmu]{\vdash \tikzmark{ad2}\nu X.X, \mu X.X\tikzmark{ad5}}
\Hypo{\vdash \nu X.\orig{introA}X\tikzmark{ad7}}
\Infer{1}[\rnu${\times}2$]{\vdash \nu X.X\tikzmark{ad6}}
\Infer{2}[\rcut]{
\vdash \tikzmark{ad1}\nu X.X
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (introB) {\ensuremath{}};
\draw [->,>=latex] (introA.north) .. controls +(0:2.3cm) and +(-8:3cm) .. (introB.west);
\end{tikzpicture}
\end{prooftree}
\begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
\draw[rounded corners, smooth=2,red, opacity=.25] ($(pic cs:ad1)+(-.1cm,.1cm)$) to ($(pic cs:ad2)+(.1cm,-.2cm)$)to ($(pic cs:ad3)+(-.1,.2cm)$) to($(pic cs:ad4)+(-.2cm,.2cm)$) to($(pic cs:ad5)+(-.2cm,0cm)$) to($(pic cs:ad6)+(-.1cm,0cm)$) to($(pic cs:ad7)+(-.1cm,0cm)$) ;
\end{tikzpicture}
\;\;
\begin{array}{cc}
\rightarrow_{\mathsf{cut}}^2~
\Hypo{\pi_0}
\Infer{1}[\rnu]{\vdash \nu X.X}
\end{prooftree}
\\[16pt]~\rightarrow_{\mathsf{cut}}^\omega~
& \begin{prooftree}
\Hypo{\vdash \nu X.\orig{introa}X}
\Infer{1}[\rnu]{
\vdash \nu X.X
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (introb) {\ensuremath{}};
\draw [->,>=latex] (introa.north) .. controls +(15:.8cm) and +(-5:.8cm) .. (introb.west);
\end{tikzpicture}}
\end{prooftree}
\end{array}      $}

Summary of the contributions.
We introduce a new decidability criterion for preproofs, based on bouncing threads. We prove that it guarantees soundness and productivity of the cut-elimination process. The criterion is compatible with simple compositions with cuts, as shown in <ref>. Contrarily to <cit.>, we also provide a treatment of axioms, which introduces substantial additional difficulties in the proof of soundness and cut-elimination.
We finally show that a parameter can be associated to our criterion (the “height” of the bouncing thread) and that every valid circular proofs is validated with a bounded height. moreover, we show that the criterion with fixed height is decidable in the multiplicative case, but that without bounding the height, the criterion becomes undecidable already in the multiplicative case.

Organization of the contributions.
In Section <ref> we recall the basic definitions for the non-wellfounded proof system .
We then define, in <ref> the cut-elimination procedure. In <ref>, we introduce our new bouncing validity
condition, and show in <ref> that it guarantees soundness of the system and productivity of the cut-elimination procedure. We finally study in <ref> the decidability of our criterion in the multiplicative case. Proofs and developments omitted due to space constraints can be found in appendix.

The pre-proofs of

In this section we introduce the multiplicative additive
linear logic extended with least and greatest fixed point operators,
and a system of infinitary (pre-)proofs for that logic.

Given infinite sets of atoms $\C{A}=\{a,b,\dots \}$ and of fixed-point variables $\C{V}=\{X,Y,\dots \}$,
-formulas are built over the following syntax:

\begin{array}{rrll}   \null\hfill
\phi,\psi &::=&
a \| a^\bot \quad a\in {\C A}, &\quad \text{(atoms)}\\
&\|& \mu X. \phi \| \nu X. \phi \| X\quad  X \in {\C V} &\quad \text{(fixed points)}\\
&\|&  \bot \| \llone \| \phi \parr \psi \| \phi \tensor \psi &\quad \text{(multiplicatives)}\\
&\| &\llzero \| \top \| \phi \oplus \psi \| \phi \with \psi. &\quad \text{(additives)}
\end{array}   $$

The connectives $\mu$ and $\nu$ bind the variable $X$ in $\phi$.

The formulas of , the multiplicative fragment, are those formulas which do not contain $\with, \oplus, \top$ nor $\llzero$ (ie. restricting the grammar to the first two lines).

is the involution on formulas satisfying:

$$\begin{array}{c}a^{\bot\bot} = a;\  X^\bot = X;\  (\nu X. \phi)^\bot = \mu X. \phi^\bot;\\
\bot^\bot = \llone;\ (\phi\parr\psi)^\bot =  \phi^\bot\tensor \psi^\bot;\ (\phi\oplus\psi)^\bot =  \phi^\bot\with \psi^\bot.
\end{array}$$

Setting $X^\bot=X$ would be incorrect when considering formulas with free
variables, but it yields the proper dualization for closed formulas,
e.g. $(\mu X.X)^\bot=\nu X.X$.
Note that, since negation is not a connective, our formulas enjoy the
positivity condition by construction: all fixed-point expressions are

There are several presentations of sequents in the literature: a sequent can
be defined as a set of formulas, a multiset of formulas, a list of formulas or
a set of named formulas. The first two presentations  (sets and multisets of
formulas) are not suitable in a Curry-Howard perspective as they identify
proofs having completely different computational behaviours.
The last two presentations are the most used in the proofs-as-programs
framework. Considering sequents as lists of formulas requires a constant use
of the exchange rule, which is very heavy. In this paper, we made the choice
to work with sequents as sets of named formulas, also called formula
We recall next their formal definition, in the style of <cit.>.

A formula occurrence is a formula together with an address. In a
derivation, all the conclusion (and cut) formula occurrences will have
pairwise distinct addresses.
When a rule is applied to a formula occurrence, the
addresses of its sub-occurrences will be extended by $\{\Al,\Ar, \Ai\}$
(standing for left, right and inside respectively)
in order to record their provenance.
This is of  great importance for our developments: our validity criterion
traces the evolution of formulas, and this evolution is completely explicit in
their addresses.

We show in the following an example of an application of the $\parr$ rule in the framework of sequents as sets, as multisets and as set of formula occurrences respectively:

\scalebox{.9}{\begin{prooftree}
\Hypo{\vdash \phi}
\Infer{1}[\rparr]{\vdash \phi\parr\phi}
\end{prooftree}}
\quad&\quad
\begin{prooftree}
\Hypo{\vdash \phi, \phi}
\Infer{1}[\rparr]{\vdash \phi\parr\phi}
\end{prooftree}
\quad&\quad
\scalebox{.9}{\begin{prooftree}
\Hypo{\vdash \phi_{\alpha\Al}, \phi_{\alpha\Ar}}
\Infer{1}[\rparr]{\vdash (\phi\parr\phi)_\alpha}
\end{prooftree}}
%\\[20pt]\text{{\small Sequents as lists}}\quad&\quad \text{{\small Sequents as multisets}} \quad&\quad  \text{{\small sequents as set of formula occurrences}}
\end{array}

In  the first case, the two subformulas of $\phi\parr\phi$ collapse into one formula, in the second framework we keep track of the multiplicity but we cannot distinguish between the formula coming from the right and the one coming from the left. In the framework of formula occurrences, we can do this thanks to the tags $\Al$ and $\Ar$ in their addresses.

Let $\FA$ be an infinite set of atomic addresses, $\FA^\perp=\{\alpha^\perp\mid \alpha \in \FA\}$, and $\Sigma=\{\Al,\Ar,\Ai\}$.
An address is a word of the form $\alpha.w$, where $\alpha\in \FA\cup\FA^\perp$ and $w\in\Sigma^*$. Let us call $\Addr$ the set of addresses.
We say that $\alpha'$ is a sub-address of $\alpha$
when $\alpha$ is a prefix of $\alpha'$,
written $\alpha \sqsubseteq \alpha'$.
We say that $\alpha$ and $\beta$ are disjoint when
$\alpha$ and $\beta$ are incomparable wrt. ${\sqsubseteq}$.

The intuition is that atomic addresses and their duals will be assigned to the conclusions and cut formulas, and all the addresses appearing in our proofs will be sub-addresses of these addresses.

A formula occurrence, or simply occurrence,
is given by a formula $\phi$ and an address $\alpha$, and written
Occurrences will be denoted by $F$, $G$, $H$.

Occurrences are disjoint when their addresses

The occurrences $\phi_\alpha$ and $\psi_\beta$ are
structurally equivalent,
written $\phi_\alpha \equiv \psi_\beta$, if $\phi=\psi$.

Note that the relation of sub-address is the inverse of the prefix relation.
This may seem surprising, but it is coherent with the sub-formula relation.
For instance, in <ref>, $\phi$ is a sub-formula of $\phi\parr\phi$, but its address is $\alpha\Ar$ while the address of $\phi\parr\phi$ is $\alpha$.

We now define the rules of linear logic with fixed points in the framework of sequents as sets of occurrences.
As seen in <ref>, a rule will look at the structure of the
formula underlying an occurrence, decompose it following a standard rule, then assign addresses to its subformulas in the obvious way. This necessitates always making the addresses explicit. In order to lighten
notation, we will have the syntax of operate directly on

Logical connectives are lifted to operations on occurrences as:

* For any $\star\in\{\parr,\tensor,\oplus,\with\}$, if  $F = \phi_{\alpha
\Al}$ and  $G = \psi_{\alpha \Ar}$ then $F\star G = (\phi\star\psi)_\alpha$.

* For any $\sigma\in\{\mu,\nu\}$, if $F = \phi_{\alpha\Ai}$ then
$\sigma X. F = (\sigma X. \phi)_\alpha$.

We define a duality over $\Addr$ by setting $(\alpha.w)^\perp=\alpha^\perp.w$ and $(\alpha^\perp.w)^\perp=\alpha.w$ for all $\alpha\in\FA$ and $w\in\Sigma^*$.
We then define $(\phi_\alpha)^\bot = (\phi^\bot)_{\alpha^\bot}$,
and write $F\bot G$ when $F^\bot=G$.
We define substitution over occurrences as follows:
$(\phi_\alpha)[\psi_\beta/X] = (\phi[\psi/X])_\alpha$.

⊢F, G, Γ
1[]⊢FG, Γ

2[]⊢FG, Γ, Δ

1[]⊢, Γ

⊢F[μX.F/X], Γ
1[] ⊢μX.F, Γ

⊢G[νX.G/X], Γ
1[]⊢νX.G, Γ

F ≡G
1[]⊢F, G^⊥

⊢Γ, F
⊢F^⊥, Δ
2[]⊢Γ, Δ

⊢F, Γ
⊢G, Γ
2[] ⊢FG, Γ

⊢F_i, Γ
1[, $i\in\{1,2\}$]⊢F_1⊕F_2, Γ

1[]⊢⊤, Γ

(no rule for $\llzero$)

% \hline
\infparr  & \infbot  & \infwith  & \inftop & \infnu\quad  &\infax \\[12pt]
\inftensor  & \infone & \infplus  & \infzero\quad  & \infmu\quad  & \infcut\\[12pt]

\end{array}$$

Rules of the proof system

We are now ready to introduce our infinitary sequent calculus.

A sequent is a set of disjoint occurrences.
A pre-proof is a possibly infinite tree, coinductively
generated by the rules of Fig. <ref>.

Given a sequent $s$ in a pre-proof $\pi$, we denote by $\prem s$
the set of sequents which are premisses of the rule of conclusion $s$
in $\pi$.

Rules other than $\rax$ and $\rcut$ are called logical rules.
For every instance of one such rule
we call principal occurrence the occurrence in its conclusion
sequent that is decomposed to obtain the premisses.

The infinite derivations of may be quite complex trees,
possibly not even computable. In practical uses one would turn to sub-systems,
typically the fragment of circular pre-proofs
In a nutshell, a circular derivation is an infinite derivation which
has only finitely many distinct sub-trees up to renaming of
addresses <cit.>.

[Two-sided notation]
While it is proof-theoretical-ly convenient to work with one-sided sequents
as in the previous definition, it is more illustrating for some examples,
especially when we shall aim at illustrating computational interpretation
of some proofs, to allow to use the usual two-sided sequent calculi.
In the following (and in the examples of the introduction), two sided
sequents may be used:

$F_1,\ldots,F_n\vdash\Gamma$ should be read as
$\vdash \Gamma, F_1^\bot,\ldots,F_n^\bot$.

Regarding the labelling of inference rules, we allow ourselves two conventions: either the inference rules are written with the labels introduced in Fig. <ref> or, as in the introductory example, we use their two-sided names, for instance $\rtensorl$ and $\rtensorr$, in which case this is a notation for the corresponding rule in the one-sided sequent calculus, respectively $\rparr$ and $\rtensor$ in this case.

We show in Fig.<ref> two examples of pre-proof,  $\pi_\mathsf{succ}$ and  $\pi_\mathsf{dup}$. (The reader can check their validity and cut-elimination behaviours once those concepts will have been introduced in the following sections.)

\pi_\mathsf{succ}\quad= \quad\begin{prooftree}
\Infer{0}[\rax]{N \vdash N''}
\Infer{1}[\roplusr]{N \vdash \llone\plus N''}
\Infer{1}[\rmu]{N \vdash N'}
\end{prooftree} $$

\pi_{\mathsf{dup}} \quad=\quad   \begin{prooftree}
\Infer{0}[\rmu,\roplusl,\rone]{\vdash N_1}
\Infer{0}[\rmu,\roplusl,\rone]{\vdash N_2}
\Infer{2}[\rbot,\rtensor]{\llone \vdash N_1\tensor N_2}
\Hypo{
\orig{opidup}{N' \vdash N'_1\tensor N'_2}}
\Hypo{\pi_\mathsf{succ}}
\Hypo{\pi_\mathsf{succ}}
\Infer{2}[\rparr,\rtensor]{N'_1\tensor N'_2 \vdash N_1\tensor N_2}
\Infer{2}[\rcut]{N' \vdash N_1\tensor N_2}
\Infer{2}[\rnu,\rwith]{
%(\star) \qquad
N \vdash N_1\tensor N_2
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (tpidup)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (opidup.north east) .. controls +(40:6cm) and +(-5:10cm) .. (tpidup.east);
\end{tikzpicture}\;}
\end{prooftree}

Examples of pre-proofs  $\pi_\mathsf{succ}$ and  $\pi_\mathsf{dup}$.

Pre-proofs are obviously
unsound: it is easy to derive the empty sequent. Hence, a validity
condition shall be required for a pre-proof to be called a proof.

The cut elimination process

In this section we introduce the cut-elimination rules for pre-proofs.
In general, the cut-elimination procedure is not productive.
However, we will show in Section <ref> that when we restrict to valid pre-proofs (that will be defined in Section <ref>), the process is productive and outputs a valid pre-proof.

§.§ The multicut rule

In finitary proof theory, cut elimination may proceed by reducing topmost cuts. In the infinitary setting however, by non-wellfoundedness, there is no such thing, in general, as a topmost cut inference.
In <cit.>, this issue is dealt with by reducing
bottom-most cuts, and when encountering during the reduction a cut which is immediately above another one, instead of permuting two consecutive cuts, merging them into a new rule called
multicut and noted . A multicut can be seen as a metarule to represent a finite tree of cuts.

We will also use this multicut approach[Note that there are various approach to cut-elimination in infinitary settings, for non-wellfounded derivations or for logics including an $\Omega$-rule, in paritcular Mints continuous cut-elimination <cit.>.], but we now have to deal with axiom/cut reductions. This leads us to enrich the structure of multicuts, by allowing those to perform a renaming.

A multicut is a rule written as:

\Hypo{\vdash\Gamma_1\quad \dots\quad  \vdash\Gamma_n}
\Infer{1}[\rmcutpar]{\vdash\Gamma}
\end{prooftree}}$$

and comes with a function $\iota$ which shows how the occurrences of the conclusion are
distributed over the premisses (modulo renaming), and a relation
$\dbot$ specifiying which occurrences are cut-connected.
Below is an example of a multicut rule: the function $\iota$ is represented by the red lines, the relation bottom  is represented by the blue ones.

\Hypo{\vdash F'\tikzmark{PC1}, G}
\Hypo{\vdash G^\bot\tikzmark{PC2},H}
\Hypo{\vdash H^\bot\tikzmark{PC3},K}
\Infer{3}[\rmcutpar]{\vdash F\tikzmark{CC},K}
\end{prooftree}
\begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
\draw[rounded corners, smooth=2,red, opacity=.25] ($(pic cs:CC)+(-.2cm,.1cm)$)to ($(pic cs:PC1)+(-.2cm,-.1cm)$)to ($(pic cs:PC1)+(-.2cm,.1cm)$);
\draw[rounded corners, smooth=2,red, opacity=.25] ($(pic cs:CC)+(.3cm,.1cm)$)to ($(pic cs:PC3)+(.3cm,-.1cm)$)to ($(pic cs:PC3)+(.3cm,.1cm)$);
\draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:PC1)+(.25cm,.1cm)$)to ($(pic cs:PC1)+(.25cm,-.1cm)$)to ($(pic cs:PC2)+(-.4cm,-.1cm)$) to ($(pic cs:PC2)+(-.4cm,.1cm)$);
\draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:PC2)+(.3cm,.1cm)$)to ($(pic cs:PC2)+(.3cm,-.1cm)$)to ($(pic cs:PC3)+(-.4cm,-.1cm)$) to ($(pic cs:PC3)+(-.4cm,.1cm)$);
\end{tikzpicture}

Precise definitions and more explanations are given in
<ref>. Later, if clear from the context, we omit to specify $\iota$ and $\dbot$ in the rule name.

Now, we add the multicut rule to our proof system in order to perform cut-elimination.

We call the infinitary proof system obtained from by adding the multicut rule.

§.§ Reduction rules and strategy

The reduction rules are the same as in <cit.>, adapting them in a straighforward way to account for the extra labellings $\iota,\dbot$ in multicut rules. We give examples of such reductions in this section.

There are two kinds of cut reductions: external
ones that push the multicut deeper in the pre-proof (Example in <ref>.a),
and internal ones, that keep the multicut at the same level, and are not productive (Example in <ref>.b).

The rules in the first category are said to be productive, since they contribute to the output of the process. Intuitively, the cut-elimination process succeeds if infinitely many productive rules occur on each branch of the proof.

An exhaustive description of the cut-reduction rules is given in

(a) Example of an external reduction rule:

\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta, F'[\mu X. F'/X]}
\Infer{1}[\rmu]{\vdash \Delta, \mu X.\tikzmark{IRPl} F'}
\Infer{2}[\rmcut]{\vdash \Sigma, \mu X.\tikzmark{IRCl} F}
\end{prooftree}
\quad&\quad\underset{}{\longrightarrow}\quad&\quad
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,F'[\mu X.\tikzmark{IRPr} F'/X]}
\Infer{2}[\rmcut]{\vdash \Sigma, F[\mu X.\tikzmark{IRCr} F/X]}
\Infer{1}[\rmu]{\vdash \Sigma, \mu X. F}
\end{prooftree}
%\begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
%   \draw[rounded corners, smooth=2,red, opacity=.25] ($(pic cs:IRCl)+(-.2cm,.1cm)$)to ($(pic cs:IRPl)+(-.2cm,.1cm)$);
%   \draw[rounded corners, smooth=2,red, opacity=.25] ($(pic cs:IRCr)+(-.2cm,.1cm)$)to ($(pic cs:IRPr)+(-.2cm,.1cm)$);
\end{array}$

(b) Examples of internal reduction rules:

\scalebox{.9}{ \begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,F}
\Hypo{\vdash \Gamma,F^\bot}
\Infer{2}[\rcut]{\vdash \Delta,\Gamma}
\Infer{2}[\rmcut]{\vdash \Sigma}
\end{prooftree}}
\quad&\quad
\underset{}{\longrightarrow}
\quad&\quad
\begin{array}{c}
\scalebox{.9}{
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,\tikzmark{MPC2}F}
\Hypo{\vdash F^\bot,\tikzmark{MPC3}\Gamma}
\Infer{3}[\rmcut]{\vdash \Sigma}
\end{prooftree}
%        \begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
%        \draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:MPC2)+(.1cm,.1cm)$)to ($(pic cs:MPC2)+(.1cm,-.1cm)$)to ($(pic cs:MPC3)+(-.45cm,-.1cm)$) to ($(pic cs:MPC3)+(-.45cm,.1cm)$);
%        \end{tikzpicture}

\\
\end{array}
\\
%      where  $\dbot'\defeq\dbot\cup\{\{F, F^\bot\}\}$.
%      \smallskip
\scalebox{.9}{
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,F[\mu X.F/X]}
\Infer{1}[\rmu]{\vdash \Delta,\mu X.\tikzmark{MPl1}F}
\Hypo{\vdash F'^\bot[\nu X.F'^\bot/X],\Gamma}
\Infer{1}[\rnu]{\vdash \nu X.F'^\bot,\tikzmark{MPl2}\Gamma}
\Infer{3}[\rmcut]{\vdash \Sigma}
\end{prooftree}}
\quad&\quad
\underset{}{\longrightarrow}
\quad&\quad
%  \quad\quad
\scalebox{.9}{
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,\tikzmark{MPr1}F[\mu X.F/X]}
\Hypo{\vdash F'^\bot[\nu X.\tikzmark{MPr2}F'^\bot/X],\Gamma}
\Infer{3}[\rmcut]{
\vdash \Sigma}
\end{prooftree}
%        \begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
%        \draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:MPl1)+(.0cm,.2cm)$)to ($(pic cs:MPl1)+(.0cm,.0cm)$)to ($(pic cs:MPl2)+(-.6cm,.0cm)$) to ($(pic cs:MPl2)+(-.6cm,.2cm)$);
%        \draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:MPr1)+(.1cm,.1cm)$)to ($(pic cs:MPr1)+(.1cm,-.1cm)$)to ($(pic cs:MPr2)+(.1cm,-.1cm)$) to ($(pic cs:MPr2)+(.1cm,.1cm)$);
%        \end{tikzpicture}
\end{array}  $$

Examples of external and internal reduction rules.

We now describe a procedure to eliminate cuts from proofs, using as an intermediary framework the system with multicuts.
We start by embedding in by adding a unary multicut at the root of the pre-proof, with the identity as $\iota$ and $\dbot=\emptyset$. We then apply internal and external reduction rules to this multicut.

We will require reduction sequences to be fair, in the sense that every redex is eventually fired.

We introduce in the following section the validity condition, that will guarantee productivity of this cut elimination process.

Bouncing threads and pre-proof validity

We now formally introduce our bouncing threads and the corresponding
notion of validity for pre-proofs.
Given an alphabet $A$, we denote by $A^\omega$ the set of infinite
words over $A$, and define $A^\infty$ to be $A^* \cup A^\omega$.
We will make use of the letter $\lambda$ to denote ordinals in $\omega+1$,
i.e. either $\omega$ or a finite ordinal in $\mathbb{N}$.
For such an ordinal, recall that $1+\lambda=\lambda$ iff $\lambda=\omega$.
Finally, we will make use of a special concatenation:
given $u=(u_i)_{i\leq n<\omega}$ and $v=(v_i)_{i\in\lambda}$
such that $u_n = v_0$, we define $u\odot v$ as the standard concatenation
of $u$ and $v$ without its first element, i.e. $u \cdot
For example $aba\odot aab= abaab$.

§.§ Threads

We start with a naive notion of pre-thread,
defined as a sequence of pointed sequents (i.e. sequents with a marked formula) together with a direction:
a pre-thread follows occurrences in consecutive sequents,
travelling up- or downwards.

A pre-thread is a sequence $\psd{F_i}{s_i}{d_i}_{i\in\lambda}$ of tuples of a formula, a sequent and a direction, such that for all $i\in\lambda$,  $F_i \in s_i$, $d_i \in
\{\uparrow,\downarrow\}$ and if $i+1\in\lambda$ one of the following
clauses holds:

* $d_i = d_{i+1} = {\uparrow}$,
$s_{i+1} \in\prem {s_i}$, and $F_{i+1} \sqsubseteq F_i$;

* $d_i = d_{i+1} = {\downarrow}$,
$s_i \in\prem{s_{i+1}}$,
and $F_i \sqsubseteq F_{i+1}$;

* $d_i = {\downarrow}$, $d_{i+1} = {\uparrow}$,
$s_i$ and $s_{i+1}$ are the two premisses of the same cut rule,
and $F_i = F^\bot_{i+1}$;

* $d_i = {\uparrow}$, $d_{i+1} = {\downarrow}$ and
$s_i = s_{i+1} = \{ F_i, F_{i+1} \}$ is the conclusion of an axiom rule (so that $F_i \equiv F^\bot_{i+1})$.

If $\lambda=n+1$ is finite we call $F_0$ and $F_n$ the endpoints
of the pre-thread.

Consider the formulas $\phi=\nu X. X$, $F=\phi_\alpha$, $F'=\phi_\beta$, $F''=\phi_{\beta.\Ai}$ where $\alpha$ and $\beta$ are disjoint addresses. Let $G, G'$ be two disjoint occurrences such that $G\equiv G'$. In the following pre-proof, the red and blue lines are two pre-threads[... which respectively correspond to the following sequences:

$t_r = (F\parr G; \vdash F\parr G; \uparrow~\!)\cdot
(F\parr G; \vdash F\parr G, F'^\perp\tensor G'^\perp; \uparrow~\!)\cdot
(F; \vdash F, F'^\perp;\uparrow~\!)\cdot
(F'^\perp; \vdash F, F'^\perp;\downarrow~\!)\cdot
(F'^\perp\tensor G'^\perp; \vdash F\parr G, F'^\perp\tensor G'^\perp; \downarrow~\!)\cdot
(F'\parr G'; \vdash F'\parr G'; \uparrow~\!)\cdot
(F'; \vdash F', G'; \uparrow~\!)\cdot
(F''; \vdash F'', G'; \uparrow~\!)$ and

$t_b = (F\parr G; \vdash F\parr G; \uparrow~\!)\cdot
(F\parr G; \vdash F\parr G, F'^\perp\tensor G'^\perp; \uparrow~\!)\cdot
(G; \vdash G, G'^\perp;\uparrow~\!)\cdot
(G'^\perp; \vdash G,G'^\perp;\downarrow~\!)\cdot
(F'^\perp\tensor G'^\perp; \vdash F\parr G, F'^\perp\tensor G'^\perp; \downarrow~\!)\cdot
(F'\parr G'; \vdash F'\parr G'; \uparrow~\!)\cdot
(F'; \vdash F', G'; \uparrow~\!)\cdot
(F''; \vdash F'', G'; \uparrow~\!)$.]:

\Infer{0}[\rax]{\vdash \tikzmark{r3}F, F'^\bot\tikzmark{r4}}
\Infer{0}[\rax]{\vdash \tikzmark{b3}G, G'^\bot\tikzmark{b4}}
\Infer{2}[\mkrule{\parr,\tensor}]{\vdash F\tikzmark{r2}\parr G, F'^\bot\otimes\tikzmark{r5} G'^\bot}
\Hypo{\vdots}
\Infer{1}[]{\vdash \tikzmark{r8}F'', G'}
\Infer{1}[\rnu]{\vdash \tikzmark{r7}F', G'}
\Infer{1}[\rparr]{\vdash F'\tikzmark{r6}\parr G'}
\Infer{2}[\rcut]{\vdash F\tikzmark{r1}\parr G}
\end{prooftree}
\begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
\draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:r1)+(-.1cm,.1cm)$) to ($(pic cs:r2)+(.1cm,-.2cm)$)to ($(pic cs:r2)+(-.1,.2cm)$) to($(pic cs:r3)+(0,.2cm)$) to($(pic cs:r4)+(0,.2cm)$) to($(pic cs:r5)+(0,.1cm)$) to($(pic cs:r6)+(.1cm,.1cm)$) to($(pic cs:r7)+(0,.2cm)$) to($(pic cs:r8)+(0,.2cm)$);
\draw[rounded corners, smooth=2,red, opacity=.25] ($(pic cs:r1)+(.2cm,.2cm)$) to ($(pic cs:r2)+(.2cm,-.15cm)$) to ($(pic cs:r2)+(.2cm,.2cm)$) to($(pic cs:b3)+(0,.2cm)$) to($(pic cs:b4)+(0,.2cm)$) to($(pic cs:r5)+(0,.2cm)$) to($(pic cs:r6)+(.2cm,.2cm)$) to($(pic cs:r7)+(.1cm,.2cm)$) to($(pic cs:r8)+(.1cm,.2cm)$);
\end{tikzpicture}

We shall define threads as pre-threads satisfying a particular condition that will make them compatible with cut reduction, in the sense that they will have residuals after cut-elimination steps. In Example <ref>, the red thread has no residual

if one performs a cut elimination step on $F'\parr G'$, because it
comes from the right-hand subformula of  $F'^\perp \tensor G'^\perp$
and goes

to the left-hand subformula of $F' \parr G'$.
In contrast,
the blue thread can meaningfully be simplified to persist over cut elimination
steps: its residual is well-defined. Geometry of Interaction <cit.> provides a formalization of
these notions, assigning weights to pre-threads and determining which weights
correspond to meaningful computations.
We follow this inspiration, adapting it to our framework.

Let $t=\psd{F_i}{s_i}{d_i}_{i\in 1+\lambda}$ be a pre-thread.
The weight of $t$
is a word $(w_i)_{i\in \lambda}\in
\{\Al, \Ar, \Ai, \bar{\Al}, \bar{\Ar}, \bar{\Ai}, \Wwait, \Aax, \Ccut\}^\infty$, written $\weight{t}$ and  defined as follows.
For every $i\in\lambda$ one of the following clauses holds:

* $w_i = x$ if $F_{i} = \phi_\alpha$ and $F_{i+1} = \psi_{\alpha x}$
for $x \in \{\Al,\Ar,\Ai\}$;

* $w_i = \bar{x}$ if $F_{i} = \phi_{\alpha x}$ and $F_{i+1} = \psi_{\alpha}$
for $x \in \{\Al,\Ar,\Ai\}$;

* $w_i = \Aax$
if $d_{i} = {\uparrow}$ and $d_{i+1} = {\downarrow}$
(corresponding to bouncing on an axiom rule);

* $w_i = \Ccut$
if $d_{i} = {\downarrow}$ and $d_{i+1} = {\uparrow}$
(corresponding to bouncing on a cut rule);

* $w_i = \Wwait$ if $F_{i} = F_{i+1}$.

The weight should be seen as a bracketed expression, where each symbol
$x\in \{{\Al},{\Ar},{\Ai}\}$ is an opening bracket with matching closing
bracket $\bar{x}$.
When defining threads from pre-threads,
we will be particularly interested in the following classes of
well-bracketed words:

Let $\C{B}$ and $\C{H}$ be the set of words defined inductively as follows:

%\C{W}:= \Wwait^*
\C{B}:= \Ccut \ \mid \ \C{B}\Wwait^*\Aax\Wwait^*\C{B} \ \mid
\ \bar{x}\Wwait^*\C{B}\Wwait^*x
\quad\quad\quad
\C{H}:= \epsilon\ \mid \ \Aax\Wwait^*\C{B}

A (finite) pre-thread is called a $b$-path if $\weight{t}\in\C{B}$.
It is called an $h$-path if $\weight{t}\in\C{H}$.

The $b$-paths start downwards and end upwards: they consist
of a series of U-shapes centered around cuts, glued together by axioms.
The endpoints of $b$-paths are negations of each other (up to renaming).

The $h$-paths start and end going upwards, and their endpoints are
structurally equivalent (up to renaming).
Intuitively, $h$-paths will be simplified during cut elimination,
and eventually disappear completely.

A pre-thread $t$ is a thread when it can be written
$\odot_{i\in 1+\lambda} (H_i\odot V_i)$ where for all $i\in 1+\lambda$:

* $\weight{V_i}\in \{\Al,\Ar, \Ai, \Wwait\}^{\infty}$
and it is non-empty if $i\neq\lambda$;

* $\weight{H_i}\in \C{H}$ and it is non-empty if $i\neq 0$.

Notice that such a decomposition is unique.
We call $(V_i)_{i\in 1+\lambda}$ the visible part of $t$,
and we denote it by $\visP{t}$,
and $(H_i)_{i\in 1+\lambda}$ its hidden part
and we denote it by $\hiddenP{t}$.
A thread is stationary when its visible part is a finite sequence (of finite words), or when there exists $k\in 1+\lambda$
such that $\weight{V_i}\in\{\Wwait\}^{\infty}$ for all
$k\leq i \in 1+\lambda$.

For instance if a pre-thread $t=(F_i,s_i,\uparrow)_{i\in\lambda_t}$ of length $\lambda_t$ goes only
upwards with $\weight{t}\in\{\Al,\Ar,\Ai,\Wwait\}^{\lambda_t}$, then the above decomposition is given by $\lambda=0$, $H_0=(F_0,s_0,\uparrow)$ and $V_0=t$.

Let us consider the blue pre-thread of Example <ref>. We can decompose it into
a visible part (plain line) and a hidden part (dashed line) as shown below:

\Infer{0}[\rax]{\vdash \tikzmark{ar3}F, F'^\bot\tikzmark{ar4}}
\Infer{0}[\rax]{\vdash \tikzmark{ab3}G, G'^\bot\tikzmark{ab4}}
\Infer{2}[\mkrule{\parr,\tensor}]{\vdash F\tikzmark{ar2}\parr G, F'^\bot\otimes\tikzmark{ar5} G'^\bot}
\Hypo{\vdots}
\Infer{1}[]{\vdash \tikzmark{ar8}F'', G'}
\Infer{1}[\rnu]{\vdash \tikzmark{ar7}F', G'}
\Infer{1}[\rparr]{\vdash F'\tikzmark{ar6}\parr G'}
\Infer{2}[\rcut]{\vdash F\tikzmark{ar1}\parr G}
\end{prooftree}
\begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
\draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:ar1)+(.2cm,.1cm)$)to ($(pic cs:ar2)+(.3cm,-.3cm)$) to ($(pic cs:ar2)+(.2cm,.1cm)$) to($(pic cs:ar3)+(0,.1cm)$);
\draw[rounded corners, smooth=2,cyan, opacity=.25,dash pattern=on 3pt off 6pt]($(pic cs:ar3)+(.1cm,.1cm)$) to($(pic cs:ar4)+(0,.1cm)$) to ($(pic cs:ar5)+(0,.1cm)$) to($(pic cs:ar6)+(.1cm,.1cm)$) to($(pic cs:ar7)+(.1cm,0cm)$);
\draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:ar7)+(.1cm,.1cm)$) to($(pic cs:ar8)+(.1cm,.1cm)$);
\end{tikzpicture}}$$

The blue pre-thread is then indeed a thread. On the contrary,

the red pre-thread from <ref> admits no such decomposition.

If we consider the sequence of formulas followed by a non-stationary thread
on its visible part, ignoring its hidden parts (which have equivalent
formulas on their endpoints), and skipping the steps in the visible parts
corresponding to $\Wwait$ weights, we obtain an infinite sequence of formulas
as in <cit.> where each formula is an immediate subformula or an
unfolding of the previous formula.
It is then well known <cit.> that the formulas appearing infinitely often in
that sequence admit a minimum w.r.t. the subformula ordering. We call this
formula the minimal formula of the thread.

A non-stationary thread is valid if its minimal
formula is a $\nu$-formula.

Consider for example the formula $F=\mu X.\nu Y.X$. The minimal formula obtained by unfolding $F$ infinitely many times is $F$ itself, a $\mu$-formula, so the corresponding thread would be invalid.

§.§ Pre-proof validity: the multiplicative case

The previous notion of valid thread suggests a first extension of the
notion of valid proof based on straight threads <cit.>:
one might say that a branch $\beta$ is valid when there is a valid bouncing thread
which meets $\beta$ infinitely often,
and declare a pre-proof valid when all its branches are.

However, this notion of weak validity turns out to allow
unsound proofs, as shown next.

We set $T:=\nu X. X$ and $F:=\mu X. X$. The following is a weakly valid proof of the empty sequent. The hidden part of the decomposition

\scalebox{.85}{\begin{prooftree}
\Infer 0[\rax]{\vdash F_{\alpha \Al}, T_{\beta \Al}}

\Infer 0[\rax]{\vdash T\tikzmark{un5}_{\alpha \Ar\Ai}, F\tikzmark{un6}_{\beta \Ar}}
\Infer 1[\rnu]{\vdash T\tikzmark{un4}_{\alpha \Ar}, F\tikzmark{un7}_{\beta \Ar}}

\Infer 2[\rtensor]{\vdash (F\tensor\tikzmark{un3}T)_\alpha,
T_{\beta \Al}, F\tikzmark{un8}_{\beta \Ar}}
\Infer 1[\rparr]{\vdash (F\tensor\tikzmark{un2}T)_\alpha,
\Hypo{
\vdash (F\tensor \orig{a}T)_{\beta^\perp}}
\Infer 2 [\rcut]{\vdash F\tensor\tikzmark{un1}T_\alpha
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (b)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (a.north east) .. controls +(10:1.5cm) and +(-5:5cm) .. (b.north east);
\end{tikzpicture}\;}
%   \Hypo{}
\Infer 0[\rax]{ \vdash T_{\alpha^\perp \Al}, F_{\alpha^\perp \Ar}}
\Infer 1[\rparr]{ \vdash (T\parr F)_{\alpha^\perp}}
\Infer 2[\rcut] {\vdash }
\end{prooftree}
\begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
\draw[rounded corners, smooth=2,green, opacity=.4] ($(pic cs:un4)$) to($(pic cs:un5)+(0cm,.1cm)$);
\draw[rounded corners, smooth=2,cyan, opacity=.4,dash pattern=on 3pt off 5pt]
($(pic cs:un1)$) to ($(pic cs:un2)$) to ($(pic cs:un3)$) to($(pic cs:un4)$);
\draw[rounded corners, smooth=2,cyan, opacity=.4,dash pattern=on 3pt off 6pt]
($(pic cs:un5)+(0cm,.1cm)$) to($(pic cs:un6)+(0cm,.1cm)$) to($(pic cs:un7)$) to($(pic cs:un8)+(.1cm,0cm)$)to($(pic cs:un9)+(-.1cm,.1cm)$)to ($(a)$) to ($(a)+(0cm,.1cm)$);
\end{tikzpicture}

A proper notion of validity must therefore be more constraining.
We shall consider the following one, which requires that the visible
part of the valid thread $t$ is contained in the infinite branch $\beta$.

Let $\pi$ be a pre-proof. An infinite branch  $\beta$ of $\pi$ is said to be valid if there is a valid thread $t$ starting  from one of its sequents, whose visible part is contained in this branch.
A proof is a pre-proof in which every infinite branch is valid.

We show below examples of valid and invalid pre-proofs:

\scalebox{.85}{\begin{prooftree}
\Infer{0}[\rax]{\vdash (\nu X\tikzmark{bb2}. X)_\alpha, (\mu X.\tikzmark{bb3}
\Hypo{
\vdash (\nu X\tikzmark{bb5}. \orig{a} X)_{\beta^\bot\Ai}}
\Infer{1}[\rnu]{\vdash (\nu X\tikzmark{bb4}. X)_{\beta^\bot}}
\Infer{2}[\rcut]{
\vdash (\nu X\tikzmark{bb1}. X)_\alpha \begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (b)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (a.north east) .. controls +(20:1.2cm) and +(-5:5.5cm) .. (b.east);
\end{tikzpicture}\;}
\end{prooftree}

\scalebox{.85}{\begin{prooftree}
\Infer{0}[\rax]{\vdash (\nu X\tikzmark{rr3}. X)_{\alpha\Ai}, (\mu
X.\tikzmark{rr4} X)_\beta}
\Infer{1}[\rnu]{\vdash (\nu X\tikzmark{rr2}. X)_\alpha, (\mu X.\tikzmark{rr5}
\Hypo{
\vdash (\nu X\tikzmark{rr6}. \orig{aa}X)_{\beta^\bot}}
\Infer{2}[\rcut]{
\vdash (\nu X\tikzmark{rr1}. X)_\alpha
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (bb)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (aa.north east) .. controls +(20:1.2cm) and +(-5:5cm) .. (bb.east);
\end{tikzpicture}\;
\end{prooftree}
\begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
\draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:bb1)+(0cm,.1cm)$) to ($(pic cs:bb2)+(.2cm,-.4cm)$) to ($(pic cs:bb2)+(-.2cm,.1cm)$) to ($(pic cs:bb2)+(.5cm,.5cm)$) to($(pic cs:bb3)+(0,.1cm)$) to($(pic cs:bb4)+(.1cm,0cm)$) to($(pic cs:bb5)+(0cm,0cm)$)to($(pic cs:bb5)+(.5cm,0.3cm)$);
\draw[rounded corners, smooth=2,red, opacity=.25] ($(pic cs:rr1)+(-.1cm,.2cm)$) to ($(pic cs:rr2)+(.2,-.4cm)$) to ($(pic cs:rr2)+(-.1,.2cm)$) to($(pic cs:rr3)+(0,.2cm)$) to($(pic cs:rr4)+(0,.2cm)$) to($(pic cs:rr5)+(0,.1cm)$) to($(pic cs:rr6)+(0cm,0cm)$) to($(pic cs:rr6)+(.1cm,0cm)$)to($(pic cs:rr6)+(.5cm,.3cm)$);

\end{tikzpicture}

The pre-proof on the left is valid: its infinite
branch is supported by the valid blue thread,
whose visible part belongs to the infinite branch.
The right pre-proof is not valid, because the red thread,
though valid, has a visible part that is not contained in
the infinite branch.

Cut elimination theorem for

In this section, we shall establish our central result:

Fair reduction sequences on proofs produce cut-free proofs.

For expository reasons, we focus on the multiplicative case here. The treatment of additives, while bringing new cases, is similar and can be found in Appendix <ref>.

The proof follows the same lines as the proof of cut elimination for straight threads <cit.>.
We will only sketch it here and emphasize the new phenomena arising from the presence of axioms and bouncing threads.  The full proof can be found in Appendix <ref>.

The proof of Theorem <ref> is in two parts.
We first prove that we cannot have a fair infinite reduction sequence made only of (unproductive) internal reductions.
Hence cut elimination is productive, reductions of proofs converge to cut-free pre-proofs.
We then establish that the obtained pre-proof is a valid proof.
In this section, we will only show productivity, validity of the resulting proof is shown in a similar way.

To show productivity, we proceed by contradiction, assuming that there exists a fair infinite sequence of internal reductions from a given proof $\pi$ of conclusion $\Gamma$. We will also assume w.l.o.g. that $\pi$ has only one multicut at the root. Note that since we perform only internal reduction rules, and since the latter do not duplicate multicuts, there is only one multicut progressing in the proof during this sequence of reductions. In the following, we refer to it as “the” multicut.

§.§ Trace of a reduction sequence
Let us start by introducing an important tool to analyse internal reduction sequences, called their trace.  The trace of an internal reduction sequence is the set of sequents that occurred as a premise of the multicut rule during this reduction sequence. The conclusion sequent of the proof is additionally included in the trace.
By analyzing the reduction rules, it is easy to see that:

Given a $\muMLLi$ proof $\pi$, the trace of $\pi$ is a subtree (possibly with open leaves) of the original proof $\pi$: the trace of $\pi$ is the proof tree $\pi$ from which some branches may have been pruned and replaced by open leaves.

An example of a trace is shown below: sequents not in the trace are grayed.

\scalebox{.9}{
\begin{prooftree}
\Hypo{\vdots}
\Infer{1}[\rmu]{\vdash \mu X. X_{\beta\Ai}}
\Infer{1}[\rmu]{\vdash \mu X. X_\beta}

\Hypo{\vdots}
\Infer{1}[\rnu]{\vdash \mu X. X_{\beta^\bot\Ai\Ai}, \mu X. X_\gamma}
\Infer{1}[\rnu]{\vdash \mu X. X_{\beta^\bot\Ai}, \mu X. X_\gamma}

\Hypo{\textcolor{gray}{\vdots}}
\Infer{1}[\rnu]{\textcolor{gray}{\vdash \nu X. X_{\gamma^\bot\Ai}, \bot_\alpha}}
\Infer{1}[\rnu]{\vdash \nu X. X_{\gamma^\bot}, \bot_\alpha}

\Infer{2}[\rcut]{\vdash \nu X. X_{\beta^\bot\Ai}, \bot_\alpha}
\Infer{1}[\rnu]{\vdash \nu X. X_{\beta^\bot}, \bot_\alpha}

\Infer{2}[\rmcut]{\vdash \bot_\alpha}
\end{prooftree}

Before going further let us see how we will use the trace to get a contradiction:

* We will define an extension of the proof system , and show that it is sound with respect to a boolean semantics.

* Then we will show that the trace can be seen as a proof of a false sequent in this extended proof system.

* This contradicts soundness and concludes the proof.

§.§ The trace is almost a proof
As said above, we will need to see the trace as a genuine proof. In fact, it is almost a proof since it is a subtree of the original proof $\pi$, but is not completely a proof for the following reasons:

* The trace may have unjustified sequents:
this happens when a sequent $S$ enters the multicut during the reduction
sequence but never gets reduced. It will then be part of the trace but
the subtree of $\pi$ rooted in $S$ will not. This is for instance the case of the sequent $\vdash \nu X. X _{\gamma^\bot\Ai},  \bot_\alpha$ in the example above.

* There is another reason why the trace might not
be a proof: its infinite branches may not be valid. The infinite
branches of the trace are also infinite branches of the proof $\pi$, thus they
are supported by valid bouncing threads of $\pi$. However, since the threads are bouncing, they might leave the branch and thus not be included in the trace.

We will show later how to handle the first problem of unjustified sequents. As for the second problem, we show that this actually never happens:
Let $T$ be the trace of a reduction sequence starting from a proof $\pi$,
and let $\beta$ be an infinite branch of $T$. If $t$ is a bouncing thread of $\pi$
validating $\beta$, then $t$ is also a bouncing thread of $T$.

This is one of the difficulties specific to the bouncing threads. This result is trivial with straight threads <cit.>, since threads belong to the branch they support.

§.§ Truncated proof system

To see the trace as a proof, we need to overcome the problem of unjustified sequents. For that, we will embed the trace in a proof system extending , called the truncated proof system.

This proof system is parameterized by a partial function $\tau:\Addr \to \{\top, \llzero\}$ (from addresses to the formulas $\top, \llzero $) called a truncation. To get a sound proof system, we impose a coherence condition on truncations: they should assign dual values to dual addresses.

The rules of the truncated proof system are the same as those of $\muMLLi$, with an extra rule
which allows to replace an occurrence by its image in $\tau$. Pre-proofs and the validity condition are defined in the same way as .

The advantage of the truncated proof system is that it allows to close sequents easily:  if the address of an occurrence of the sequent is mapped to $\top$  by $\tau$, we can justify the sequent by a $\top$ rule.

The boolean semantics can be extended in the presence of truncations in a natural way: the occurrences whose addresses are in the domain of the truncation obtain as a boolean value their image by $\tau$. The rest of the boolean values are propagated through the connectives in the usual way.

We show that the truncated proof system is sound for this semantics.
Note that can be seen as a truncated proof system, where the truncation has empty domain. In this case the truncated boolean semantics coincides with the classical boolean semantics. Hence is sound for the boolean semantics.

The proof system is sound for the boolean semantics.

§.§ Trace as a truncated proof
Let us see how to transform the trace into a proof in a truncated proof system. For this , we need to find a truncation $\tau$ that can allow us to close every unjustified sequent. In other words, we need to find a strategy for selecting an occurrence in each unjustified sequent, to which we will assign $\top$ by the truncation $\tau$. This strategy should define a coherent truncation in the sense that it should not assign $\top$ to two dual occurrences.

In <cit.>, we have given such a strategy: we select the occurrence of the unjustified sequent which is principal in the proof $\pi$. The presence of axioms complicates the situation:  If $F$ is the occurrence that has been selected in an unjustified sequent, then its dual might appear in an axiom rule $\vdash F^\perp, G$.
By coherence of the truncation, the address of $F^\perp$ must have been assigned $\llzero$ and the axiom rule cannot be soundly applied anymore. To justify the sequent $\vdash F^\perp, G$, we need to assign $\top$ to the address of $G$. Since the same can happen on the $G$ side, we need to show that it remains possible to define $\tau$ in a coherent way.

To get our desired contradiction, we need in addition for $\tau$ to assign $\llzero$ to the conclusion, thereby obtaining a proof of a false sequent. This needs to be done while still respecting the aforementioned constraints induced by axioms.
préciser l'explication du paragraphe précédent: comment assigner 0.

§.§ Summary
To sum up, we have found a truncation $\tau$ i) which assigns $\llzero$ to the conclusion formula ii) for which the trace can be seen as a proof in the corresponding truncated proof system. Since the proof system is sound, we get a contradiction and this concludes the proof of productivity.

Decidability properties of

§.§ An operational approach to threads

In this section, we will explicate how threads can be recognized by a specific deterministic pushdown automaton reading only the weight of a pre-thread.
This will allow us to define the height of a thread and the notion of constraint stack.

Let $\Athread$ be the deterministic pushdown automaton described in Fig. <ref>, on alphabet $\Sigma=\{\Al,\Ar,\Ai, \bar{\Al},\bar{\Ar},\bar{\Ai},\Aax,\Ccut, \Wwait\}$ and stack alphabet $\Gamma=\{\Al,\Ar,\Ai,\bot\}$ where $\bot$ is the empty stack symbol.

The transitions are labelled “$(a,\gamma) \mid \tau$”, where $a\in\Sigma$ is the input letter, $\gamma\in\Gamma$ is the topmost stack symbol, and $\tau$ is the action performed on the stack (no action if $\tau$ is not specified). If no stack symbol is specified, the stack is left unchanged. Symbol $x$ stands for an element in $\{\Al,\Ar,\Ai\}$. No acceptance condition is specified, meaning that any run is accepting. Only the absence of an available transition can cause the automaton to reject its input, for instance reading $\Al$ with topmost stack symbol $\Ar$ in state $\uparrow$.
The transition marked with a double arrow corresponds to the visible part of the thread.

[shorten >=1pt,node distance=3cm,on grid,auto,initial text=,
every state/.style=inner sep=0pt,minimum size=6mm, every loop/.style=min distance=.5cm, looseness=10]

[state,initial] (up) $\uparrow$;
[state, right=of up] (down) $\downarrow$;
(up) edge[loop below,double] node$(x,\bot)$ ()
edge[loop above] node$\begin{array}{c}(x,x)\mid\pop()\\\Wwait\end{array}$ ()
edge[bend left] node $\Aax$ (down)
(down) 	edge[loop above] node$\begin{array}{c}(\bar{x},\gamma)\mid\push(x)\\W\end{array}$ ()
edge[bend left] node $\Ccut$ (up)

The deterministic pushdown automaton $\Athread$

Let $t$ be a pre-thread. Then $t$ is a thread if and only if $\weight{t}$ is accepted by $\Athread$.

The constraints on the stack match the grammar from Def. <ref>.

The stack of $\Athread$ will be referred to as the constraint stack.

§.§ Undecidability of bouncing validity

In this section, we sketch why the validity condition is already undecidable for

. This will motivate the following section introducing decidable subcriteria constituting a hierarchy of criteria while exact definitions, encodings and proof of undecidability are postponed to  Section <ref> for readability.

To show undecidability, we reduce from the halting problem for Minsky Machines, i.e. two-counter machines (2CM) able to perform increment, decrement, and zero test on the counters. The halting problem for 2CM is known to be $\Sigma^0_1$-complete <cit.>.
The proof is only sketched here, and some technicalities have been abstracted away for clarity purposes. See Section <ref> for exact definitions and encodings.

We encode the halting problem of a 2CM $M$ using a bouncing thread. The thread of interest will always follow a formula $F=\nu X.(X\parr X)$ when going upwards, and its dual $G=\mu X.(X\tensor X)$ when going downwards. The idea is to use the constraint stack to encode the value of counters, and the position in the graph to encode the control state of the machine. The general shape of the main preproof $P$ performing the desired reduction is represented Fig. <ref>. Boldface formulas are those introduced in cuts, and grayed formulas are the ones that are not part of the thread of interest. We will also ignore addresses in this proof sketch, except those relevant to our encoding.

$$\scalebox{.9}{   \begin{prooftree}
\Infer{0}[\rax]{\vdash \gG, \gray{F}}

\Hypo{
\orig{a}\vdash \gG, \tikzmark{d12}F}
\Infer{2}[\mvw]{\vdash \gG, F\parr\tikzmark{d11} F}
\Infer{1}[\mkrule{\textcolor{red}{\nu}}]{\vdash \gG,\tikzmark{d10}\mathbf{F}}

\Hypo{\pi_R\tikzmark{d7}}
\Infer{1}{\vdash \tikzmark{d8}G,\mathbf{F}\tikzmark{d6}}

\Hypo{\pi_M\tikzmark{d4}}
\Infer{1}{\vdash \tikzmark{d5}\mathbf{G},\tikzmark{d3}F}
\Infer{2}[\rcut]{\vdash \tikzmark{d9}\mathbf{G},\tikzmark{d2}F}
\Infer{2}[\rcut]{
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (b)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] ($(pic cs:d12)+(-.1cm,.3cm)$) .. controls +(150:4.2cm) and +(185:5.6cm) .. (b.west);
\end{tikzpicture}\;
\vdash \gG,\tikzmark{d1}F}
\end{prooftree}
\begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
\draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:d1)+(.1cm,.1cm)$)to ($(pic cs:d2)+(-.2cm,.-.4cm)$)  to ($(pic cs:d2)+(.2cm,.2cm)$)  to($(pic cs:d3)+(.2cm,.1cm)$) to($(pic cs:d4)+(0cm,.2cm)$)to($(pic cs:d4)+(-.4cm,.2cm)$) to($(pic cs:d5)+(.2cm,.1cm)$)  to($(pic cs:d6)+(-.1cm,.1cm)$) to($(pic cs:d7)+(0,.2cm)$) to($(pic cs:d7)+(-.4cm,.2cm)$) to($(pic cs:d8)+(0,.2cm)$)  to($(pic cs:d9)+(.2cm,.1cm)$)  to($(pic cs:d10)+(0,.1cm)$) to($(pic cs:d11)+(-.1cm,0cm)$) to($(pic cs:d12)+(.1cm,.2cm)$);
\end{tikzpicture}

A sketch of the main preproof $P$

We build $P$ so that the only branch which is not clearly validated is the one going infinitely many times through the loop. A thread validating this branch (in blue in Fig. <ref>) must go through the two cuts, and bounce on axioms in $\pi_M$ and $\pi_R$.
The trajectory of this thread in $\pi_M$  will simulate the run of $M$, and it will be allowed to exit $\pi_M$ if and only if $M$ terminates.

We now give an example of one of the simplest gadgets used to perform this simulation: the increment gadget on the first counter.
Consider a state $p$ of the machine $M$, whose action is to increment the first counter and go to state $q$. Assume counter values $(n,m)$ are encoded by a constraint stack $\lc^n\rc\lc^m\rc$, where $\lc$ (resp. $\rc$) stands for a left (resp. right) constraint on the unfolding of $F$, i.e. a relative address $\Ai\Al$ (resp. $\Ai\Ar$). This means that to increment the first counter, we need to add a left constraint at the top of the stack.
This can be performed by the following gadget, where nodes labeled $(p)$ and $(q)$ encode the current control state:

\begin{prooftree}
\Hypo{(q)\vdash G,\mathbf{F},\gA}

\Infer{0}[\rax]{\vdash G_\lc,F}
\Infer{0}[\rinf]{\vdash \gray{G_\rc,A}}
\Infer{2}[\we]{\vdash G_\lc\tensor G_\rc,F,\gA}
\Infer{1}[\mm]{\vdash \mathbf{G},F,\gA}

\Infer{2}[\rAcut]{(p)\vdash G,F,\gA}
\end{prooftree}}

Here $A$ is an auxiliary formula $\nu X.(X\parr X)\tensor X$, that can be duplicated as required and used to build axiomless valid proofs, denoted by an $\infty$ metarule. The rule (Acut) denotes a cut combined with a duplication of $A$.

A thread entering node $(p)$ upwards with constraint stack $\lc^n\rc\lc^m\rc$ will enter node $(q)$ with constraint stack $\lc^{n+1}\rc\lc^m\rc$.

In order to fully simulate the run of $M$, we also need to design gadgets simulating increment on the second counter, as well as decrement and zero test on both counters.
The main difficulty lies in the tests performed by the machine: we want the thread to follow a conditional branching, depending on the value of the constraint stack. This can be done, but because of the linearity of the proof system, we cannot avoid leaving some extra constraints encoding the results of the tests. These “garbage constraints” will be collected by the thread on its path downwards in $\pi_M$, after the simulation of the machine is completed.
Since we want to finish with empty constraint, we need to erase these garbage constraints.
To do this, we add a second gadget $\pi_R$ performing the computation in a dual way: garbage constraints are fed to the thread, which rewinds the computation while erasing these unwanted constraints. All gadgets in $\pi_R$ are dual versions of those in $\pi_M$. This technique is reminiscent of the one used by Bennett <cit.> to prove Turing-completeness of reversible Turing machines, where a history of the computation is produced to guarantee reversibility, then this history is erased by rewinding the computation.

We can finally exit this detour with no constraint, and perform a visible $\nu$-unfolding on the main branch (in red in Fig. <ref>), before looping back to the root of the proof.

The global pre-proof $P$ will be a valid proof according to the criterion if and only if the machine $M$ halts.

Notice that among the simplifications we made here for clarity of exposition, the auxiliary formula $A$ needed in some gadgets has been removed from the main preproof $P$.

§.§ A hierarchy of decidable validity conditions

In order to recover a decidable criterion, we will consider restrictions on the constraint stack of valid threads.

If $t$ is a thread, we define its height $h(t)\in\omega+1$ to be the supremum of the size of the stack of $\Athread$ along its run on $\weight{t}$.

Let $k\in\N$. An infinite branch is $k$-valid if there is a thread of height at most $k$ validating it. A proof $P$ is a $k$-proof if every infinite branch of $P$ is $k$-valid.

The two following theorems show that the height parameter $k$ induces a hierarchy of decidable criteria, whose union matches the full validity criterion.

If $P$ is a valid circular proof of , there exists $k\in\N$ such that $P$ is a $k$-proof.

Given a circular pre-proof $P$ of and an integer $k$, it is decidable whether $P$ is a $k$-proof.

We now give a brief proof sketch to give an intuition on how to prove Theorems <ref> and <ref>. See Appendix for details.

We will use the fact that once a starting point for a thread has been chosen, the thread evolves deterministically along the proof tree until a visible event occur. We define the notion of minimal shortcut which is a part of a thread with no visible weight, bouncing on an axiom, and ending in the first point where the constraint stack is empty. It corresponds to an $\epsilon$-path.

By bounding the maximal height of the stack by $k$, we can detect loops or declare stack overflow, and we are able to compute the unique minimal shortcut (if it exists) for each starting point in the finite proof graph.
Now, checking validity of the proof can be done using an algorithm for straight threads <cit.>, allowing them to take these shortcuts.

Theorem <ref> is obtained by taking the maximal height reached by all minimal shortcuts of the proof graph.

Combining Theorems <ref> and <ref>, we obtain that validity of a circular pre-proof of is in $\Sigma^0_1$, i.e. recursively enumerable. Together with the reduction from Sec. <ref>, we obtain the following corollary:

The problem of deciding whether a circular pre-proof of is a proof is $\Sigma^0_1$-complete.

The previous definition of validity is too weak to ensure cut-elimination for ,

which is not a strictly linear sequent calculus (as $\muMLLi$ is)

since commutation/external reductions for the  connective induce the duplication of a subproof. As a result, the extension of the validity condition in Section <ref> fails to ensure productivity and validity of cut-elimination as shown in figure <ref>.(i).

$  \begin{array}{l|l|l}
\hspace{-.6cm}    \pi_k =
\scalebox{.85}{
\begin{prooftree}
\Hypo{}
\Infer 1[\rax$\dagger$]{\vdash T\tikzmark{add16},T^\perp\tikzmark{add17}}
\Infer 1[\rbot]{\vdash \bot,T\tikzmark{add15},T^\perp\tikzmark{add18}}
\Hypo{}
\Infer 1[\rax$\ddagger$]{\vdash T,T^\perp}
\Infer 1[\rbot]{\vdash \bot,T,T^\perp}
\Infer 1[\scriptsize{$\color{red}{\rmu^k}$}]{{\vdash \bot, T,T^\perp}}
\Infer 2 [\rwith]{\vdash \bot\with\bot, T\tikzmark{add14},T^\perp\tikzmark{add19}}
\Hypo{\vdash S,\orig{a}T\tikzmark{add20}}
\Infer 2[\rcut]{\vdash \bot\with\bot, S,T\tikzmark{add13}}
\Infer 1[\rmu,\rparr]{\vdash S,T\tikzmark{add12}}
\Infer 1[\rnu]{\vdash S,T\tikzmark{add11}
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (b)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (a.north east) .. controls +(20:1.2cm) and +(0:4.5cm) .. (b.east);
\end{tikzpicture}\;}
\end{prooftree} \begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
\draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:add11)+(0cm,.1cm)$) to ($(pic cs:add12)+(-0.1cm,.1cm)$) to($(pic cs:add13)+(0,.1cm)$) to($(pic cs:add14)+(.1cm,-0.1cm)$) to($(pic cs:add15)+(0,-.1cm)$)to($(pic cs:add16)+(-0.1cm,.3cm)$)to($(pic cs:add17)+(-0.1cm,.3cm)$)to($(pic cs:add18)+(-.2cm,.1cm)$)to($(pic cs:add19)+(0,.1cm)$)to($(pic cs:add19)+(1cm,-.1cm)$)to($(pic cs:add20)+(-0.1cm,-.1cm)$)to($(pic cs:add20)+(0,.3cm)$);
\end{tikzpicture}}
\hspace{.2cm}    &
\qquad
\scalebox{.85}{
\begin{prooftree}
\Hypo{\orig{a}\vdash S,T}
\Infer 1[\rbot]{\vdash \bot,S,T}
\Hypo{\vdash S,\orig{aa}T}
\Infer 1[\rbot]{\vdash \bot, S,T}
\Infer 2[\rwith]{\vdash \bot\with\bot, S,T}
\Infer 1[\rmu,\rparr]{\vdash S,T
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (bb)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (aa.north east) .. controls +(10:2cm) and +(0:4.5cm) .. (bb.east);
\end{tikzpicture}\;}
\Infer 1[\rnu]{          \begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (b)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (a.north east) .. controls +(160:2cm) and +(180:2.5cm) .. (b.east);
\end{tikzpicture}\;\vdash S,T}
\end{prooftree}
} \hspace{1cm}
&Sl(\pi_k) \ni
\scalebox{.85}{
\begin{prooftree}
%    \Hypo{}
%    \Infer 1[\rax$\dagger$]{\vdash T\tikzmark{add16},T^\perp\tikzmark{add17}}
%    \Infer 1[\rbot]{\vdash \bot,T\tikzmark{add15},T^\perp\tikzmark{add18}}
\Hypo{}
\Infer 1[\rax]{\vdash T,T^\perp}
\Infer 1[\rbot]{\vdash \bot,T,T^\perp}
\Infer 1[\scriptsize{$\rmu^k$}]{{\vdash \bot, T,T^\perp}}
%    \Infer 2
\Infer 1
[\rwithr]{\vdash \bot\with\bot, T,T^\perp}
\Hypo{\vdash S,\orig{a}T}
\Infer 2[\rcut]{\vdash \bot\with\bot, S,T}
\Infer 1[\rmu,\rparr]{\vdash S,T}
\Infer 1[\rnu]{\vdash S,T
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (b)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (a.north east) .. controls +(20:1.2cm) and +(0:4.5cm) .. (b.east);
\end{tikzpicture}\;}
\end{prooftree}}
\\[-.5cm]
(i) & (ii) & (iii)
\end{array}

(i) Pre-proof family $(\pi_k)_{k\in\mathbb{N}}$ with  $S= \mu Y.((\bot\with\bot)\parr Y), T=\nu X.X$. Note that we omit the occurrences and that $k$ is a parameter fixing how many times the $\mu$ rule (in red) should be applied to the sequent $\vdash \bot, T,T^\perp$. (ii) Result of applying (infinitary) cut-elimination to $\pi_1$. (iii) Example of a slice of $\pi_k$.

The result of cut-elimination on the proofs in the sequence $(\pi_k)_{k\geq 0}$ can be split into the following cases:

(i) from $\pi_0$, cut-elimination is productive and produces a valid cut-free proof;

(ii) from $\pi_1$, cut-elimination  produces an invalid pre-proof (see Figure <ref>.(ii)):
any infinite branch following only finitely many times the left back-edge is invalid;

(iii) from $\pi_k$, for $k\geq 2$ it is not even productive.

Indeed, in these examples, each $\pi_k$ contains exactly one infinite
branch which is supported by a thread on $T$ bouncing on the left-most
axiom and this thread is valid.
Still, this does not ensure productivity nor validity.
For instance, $\pi_1$ reduces to the following pre-proof:

$$  \begin{prooftree}
\Hypo{\orig{a}\vdash S,T}
\Infer 1[\rbot]{\vdash \bot,S,T}
\Hypo{\vdash S,\orig{aa}T}
\Infer 1[\rbot]{\vdash \bot, S,T}
\Infer 2[\rwith]{\vdash \bot\with\bot, S,T}
\Infer 1[\rmu,\rparr]{\vdash S,T
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (bb)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (aa.north east) .. controls +(10:2cm) and +(0:4.5cm) .. (bb.east);
\end{tikzpicture}\;}
\Infer 1[\rnu]{          \begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (b)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (a.north east) .. controls +(160:2cm) and +(180:2.5cm) .. (b.east);
\end{tikzpicture}\;\vdash S,T}
\end{prooftree}

which is not valid since any infinite branch which takes only finitely many times the left back-edge is invalid.

To understand the problem, consider the first step of cut-reduction (from $\pi_k$, for any $k$):
it is a $\rcut/\rwith$ commutation step, which copies the right-premiss of
the cut (ie. the
non-wellfounded part of the proof): after this step, the pre-proof contains
two infinite branches, but only one thread to validate them.
While the leftmost copy can be validated by the original thread, the
rightmost copy does not contain a residual of the original thread. Of course,
one might consider a thread originated in the cut inference, but that
will not suffice to ensure validity, nor productivity, as $\pi_2$ examplifies: its rightmost branch produces bottom rule.

§.§.§ Sliced proof system and its cut-reduction

This issue is solved by refining the criterion using slices <cit.> and requiring that there exists
a supporting thread not only for every infinite branch of the proof, but also for every infinite branch of every persistent slice of the pre-proof.
In linear logic, an additive slice is a subtree of a sequent proof obtained by removing, for any of its $\rwith$ inference, the subtree rooted in one of its premisses (see Appendix <ref> for details and precise definitions).

is obtained by extending with the following three inference rules:

\Hypo{\vdash A, \Gamma}
\Infer 1[\rwithl]
{\vdash A\with B, \Gamma}
\end{prooftree}
\qquad \begin{prooftree}
\Hypo{\vdash B, \Gamma}
\Infer 1[\rwithr]
{\vdash A\with B, \Gamma}
\end{prooftree}
\qquad
\begin{prooftree}
\Hypo{}
\Infer 1[$\rdai$]{\vdash \Gamma}
\end{prooftree}

Partially sliced pre-proofs are the non-wellfounded

A(n additive) slice is a $\rwith$-free, $\rdai$-free, -preproof.

To a $\muMALLi$ sequent (pre-)proof, one can associate a set of slices
by keeping, for each $\rwith$ inference, only one of its premisses and replacing the $\rwith$ with  the corresponding inference in $\rwithl,\rwithr$
by applying corecursively one of the following two reductions:

$$    \scalebox{.9}{
\begin{prooftree}
\Hypo{\pi_1}
\Infer 1{\vdash A_1, \Gamma}
\Hypo{\pi_2}
\Infer 1{\vdash A_2, \Gamma}
\Infer 2[\rwith]{\vdash A_1\with A_2, \Gamma}
\end{prooftree}
\begin{prooftree}
\Hypo{\pi_1}
\Infer 1{\vdash A_1, \Gamma}
\Infer 1[\rwithl]
{\vdash A_1\with A_2, \Gamma}
\end{prooftree}, \begin{prooftree}
\Hypo{\pi_2}
\Infer 1{\vdash A_2, \Gamma}
\Infer 1[\rwithr]
{\vdash A_1\with A_2, \Gamma}
\end{prooftree}

More precisely:

The set of slices of $\pi$, $Sl(\pi)$, is defined corecursively by

\scalebox{.9}{$
\Hypo{\pi_1}
\Infer 1{\vdash A_1, \Gamma}
\Hypo{\pi_2}
\Infer 1{\vdash A_2, \Gamma}
\Infer 2[\rwith]{\vdash A_1\with A_2, \Gamma}
\end{prooftree}
\right) =
%\left\{ \begin{prooftree}
%      \Hypo{\pi'_1}
%      \Infer 1{\vdash A_1, \Gamma}
%      \Infer 1[\rwithl]
%             {\vdash A_1\with A_2, \Gamma}
%        \end{prooftree}, \pi'_1\in Sl(\pi_1)
%\bigcup \left\{\begin{prooftree}
%      \Hypo{\pi'_2}
%      \Infer 1{\vdash A_2, \Gamma}
%      \Infer 1[\rwithr]
%             {\vdash A_1\with A_2, \Gamma}
%        \end{prooftree}, \pi'_2\in Sl(\pi_2)
%\right\}        $$
\left\{\begin{prooftree}
\Hypo{\pi'_i}
\Infer 1{\vdash A_i, \Gamma}
\Infer 1[\rwithi]
{\vdash A_1\with A_2, \Gamma}
\end{prooftree},
\begin{array}{c}
\pi'_i\in Sl(\pi_i),\\
\end{array}
\right\}

(The other inferences are treated homomorphically.)

Fig. <ref>.(iii) gives an example of a slice.

§.§.§ Cut-reductions for sliced proofs

Cut-reduction rules for (partial) slices of $\muSMALLi$ extend those for
$\muMALLi$ with specific rules for sliced additives and $\rdai$.
Indeed, one may have a problematic situation, e.g. when a $\rwithl$ shall interact
with a $\roplusr$: cut-elimination cannot be performed by relying on subproofs.

The sliced additive principal case is reduced as follows,
\Hypo{\pi_i}
\Infer 1{\vdash A_i, \Gamma}
\Infer 1[\rwithi]
{\vdash A_1\with A_2, \Gamma}
\Hypo{\pi'_j}
\Infer 1{\vdash A^\perp_j, \Gamma}
\Infer 1[\roplusj]
{\vdash A^\perp_1\oplus A^\perp_2, \Delta}
\Infer 2 [\rcut]{\vdash \Gamma, \Delta}
\end{prooftree}
$\rightarrow \left\{
\begin{array}{cc}
\begin{prooftree}\Hypo{}\Infer 1[$\rdai$]{\vdash \Gamma,\Delta}\end{prooftree} & \text{if }i\neq j\\
\begin{prooftree}
\Hypo{\pi_i}
\Infer 1{\vdash A_i, \Gamma}
\Hypo{\pi'_i}
\Infer 1{\vdash A^\perp_i, \Delta}
\Infer 2 [\rcut]{\vdash \Gamma, \Delta}
\end{prooftree}  & \text{if }i = j\\
\end{array}
\right.$

if $\{A^\perp_1\with A^\perp_2, {A'}_1\oplus {A'}_2\}\in\dbot$, with $r = (\mathsf{princ}, \{A^\perp_1\with A^\perp_2, {A'}_1\oplus {A'}_2\})$.

\Hypo{\C C}
\Hypo{\pi_i}
\Infer 1
{\vdash A^\perp_i, \Gamma}
\Infer 1[\rwithi]
{\vdash A^\perp_1\with A^\perp_2, \Gamma}
\Hypo{\pi'_j}
\Infer 1{\vdash {A'}_j, \Gamma}
\Infer 1[\roplusj]
{\vdash {A'}_1\oplus {A'}_2, \Delta}
\Infer 3 [{\scriptsize\ensuremath{\mathsf{mcut(\iota, \perp\!\!\!\perp)}}}\xspace]{\vdash \Sigma}
\end{prooftree}

\left\{
\begin{array}{cc}
\begin{prooftree}\Hypo{}\Infer 1[$\rdai$]{\vdash \Sigma}\end{prooftree} & \text{if }i\neq j\\[12pt]
\begin{prooftree}
\Hypo{\C C}
\Hypo{\pi_i}
\Infer 1{\vdash A^\perp_i, \Gamma}
\Hypo{\pi'_i}
\Infer 1{\vdash A'_i, \Delta}
\Infer 3 [{\scriptsize\ensuremath{\mathsf{mcut(\iota, \perp\!\!\!\perp')}}}\xspace]{\vdash \Sigma}
\end{prooftree}  & \text{if }i = j\\
\text{where }\dbot'=\dbot\cup\{\{A^\perp_i,{A'}_i\}\}&
\end{array}
\right.$$

\Hypo{\C C}
\Hypo{}
\Infer 1[\rdai]
{\vdash \Gamma}
\Infer 2 [{\scriptsize\ensuremath{\mathsf{mcut(\iota, \perp\!\!\!\perp)}}}\xspace]{\vdash \Sigma}
\end{prooftree}
\underset{r}{\longrightarrow}
\begin{prooftree}
\Hypo{}
\Infer 1[\rdai]
{\vdash \Sigma}
\end{prooftree} \quad \text{with $r = (\mathsf{princ}, \dai)$.}$$

Notions of $b$-paths and $\epsilon$-paths can be naturally extended to additive slices.

§.§.§ Persistent slices

Persistent slices are introduced precisely as those in which no case of the above mismatch ever occurs:

Given a slice $\pi$, a $\rwithi$ rule of principal formula $A_1\with A_2$
occurring in $\pi$ is said to be

well-sliced if
no $b$-path starting down from the $A_1\with A_2$ occurrence of
this sequent ends in a formula
$A^\perp_1\oplus A^\perp_2$ that is the principal formula for a $\roplusj$ inference with $i\neq j$.

A slice is persistent if all its $\rwithi$ occurrences are well-sliced.

Pre-proof in Fig. <ref>.(iii) is (obviously) a persistent slice.

The following two properties of persistent slices are the key for the cut-elimination property:

All reducts of a persistent slice are $\rdai$-free, and therefore are slices.

If $\pi \rightarrow^* \pi'$ (resp. $\pi \rightarrow^\omega \pi'$) and

$S' \in Sl(\pi')$, then there is a

$S\in Sl(\pi)$

such that $S\rightarrow^* S'$ (resp. $S \rightarrow^\omega S'$).

§.§.§ Additive validity

Def <ref> and <ref> of (pre-)threads directly adapt to the additives – as they are not specific to – and allow us to consider the following definition:

A persistent slice is valid if it is valid in the multiplicative sense[That is, every infinite branch of the slice is visited by a valid thread having its visible part contained in the branch.].

A pre-proof $\pi$ is valid if all its persistent slicings are valid.

\hspace{2cm}\pi_{\mathsf{filter}} = \quad
%    \scalebox{.85}{
\begin{prooftree}
\Hypo{\pi_k}
\Infer{1}{\vdash N}
\Hypo{}
\Infer{1}[\rax]{B \vdash B}
\Hypo{\orig{adda} S \vdash S}
\Infer{2}[\rnul,\rtensorl,\rnur,\rtensorr]{S\vdash S}
\Infer{1}[\ronel]{1, S \vdash S}
\Hypo{\orig{addb}{N, S \vdash S} }
\Hypo{\pi_{neg}}
\Infer{1}[]{B\vdash B}
\Hypo{}
\Infer{1}[\rax]{S\vdash S}
\Infer{2}[\rnul,\rtensorl,\rnur,\rtensorr]{S\vdash S}
\Infer{2}[\rcut]{N, S\vdash S}
\Infer{1}[\rweakbooll]{N, B, S\vdash S}
\Infer{1}[\rnul,\rtensorl]{N, S\vdash S}
\Infer{2}[\rmul,\roplusl]{N, S\vdash S
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (addbb)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (addb.north) .. controls +(50:7cm) and +(-5:11.5cm) .. (addbb.north east);
\end{tikzpicture}\;}
\Infer{2}[\rcut]{
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (addaa)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (adda.north east) .. controls +(150:4cm) and +(190:5cm) .. (addaa.east);
\end{tikzpicture}\;
S\vdash S}
\end{prooftree}
%    }

Example of an additive circular proof

The circular pre-proof of Fig. <ref> is an example of a valid additive circular proof. It corresponds to the last program considered in the introduction.

We have studied non-weelfounded and circular proofs of and defined an extended validity criterion for the  pre-proofs of compared to previous work by Baelde, Doumane and Saurin <cit.>. We have shown that our criterion enjoys cut elimination and soundness, but reaches the barrier of undecidability: in the purely multiplicative fragment already, a parameter has to be bouned by an explicit value to make the criterion decidable.

For future work, we plan to investigate whether this decidability result still holds when adding the additive connectives.

We also want to extend these results to more relaxed criteria, for instance where the visible parts are only required to meet the validated branch infinitely often.

A less sequential variant of circular proofs is also currently developed by De and Saurin <cit.>, under the name infinets: the canoncity and absence of commutation rules of proof nets may have good properties with respect to cut-elimination and we expect that bouncing validity may be fruitful in their setting.

Finally, the present work is a first step in improving the compositionality of circular proofs. In addition to strengthening our cut-elimination result us mentioned above, we plan to investigate how one can import results from sized types <cit.> or copattern <cit.> approach which also have good proprerties with respect to compositionality and may be used in an infinitary scenario <cit.>.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

authorpersonAndreas Abel.
Mixed inductive/coinductive types and strong
normalization. In booktitleAsian Symposium on Programming
Languages and Systems. Springer, pages286–301.

authorpersonAndreas Abel.
titleCompositional Coinduction with Sized Types.
Abstract for the invited talk at the 13th IFIP WG 1.3 International
Workshop on Coalgebraic Methods in Computer Science (CMCS 2016), Eindhoven,
the Netherlands, 2-3 April 2016.

[Abel and PientkaAbel and Pientka2016]
authorpersonAndreas Abel and
personBrigitte Pientka. year2016.
Well-founded recursion with copatterns and sized
journalJournal of Functional Programming
volume26 (year2016), pages61.

ICFP 2013 special issue.

[Abel, Pientka, Thibodeau, and SetzerAbel
et al2013]
authorpersonAndreas Abel, personBrigitte
Pientka, personDavid Thibodeau, and personAnton
Setzer. year2013.
Copatterns: programming infinite structures by
observations. In booktitleThe 40th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
'13, Rome, Italy - January 23 - 25, 2013,
editorpersonRoberto Giacobazzi and
personRadhia Cousot (Eds.). publisherACM,

[Baelde, Doumane, and SaurinBaelde
et al2016]
authorpersonDavid Baelde, personAmina
Doumane, and personAlexis Saurin.
Infinitary Proof Theory: the Multiplicative
Additive Case. In booktitle25th EACSL Annual Conference
on Computer Science Logic, CSL 2016, August 29 - September 1, 2016,
Marseille, France (seriesLIPIcs),
Vol. volume62. publisherSchloss Dagstuhl -
Leibniz-Zentrum fuer Informatik, pages42:1–42:17.

authorpersonC. H. Bennett.
Logical Reversibility of Computation.
journalIBM J. Res. Dev. volume17,
number6 (dateNov. year1973),

[Brotherston and SimpsonBrotherston and
authorpersonJames Brotherston and
personAlex Simpson. year2011.
Sequent calculi for induction and infinite
journalJournal of Logic and Computation
volume21, number6 (dateDec.
year2011), pages1177–1216.

[Cave, Ferreira, Panangaden, and PientkaCave
et al2014]
authorpersonAndrew Cave, personFrancisco
Ferreira, personPrakash Panangaden, and
personBrigitte Pientka. year2014.
Fair Reactive Programming. In
booktitleProceedings of the 41st ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages
(seriesPOPL '14). publisherACM,
addressNew York, NY, USA, pages361–372.

[Dax, Hofmann, and LangeDax
et al2006]
authorpersonChristian Dax, personMartin
Hofmann, and personMartin Lange.
A Proof System for the Linear Time
\(\mathrm{\mu}\)-Calculus. In booktitleFSTTCS 2006:
Foundations of Software Technology and Theoretical Computer Science, 26th
International Conference, Kolkata, India, December 13-15, 2006,
Proceedings. pages273–284.

[De and SaurinDe and Saurin2019]
authorpersonAbhishek De and personAlexis
Saurin. year2019.
Infinets: the parallel syntax for non-wellfounded
proof-theory. In booktitleAutomated Reasoning with Analytic
Tableaux and Related Methods – TABLEAUX 2019
(seriesLecture Notes in Computer Science),
editorpersonSerenella Cerrito and
personAndrei Popescu (Eds.), Vol. volumexxxx.
publisherSpringer, pagesXXX–YYY.
to appear

authorpersonAmina Doumane.
titleOn the infinitary proof theory of logics with
fixed points. (Théorie de la démonstration infinitaire pour les
logiques à points fixes).
thesistypePh.D. Dissertation. schoolParis
Diderot University, France.

[Doumane, Baelde, Hirschi, and SaurinDoumane
et al2016]
authorpersonAmina Doumane, personDavid
Baelde, personLucca Hirschi, and personAlexis
Saurin. year2016.
Towards Completeness via Proof Search in the Linear
Time \(\mu\)-calculus: The case of Büchi inclusions. In
booktitleProceedings of the 31st Annual ACM/IEEE Symposium
on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8,
2016, editorpersonMartin Grohe,
personEric Koskinen, and personNatarajan Shankar
(Eds.). publisherACM, pages377–386.

[Fortier and SantocanaleFortier and
authorpersonJérôme Fortier and
personLuigi Santocanale. year2013.
Cuts for circular proofs: semantics and
cut-elimination. In booktitleComputer Science Logic 2013
(CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy
(seriesLIPIcs), editorpersonSimona
Ronchi Della Rocca (Ed.), Vol. volume23.
publisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik,

authorpersonEduardo Giménez.
Structural Recursive Definitions in Type Theory.
In booktitleProceedings 25th Int. Coll. on
Automata, Languages and Programming, ICALP'98, Aalborg, Denmark, 13–17 July
1998, editorpersonK. G. Larsen,
personS. Skyum, and personG. Winskel (Eds.).
seriesLNCS, Vol. volume1443.
publisherSpringer-Verlag, addressBerlin,

authorpersonJean-Yves Girard.
Linear Logic.
journalTheor. Comput. Sci.  volume50
(year1987), pages1–102.

authorpersonJean-Yves Girard.
Towards a Geometry of Interaction. In
booktitleCategories in Computer Scienc e and Logic
(seriesContemporary Mathematics).
publisherAMS, pages69–108.

authorpersonJean-Yves Girard.
Locus Solum.
volume11 (year2001),

[Hughes and van GlabbeekHughes and van
authorpersonDominic J. D. Hughes and
personRob J. van Glabbeek. year2005.
Proof nets for unit-free multiplicative-additive
linear logic.
journalACM Trans. Comput. Log.
volume6, number4 (year2005),

authorpersonPierre Hyvernat.
The Size-Change Termination Principle for
Constructor Based Languages.
journalLogical Methods in Computer Science
volume10, number1 (year2014).

[Janin and WalukiewiczJanin and
authorpersonDavid Janin and personIgor
Walukiewicz. year1995.
Automata for the Modal mu-Calculus and related
Results. In booktitleMathematical Foundations of Computer
Science 1995, 20th International Symposium, MFCS'95, Prague, Czech Republic,
August 28 - September 1, 1995, Proceedings (seriesLecture
Notes in Computer Science), editorpersonJirí
Wiedermann and personPetr Hájek (Eds.),
Vol. volume969. publisherSpringer,

authorpersonN. P. Mendler.
Inductive Types and Type Constraints in the Second
Order Lambda Calculus.
journalAnnals of Pure and Applied Logic
volume51, number1 (year1991),

authorpersonMarvin L. Minsky.
Recursive Unsolvability of Post's Problem of "Tag"
and other Topics in Theory of Turing Machines.
journalAnnals of Mathematics volume74,
number3 (year1961), pages437–455.

authorpersonGrigori E Mints.
Finite investigations of transfinite derivations.
journalJournal of Soviet Mathematics
volume10, number4 (year1978),

authorpersonLuigi Santocanale.
A Calculus of Circular Proofs and Its Categorical
Semantics. In booktitleFoundations of Software Science and
Computation Structures (seriesLecture Notes in Computer
Science), editorpersonMogens Nielsen and
personUffe Engberg (Eds.), Vol. volume2303.
publisherSpringer, pages357–371.

authorpersonKazushige Terui.
Computational ludics.
journalTheoretical Computer Science
volume412, number20 (year2011),

§ APPENDICES

§.§ The multicut rule

A new phenomenon occurs in the presence of axioms. Consider for instance the following pre-proof where $F=\phi_\alpha$ and $G=\phi_\beta$:

\scalebox{.9}{
\begin{prooftree}
\Infer{0}[\rax]{\vdash F, G^\perp}
\Hypo{\pi}
\Infer{1}[]{\vdash G, \Gamma}
\Hypo{\dots}
\Infer{3}[\rmcut]{\vdash F, \Gamma'}
\end{prooftree}}

In the finitary cut-elimination procedure, we would reduce this multicut to the derivation labelled $\rmcutone$ below. Doing so, we have to perform a substitution on addresses
(denoted by $[\alpha/\beta]$) to relocate the subderivation $\pi$
on the required occurrence. Another option, described by the derivation $\rmcuttwo$ below, is to avoid the renaming by keeping a link explicitely in the multicut rule.

\scalebox{.9}{
\begin{prooftree}
\Hypo{\pi[\beta/\alpha]}
\Infer{1}[]{\vdash F, \Gamma}
\Hypo{\dots}
\Infer{2}[\rmcutone]{\vdash F, \Gamma'}
\end{prooftree}
\qquad\text{or}\qquad\begin{prooftree}
\Hypo{\pi}
\Infer{1}[]{\vdash G\tikzmark{Gcut}, \Gamma}
\Hypo{\dots}
\Infer{2}[\rmcuttwo]{\vdash F\tikzmark{Fcut}, \Gamma'}
\end{prooftree}
\begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
\draw[rounded corners, smooth=2,red, opacity=.25] ($(pic cs:Fcut)+(-.1cm,.1cm)$)to ($(pic cs:Gcut)+(-.1cm,.1cm)$);
\end{tikzpicture}

We choose the last option to avoid the
global renaming, which would complicate our technical development.

A multicut rule will now be written as:

\Hypo{\vdash\Gamma_1\quad \dots\quad  \vdash\Gamma_n}
\Infer{1}[\rmcutpar]{\vdash\Gamma}
\end{prooftree}}$$

and comes with a function $\iota$ which shows how the occurrences of the conclusion are
distributed over the premisses (modulo renaming), and a relation
$\dbot$ specifiying which occurrences are cut-connected. A precise definition of the multicut rule is given in the appendix.

Given sequents $s, s_1, \dots, s_n$ where $n>0$
and such that $s_i,s_j$ are disjoint for all $i\neq j$,
a multicut of conclusion $s$ and premisses
$(s_i)_{i\in[1;n]}$ is given by an injection
$\iota : s \mapsto \cup_{i\in[1;n]} s_i$ and a
symmetric relation $\dbot \subseteq (\cup_{i\in[1;n]} s_i)^2$ such that:

* For all $F \in s$, $\iota(F) \equiv F$.

* For all $F,G \in \cup_{i\in[1;n]} s_i$,
$F \dbot G$ implies $F \equiv G^\perp$.

* $\mathrm{dom}(\dbot) =
(\cup_{i\in[1;n]} s_i) \setminus \mathrm{im}(\iota)$.

* Given two sequents $s_i$ and $s_j$, we say that they are $\dbot$-connected
on the formula occurrences $F,G$ when $F\in s_i$ and $G\in s_j$ such that $F \dbot G$.
We say that they are $\dbot$-connected, and we write $s_i \dbot s_j$,
when they are $\dbot$-connected on some $F,G$.  The relation $\dbot$ on sequents
must satisfy two conditions:

* two sequents must be $\dbot$-connected on at most one pair of
occurrences $F,G$;

* the graph of the relation $\dbot$ must be connected and acyclic.

We write this multicut rule as:

\Hypo{s_1\quad \dots \quad s_n}
\Infer{1}[\rmcutpar]{s}
\end{prooftree}$$

§.§ Cut elimination rules

We detail the rules of cut elimination introduced in <ref>.

External reductions are defined in <ref>.

In the first external rule, the sets $\C{C}_\Delta$ and $\C{C}_\Gamma$ are the
subsets of $\C C$ which are respectively connected to $\Delta$ and $\Gamma$
More precisely,

\begin{array}{cc}  \C C_\Delta = &\{
s \ | \ \exists s',
s\dbot^* s' \text{ and } s'
\text{ is $\dbot$-connected to }\\
&	 \vdash \Delta,\Gamma, F\otimes G
\text{ on an occurrence of } \Delta
\},
\end{array}$$

where $\dbot^*$ is the transitive closure of the relation $\dbot$ on sequents.
$\C C_\Gamma$ is defined similarly.

\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,F'}
\Hypo{\vdash \Gamma,G'}
\Infer{2}[\rtensor]{\vdash \Delta,\Gamma, F'\tensor G'}
\Infer{2}[\rmcutpar]{\vdash \Sigma_\Delta, \Sigma_\Gamma, F\tensor G}
\end{prooftree}
\begin{prooftree}
\Hypo{\C C_\Delta}
\Hypo{\vdash \Delta,F'}
\Infer{2}[\scriptsize\ensuremath{\mathsf{mcut(\iota', \perp\!\!\!\perp)}}]{\vdash \Sigma_\Delta, F}
\Hypo{\C C_\Gamma}
\Hypo{\vdash \Gamma,G'}
\Infer{2}[\scriptsize\ensuremath{\mathsf{mcut(\iota'', \perp\!\!\!\perp)}}]{\vdash \Sigma_\Gamma, G}
\Infer{2}[\rtensor]{\vdash \Sigma_\Delta, \Sigma_\Gamma, F\tensor G}
\end{prooftree}
\\[35pt]
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,F',G'}
\Infer{1}[\rparr]{\vdash \Delta, F'\parr G'}
\Infer{2}[\rmcutpar]{\vdash \Sigma, F\parr G}
\end{prooftree}
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,F',G'}
\Infer{2}[\scriptsize\ensuremath{\mathsf{mcut(\iota', \perp\!\!\!\perp)}}]{\vdash \Sigma, F,G}
\Infer{1}[\rparr]{\vdash \Sigma, F\parr G}
\end{prooftree}
\\[35pt]
%% \begin{prooftree}
%% \Hypo{\C C}
%% \Hypo{\vdash \Delta,F}
%% \Hypo{\vdash \Delta,G}
%% \Infer{2}[\rwith]{\vdash \Delta, F\with G}
%% \Infer{2}[\rmcutpar]{\vdash \Sigma, F\with G}
%% \end{prooftree}
%% &\underset{r}{\longrightarrow}&
%% \begin{prooftree}
%% \Hypo{\C C}
%% \Hypo{\vdash \Delta,F}
%% \Infer{2}[\scriptsize\ensuremath{\mathsf{mcut(\iota', \perp\!\!\!\perp)}}]{\vdash \Sigma, F}
%% \Hypo{\C C}
%% \Hypo{\vdash \Delta,G}
%% \Infer{2}[\scriptsize\ensuremath{\mathsf{mcut(\iota', \perp\!\!\!\perp)}}]{\vdash \Sigma, G}
%% \Infer{2}[\rwith]{\vdash \Sigma, F\with G}
%% \end{prooftree}
%% \\[35pt]
%% \begin{prooftree}
%% \Hypo{\C C}
%% \Hypo{\vdash \Delta,F_i}
%% \Infer{1}[\roplusi]{\vdash \Delta, F_1\oplus F_2}
%% \Infer{2}[\rmcutpar]{\vdash \Sigma, F_1\oplus F_2}
%% \end{prooftree}
%% &\underset{r}{\longrightarrow}&
%% \begin{prooftree}
%% \Hypo{\C C}
%% \Hypo{\vdash \Delta,F_i}
%% \Infer{2}[\scriptsize\ensuremath{\mathsf{mcut(\iota', \perp\!\!\!\perp)}}]{\vdash \Sigma, F_i}
%% \Infer{1}[\roplusi]{\vdash \Sigma, F_1\oplus F_2}
%% \end{prooftree}
%% \\[35pt]
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta, F'[\sigma X. F'/X]}
\Infer{1}[\rsigma]{\vdash \Delta, \sigma X. F'}
\Infer{2}[\rmcutpar]{\vdash \Sigma, \sigma X. F}
\end{prooftree}
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,F'[\sigma X. F'/X]}
\Infer{2}[\scriptsize\ensuremath{\mathsf{mcut(\iota', \perp\!\!\!\perp)}}]{\vdash \Sigma, F[\sigma X. F/X]}
\Infer{1}[\rsigma]{\vdash \Sigma, \sigma X. F}
\end{prooftree}
%% %% %% \\[35pt]
%% \begin{prooftree}
%% \Hypo{\C C}
%% \Infer{0}[\rtop]{\vdash \Delta, \top_\alpha}
%% \Infer{2}[\rmcutpar]{\vdash \Sigma, \top_\alpha}
%% \end{prooftree}
%% &\underset{r}{\longrightarrow}&
%% \begin{prooftree}
%% \Infer{0}[\rtop]{\vdash \Sigma, \top_\alpha}
%% \end{prooftree}
\end{array}$

\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta}
\Infer{1}[\rbot]{\vdash \Delta, \bot_\beta}
\Infer{2}[\rmcutpar]{\vdash \Sigma, \bot_\alpha}
\end{prooftree}
\underset{r}{\longrightarrow}
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta}
\Infer{2}[\scriptsize\ensuremath{\mathsf{mcut(\iota', \perp\!\!\!\perp)}}]{\vdash \Sigma}
\Infer{1}[\rbot]{\vdash \Sigma, \bot_\alpha}
\end{prooftree}
\hspace{1cm}
\begin{prooftree}
\Infer{0}[\rone]{\vdash \llone_\beta}
\Infer{1}[\rmcutpar]{\vdash \llone_\alpha}
\end{prooftree}
\underset{r}{\longrightarrow}
\begin{prooftree}
\Infer{0}[\rone]{\vdash \llone_\alpha}
\end{prooftree}

In the first reduction ($\rtensor/\rmcut$) we require that
$\iota(F\tensor G) = F'\tensor G'$ and take $\iota'$ and $\iota''$
that coincide with $\iota$ on $\Sigma_\Delta$ and $\Sigma_\Gamma$
respectively, and such that $\iota'(F)=F'$ and $\iota''(G)=G'$.
In the other reductions $\iota$ and $\iota'$ are similarly

External reduction rules,
where $r=(\mathsf{ext},F)$ and $F$ is the principal occurrence.

Note that the $\rtensor/\rmcut$  external reduction yields
multiple multicuts, though always on disjoint sub-trees.
Thus, is stable by external reductions.

In external reductions, we pushed a multicut away from the root,
above a logical rule.
If we start with a pre-proof and apply a reduction sequence where
external rules are applied infinitely often to each multicut, we
will produce at the limit a cut-free proof.
This is the reason why we say that external reductions are
productive. This is not the case for the internal reduction rules
given next.

Internal reductions are the principal reductions
given in <ref> together with the following two reductions:

* the merge $\rmcut/\rcut$ reduction

\scalebox{.9}{\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,F}
\Hypo{\vdash \Gamma,F^\bot}
\Infer{2}[\rcut]{\vdash \Delta,\Gamma}
\Infer{2}[\rmcutpar]{\vdash \Sigma}
\end{prooftree}}
\\[10pt]
\qquad\qquad\qquad
\ \underset{r}{\longrightarrow}\qquad
\scalebox{.9}{\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,F}
\Hypo{\vdash \Gamma,F^\bot}
\Infer{3}[
\scriptsize\ensuremath{
\mathsf{mcut(\iota, \perp\!\!\!\perp')}}\xspace]{
\vdash \Sigma}
\end{prooftree}}
\end{array}$$

where $\dbot'$ extends $\dbot$ with
$F\mathrel{\dbot'}F^\perp$ and

* the axiom reduction $\rmcut/\rax$

\scalebox{.9}{\begin{prooftree}
\Hypo{\C C}
\Infer{0}[\rax]{\vdash F, F'^\bot}
\Hypo{\vdash F'', \Gamma}
\Infer{3}[\rmcutpar]{\vdash \Sigma}
\end{prooftree}}
\\[10pt]
\qquad\quad\qquad\qquad\qquad
\ \underset{r}{\longrightarrow}\ \qquad
\scalebox{.9}{\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash F'', \Gamma}
\Infer{2}[\scriptsize\ensuremath{\mathsf{mcut(\iota', \perp\!\!\!\perp')}}\xspace]{\vdash \Sigma}
\end{prooftree}}
\end{array}$$

where $r=(\mathsf{CutAx},\{F,F'^\bot\})$,
and $\iota', \dbot'$ are defined as follows:

* for all $G \in \Sigma$,
if $\iota(G)=F$ then $\iota'(G)=F''$, otherwise

* $\dbot'=\dbot\cup\{\{F'',G\}| \{F,G\}\in\dbot\}$.

\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,F}
\Hypo{\vdash \Gamma,G}
\Infer{2}[\rtensor]{\vdash \Delta,\Gamma,F\tensor G}
\Hypo{\vdash \Theta,F'^\bot,G'^\bot}
\Infer{1}[\rparr]{\vdash \Theta,F'^\bot\parr G'^\bot}
\Infer{3}[\rmcutpar]{\vdash \Sigma}
\end{prooftree}
\\[20pt] \hspace{4cm}
\underset{r}{\longrightarrow}\qquad
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta,F}
\Hypo{\vdash \Gamma,G}
\Hypo{\vdash \Theta,F'^\bot,G'^\bot}
\Infer{4}[{\scriptsize\ensuremath{\mathsf{mcut(\iota, \perp\!\!\!\perp')}}}\xspace]{\vdash \Sigma}
\end{prooftree}
\\[15pt]
\text{where }
F\tensor G \mathrel{\dbot} G'^\bot\parr G'^\bot
\text{ and $\dbot'$ coincides with $\dbot$ except for }
F \mathrel{\dbot'} F'^\bot \text{ and } G \mathrel{\dbot'} G'^\bot
\\[35pt]
% \begin{prooftree}
% \Hypo{\C C}
% \Hypo{\vdash \Delta, F'_1}
% \Hypo{\vdash \Delta,F'_2}
% \Infer{2}[\rwith]{\vdash \Delta,F'_1\with F'_2}
% \Hypo{\vdash \Gamma,F_i^\bot}
% \Infer{1}[\roplusi]{\vdash \Gamma,F_1^\bot\oplus F_2^\bot}
% \Infer{3}[\rmcutpar]{\vdash \Sigma}
% \end{prooftree}
% \\[20pt] \hfill \underset{r}{\longrightarrow}\qquad
% \begin{prooftree}
% \Hypo{\C C}
% \Hypo{\vdash \Delta,F'_i}
% \Hypo{\vdash \Gamma,F_i^\bot}
% \Infer{3}[{\scriptsize\ensuremath{\mathsf{mcut(\iota, \perp\!\!\!\perp')}}}\xspace]{\vdash \Sigma}
% \end{prooftree}
% \\[15pt]
% \qquad\qquad\text{If } \{F'_1\with F'_2,F_1^\bot\oplus F_2^\bot\}\in\dbot, \quad\text{ where: } \qquad\dbot'\defeq\dbot\cup\{\{F'_i,F_i^\bot\}\}.
% \\[35pt]
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta, F'[\mu X.F'/X]}
\Infer{1}[\rmu]{\vdash \Delta,\mu X.F'}
\Hypo{\vdash \Gamma, {F}^\perp[\nu X.{F}^\perp/X]}
\Infer{1}[\rnu]{\vdash  \Gamma,\nu X.{F}^\perp}
\Infer{3}[\rmcutpar]{\vdash \Sigma}
\end{prooftree}
\\[20pt] \hfill \underset{r}{\longrightarrow}\qquad
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Delta, F'[\mu X.F'/X]}
\Hypo{\vdash \Gamma, {F}^\perp[\nu X.{F}^\perp/X]}
\Infer{3}[{\scriptsize\ensuremath{\mathsf{mcut(\iota, \perp\!\!\!\perp')}}}\xspace]{\vdash \Sigma}
\end{prooftree}
\\[15pt]
\text{where }
\mu X.F' \mathrel{\dbot} \nu X.{F}^\perp
\text{ and $\dbot'$ coincides with $\dbot$ except for }
F'[\mu X. F'/X] \mathrel{\dbot'} F^\bot[\nu X. F^\bot/X]
\\[35pt]
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Gamma}
\Infer{1}[\rbot]{\vdash \Gamma,\bot_\alpha}
\Infer{0}[\rone]{\vdash \llone_{\beta}}
\Infer{3}[\rmcutpar]{\Sigma}
\end{prooftree}
\quad\underset{r}{\longrightarrow}\quad
\begin{prooftree}
\Hypo{\C C}
\Hypo{\vdash \Gamma}
\Infer{2}[{\scriptsize\ensuremath{\mathsf{mcut(\iota, \perp\!\!\!\perp)}}}\xspace]{\Sigma}
\end{prooftree}
\quad \text{ where } \bot_\alpha \mathrel{\dbot} \llone_\beta
\end{array}$

Principal reductions,
where $r=(\mathsf{princ},\{F,F'^\bot\})$ with $\{F, F'^\bot\}$ the principal occurrences that have been reduced.

In internal reductions, the multicut remains at the root of the redex.
Thus, if a sequence of multicut reductions eventually involved only
internal reductions, it would not produce be productive.

The use of labels in reductions allows us to define in full details
our notion of reduction sequence and fairness.

A reduction sequence is a finite or infinite sequence
$\sigma = (\pi_i,r_i)_{i\in1+\lambda}$ with $\lambda\in\omega+1$,
where the $\pi_i$ are pre-proofs, the $r_i$ are labels
identifying multicut reduction rules and, for all $i\in\lambda$,
$\pi_i \underset{r_i}{\longrightarrow} \pi_{i+1}$.
The sequence is fair if for all $i\in\lambda$ and $r$
such that $\pi_i \underset{r}{\longrightarrow} \pi'$ there is
some $j\in\lambda$ such that $j \geq i$ and $\pi_j
\underset{r}{\longrightarrow} \pi_{j+1}$.

§.§ Cut elimination for

§.§.§ Trace of a reduction sequence

If $\C R$ is a reduction sequence starting from $\pi$, we start by defining the trace of $\C R$ to be the subtree of $\pi$ whose sequents occur in the reduction sequence as premisses of some multicut.
Note that each node of the trace corresponds to a well-formed inference:
indeed, if sequents $S$ and $S'$ are premisses of a same inference (which must
thus be a tensor or cut) and $S$ enters a multicut at some point in the
reduction sequence, then $S'$ must also enter a multicut – though not
necessarily the same one.
However, the trace may have unjustified sequents:
this happens when a sequents $S$ enters the multicut during the reduction
sequence but never leaves it; it will then be part of the trace but
the subtree of $\pi$ rooted in $S$ will not.

The unjustified sequents of the trace are called its border sequents.

Note that a border sequent cannot be the conclusion of an axiom rule nor a
cut rule in the initial derivation $\pi$.
If this were the case, by fairness, it would have been
absorbed by an $\rax/\rmcut$ or a $\rcut/\rmcut$ reduction respectively.
This allows to define the distinguished occurrence of a border
sequent as the principal occurrence of the logical rule applied to the border
sequent in $\pi$.

There is another reason why the trace of a reduction sequence might not
be a proof: its infinite branches may not be valid. The infinite
branches of the trace are also infinite branches of the proof $\pi$, thus they
are supported by valid threads of $\pi$, but these threads might not be
included in the trace. We show that this actually never happens.

§.§.§ The bouncing threads of the trace belong to the trace

This section is dedicated to proving the following theorem.

Let $T$ be the trace of a reduction sequence starting from a proof $\pi$,
and let $\beta$ be an infinite branch of $T$. If $t$ is a thread of $\pi$
validating $\beta$, then $t$ is also a thread of $T$.

We now introduce a
a useful technical tool called the residual of a pre-thread.

Let  $\C R$ be a finite reduction path starting from $\pi$ to $\pi'$
and let $t$ be a pre-thread of $\pi$.
Let $S'$ be the set of sequents of $\pi'$.
We call the residual of $t$
after the reduction $\C R$ the pre-thread
$t\cap \{(F,s,d)| s\in S', d\in \{\uparrow, \downarrow\}\}$.

By definition, the length of the residual of $t$ is smaller than the length
of $t$.

Let  $\C R$ be a finite reduction path starting from $\pi$ to $\pi'$,
let $T$ be its trace.
Let $t$ be a $b$-thread of $\pi$ and $t'$ its residual after $\C R$.
Then $t'$ is a $b$-thread.
Furthermore, if $t$ is a $B$-path of $\pi$,
then $t'$ is a $B$-path of $T$,
and $t'$ has the same endpoints as $t$.

It suffices to consider a single reduction step.
Most of the claims follow from a simple inspection of the reduction rules.
For the last one (i.e. $t$ and $t'$ have the same endpoints)
we have to additionnally rule out the possibility that, if $s$ and $s'$
are the endpoints of $t$, $s$ gets reduced at some point of the
reduction while $s'$ does not: this could only happen if $s$ (or $s'$)
was part of an $\rax/\rmcut$ reduction, but that would mean that our
$B$-path can be extended into an $h$-path (if the axiom is at the beginning
of the path) or the reverse of an $h$-path (if the axiom is at the end).

A pre-thread $t$ is a $B$-path of $\pi$ if:

* it is a maximal $b$-path of $\pi$,
i.e. there is no $b$-path of $\pi$ which contains $t$ as an infix;

* it cannot be extended as an $h$-path or as the reverse of an

Intuitively, the second condition means that the path cannot be extended
by an axiom on either side, possibly after silent steps corresponding
to $\Wwait$ weights.

Let $\C R=\{\pi_i,r_i\}_{i\in\omega}$ be a reduction sequence and
let $T=Tr(\C R)$ be its trace.

If $t$ is a $B$-path of $T$, then there is an index $i$ such that
the endpoints of $t$ are mcut-connected in the multicut of $\pi_i$.

As reductions are performed, the thread $t$ is simplified into
residuals. As long as these residuals remain non-empty, they are
still $b$-paths in their respective derivations, and they keep the same
endpoints because the only way to reduce one endpoint without the other
is through an $\rax/\rmcut$ reduction. Moreover, the length of
residuals only decreases. In fact, since $t$ is in the trace,
it strictly decreases infinitely often. Thus, at some point, the two
endpoints of $t$ are directly mcut-connected.

Let $t$ be a thread validating the branch $\beta$ in $\pi$. The visible part
of $t$ belongs to $\beta$, hence its belongs to the trace $T$. One needs to
prove that the hidden part belongs also to the trace.

Suppose by contradiction that some
$H=\psd{F_i}{s_i}{d_i}_{1\leq i\leq n}\in \hiddenP{t}$ leaves the trace.
Thus there is an index $j\leq n$ such that $s_j$ is a border sequent of the
trace. Take the maximal such $j$. If $d_j = {\uparrow}$ then, since the
hidden part $H$ ends in a sequent of $\beta$,
there must be a position $k\in]j;n[$ where
the path exits the subtree rooted in $s_j$ to re-enter $\beta$: we would
then have $s_k = s_j$, contradicting the maximality of $j$.
Hence, $d_j = {\downarrow}$.

Since $H$ is a b-path, and $d_j=\downarrow$, then  there is $k>j$ such that
$H[j,k]$ is a $b$-path:
keeping with the intuition that $b$-paths are well-bracketed words,
the opening bracket at position $j$ must have a corresponding closing
bracket at position $k$ such that the word in between is well-bracketed,
thus a $b$-path.
By maximality of $j$, $H[j,k]$ is in the trace.

Let $k$ be maximal with this property.   Note that $H[j,k]$ is a maximal
$b$-path in the trace, since $s_j$ is a border sequent and $k$
is chosen to be maximal. Let us show that $H[j,k]$ cannot be extended to an
$\epsilon$-path of the trace.
Suppose by contradiction that this is the case. Since $s_j$ is a border
sequent, $H[j,k]$ can be extended only on the right. Thus there is $l>k$
such that $H[j,l]$ is an $\epsilon$-path. Since $H[j,l]$ starts with a
downward direction, and since $\epsilon$-paths have the same direction in
their endpoints, we have that  $d_l={\downarrow}$.
Thus by the same reasoning as before, there is $m>l$ such that $H[l,m]$ is a
$b$-path. Thus $H[j,m]$ is a $b$-path, which contradicts the maximality of

We can now apply <ref> to $H[j,k]$:
at some point of the reduction, the sequents $s_j$ and $s_k$
are mcut-connected through the occurrences $F_j$ and $F_k$. Note that
$s_{k+1}$ belongs to $T$ (by maximality of $j$)
and that $F_{k+1}$ is a strict sub-occurrence of $F_k$ (otherwise, this
would contradict the maximality of $k$).
Cela ne marche que si les b-paths peuvent finir par des $\Wwait$,
ce qui n'est pas le cas…
Since $F_{k+1}$ is in the trace,
this means that $F_j$ has been reduced which is not possible since $s_j$ is
in the border of the trace.

In order to view a trace as a proof, we shall devise a way to
justify its border sequents. Intuitively, we will identify each distinguished
occurrence with the true constant $\top$. To achieve this formally,
we introduce a truncated proof system in the next section.
Before that, let us mention a key technical result, which builds on the
intuition that $b$-paths are simplified during cut elimination.

§.§ Truncated proof system

The truncated proof system builds on a truncation that forces
a semantics on particular occurrences.

A truncation $\tau$ is a partial function from
$\Sigma^*$ to $\{\top,\llzero\}$ such that:

* For any $\alpha \in \Sigma^*$,
if $\alpha\in\dom(\tau)$, then $\alpha^\perp\in \dom(\tau)$ and

* If $\alpha\in\dom(\tau)$ then for any $\beta\in\Sigma^+$,

Given a truncation $\tau$, the infinitary proof system  is
obtained by taking all the rules of together with the following rule for $\top$:

\begin{prooftree}
\Infer{0}[\rtop]{\vdash \Gamma, \top_\alpha}
\end{prooftree}

with the following proviso.
The rules of only apply when the address of their principal occurrence is not in
the domain of $\tau$, otherwise the following rule has to be applied:

\begin{prooftree}
\Hypo{\vdash \tau(\alpha)_{\alpha i},\Delta}
\Infer{1}[\rt]{ \vdash \phi_\alpha, \Delta}
\end{prooftree}
\qquad
\text{if }\alpha\in \dom(\tau)

The notions of thread and validity are the same as in .

As in <cit.> we define a classical truth semantics for
our truncated proof system.
Truncated occurrences (i.e. whose address is in
$\dom(\tau)$) are assigned their value under $\tau$.
The semantics of a unit $\top$ or $0$ is itself.
Then this semantics is propagated to more complex formulas inductively,
interpreting $\parr$ as disjunction, $\tensor$ as conjunction, and $\mu,\nu$
as least and greatest fixed points respectively.The semantics of an occurrence $F$ under a truncation $\tau$
is noted $\interp{F}$.
We establish, in the same way as in <cit.> that is sound wrt. this semantics:

If $\vdash \Gamma$ is provable in $\muMLLit$, then
$\interp{F}=\top$ for some $F\in \Gamma$.

quelles différences avec straight threads ?
Since is a sub-system of , we obtain as a corollary that
is sound wrt. the boolean semantics.

§.§ From traces to truncated proofs

Let $\pi$ be a pre-proof.
We define the relations $\approx_\pi$ and $\dbot_\pi$ as follows:

* $F\approx_\pi G$ if there is an $h$-path in $\pi$ from $F$ to $G$,
or from $G$ to $F$.

* $F\dbot_\pi G$ if there is a $b$-path in $\pi$ between $F$ and $G$.

The relations $\dbot_\pi$ and $\approx_\pi$ are symmetric —
note that the reverse of a $b$-path from $F$ to $G$ is a $b$-path from
$G$ to $F$.
The relation $\approx_\pi$ is reflexive.

Let $\C R$ be a reduction. The trace of $\C R$ cannot contain
an occurrence $F$ and two distinguished occurrences $G$ and $H$
such that $F\dbot_T G$ and $F\approx_T H$.

We proceed by contradiction.
Let $t_2$ be the $b$-path from $G$ to $F$, starting with a $\downarrow$
direction and ending with $\uparrow$.
Let $t_1$ be the path from $F$ to $H$. It must be an $h$-path, starting
and ending with $\uparrow$. Indeed, the reverse of an $h$-path would reach
$H$ with a $\downarrow$ which is absurd since $H$ is a distinguished
occurrence of a border sequent.

Let $t$ be the $b$-path obtained by gluing the path from $G$ to $F$
with the path from $F$ to $H$.
This path is a $B$-path of $T$, since its endpoints are distinguished
formulas, so they are in the border of the trace.

By applying <ref>, there is a point in the reduction
where the occurrences $G$ and $H$ are directly mcut-connected.

Since $G$ and $H$ are distinguished, they are principal occurrences of the
rules applied to their border sequents in $\pi$. Thus, considering the
point of the reduction where they are directly mcut-connected,
there is an internal redex on $G$ and $H$. By fairness it is reduced,
which contradicts the fact that they are distinguished occurrences
of border sequents.

By <ref> we can define the truncation
and truncated proof associated to a trace.

Let $\C R$ be a reduction sequence and $T$ be its trace. The truncation $\tau$ associated with $\C R$ is defined by setting:

* $\tau(F)=\llzero$ if there is a distinguished occurrence $G$ such that $F\dbot_T G$,

* $\tau(F)=\top$ if there is a distinguished occurrence $G$ such that $G\approx_T F$.

Let $T$ be the trace of a infinite internal reduction sequence starting from $\pi$, and let $\tau$ be the truncation associated to this reduction. The truncated proof $\pi_\tau$ is obtained from $T$ by replacing every border sequent $\vdash \phi_\alpha, \Gamma$, whose distinguished occurrence is $\phi_\alpha$ by the following derivation:

\Infer{0}[\rtop]{\vdash \top_{\alpha.i},  \Gamma}
\Infer{1}[\rt]{\vdash \phi_\alpha,  \Gamma}
\end{prooftree}$$

It is now easy to establish productivity of cut elimination.
Any fair reduction sequence produces a pre-proof.

By contradiction, consider a fair infinite sequence of internal multicut
reductions starting from $\pi$. Let $\pi_\tau$ be the truncated proof of
its trace.
Since no external reduction occurs,
it means that an occurrence $F$ in the conclusion of $\pi_\tau$ can only
be principal in an $\rax/\rmcut$ reduction of the considered sequence.
If $\iota$ is the injection associated to the multicut after that reduction,
the same observation holds for $\iota(F)$, and so on.
In short, any occurrence $F' \approx_{\pi_\tau} F$
will never be principal in a logical rule. Hence we can replace all
these occurrences by occurrences of $\bot$.
We thus obtain a proof of the sequent $\vdash \bot,\ldots,\bot$ which
contradicts the soundness of .

§.§.§ Proof of cut elimination

We have shown in <ref> that multicut reduction is productive.
To establish cut-elimination (<ref>), it only remains to prove that
the resulting (cut-free) pre-proof is actually a valid proof.

Let $\pi$ be a proof of conclusion $\vdash A$,
and $\pi'$ the cut-free pre-proof obtained by <ref>,
the limit of the multicut reduction process.
Any branch of $\pi'$ corresponds to a multicut reduction path.
For the sake of contradiction, assume that $\pi'$ is invalid.
It must thus have an invalid infinite branch $\beta=(s_i)_{i\in\omega}$,  corresponding
to an infinite reduction path $\C R$.
Let $\tau$ and $\theta$ be the associated truncation and
truncated proof in .

We set $\mathsf{Froz}(\beta)$ to be the set of occurrences of $\beta$
which are never principal. For convenience we will use the weakening rule:

\Hypo{\vdash \Gamma}
\Infer{1}[\rweak]{\vdash \Gamma,\Delta}
\end{prooftree}$$

Weakening is indeed admissible as long as the derivation on which it
is applied contains an infinite branch,
since one can let the weakened occurrences "travel" into this infinite branch.
Without loss of generality, we now assume that all occurrences of
$\mathsf{Froz}(\beta)$ have been weakened away in $\beta$.

We define the truncation $\tau'$ to be the truncation obtained by extending $\tau$ as follows.
For every occurrence $F_1\parr F_2$  which is principal in $\beta$, we set, for $i\in\{1,2\}$, $\tau'(F_i)=\llzero$ if $F_i \in \mathsf{Froz}(\beta)$.

Let $\beta_{\geq i}$ be the suffix of $\beta$ starting from the $i^{th}$ element.
If $\vdash \Gamma$ is the conclusion of $\beta_{\geq i}$, then for every  $\Delta\subseteq \Gamma$,  we define coinductively the proof ${\beta_{\geq i}}^\bot(\Delta)$ of conclusion $\vdash \Delta^\bot$ as follows. We proceed by case analysis on the rule applied to the conclusion of $\beta$.  This rule can be either a logical rule or a weakening.
If the rule is a weakening, then it is simulated by a weakening rule.
If it is a logical rule, then let $F$ be its principal occurrence. We set  $\Delta'=\Delta\setminus\{F\}$. We have either:

* $F =\sigma X. G$ where $\sigma\in\{\mu, \nu\}$.  We set $\overline{\sigma}$ to be the dual of $\sigma$, and:

$$\beta_{\geq i}^\bot(\Delta)=\begin{prooftree}
\Hypo{\beta_{\geq i+1}^\bot(\Delta', G[F/X]) }
\Infer{1}[]{\vdash \Delta'^\bot, G^\bot[F^\bot/X]}
\Infer{1}[\scriptsize ($\overline{\sigma}$)]{\vdash \Delta'^\bot,F^\bot}
\end{prooftree}$$

*  $F= G\otimes H$. Suppose wlog. that $G\in
s_{i+1}$ ($H$ left the branch $\beta$). We set $\Delta''=\Delta'\cap
s_{i+1}$ and:

$$\beta_{\geq i}^\bot(\Delta)=\begin{prooftree}
\Hypo{\beta_{\geq i+1}^\bot(\Delta'', G) }
\Infer{1}[]{\vdash \Delta''^\bot, G^\bot}
\Infer{1}[\rweak]{\vdash \Delta'^\bot, G^\bot, H^\bot}
\Infer{1}[\rparr]{\vdash \Delta'^\bot,F^\bot}
\end{prooftree}$$

* $F=G\parr H$ and  $G \in \dom(\tau')$ and $H\notin \dom(\tau')$,
or symmetrically. We set:

$$\beta_{\geq i}^\bot(\Delta)=
\begin{prooftree}

\Infer{0}[\rtp, \rtop]{\vdash  G^\bot}

\Hypo{\beta_{\geq i+1}^\bot(\Delta', H)}
\Infer{1}[]{\vdash \Delta'^\bot, H^\bot}
\Infer{2}[\rtensor]{\vdash \Delta'^\bot, F^\bot}
\end{prooftree}$$

* $F=G\parr H$, $G \in \dom(\tau')$ and $H\in \dom(\tau')$. In this case we set:

$$\beta_{\geq i}^\bot(\Delta)=
\begin{prooftree}

\Infer{0}[\rtp, \rtop]{\vdash  G^\bot}

\Infer{0}[\rtp, \rtop]{\vdash \Delta'^\bot, H^\bot}
\Infer{2}[\rtensor]{\vdash \Delta'^\bot, F^\bot}
\end{prooftree}$$

* $F=G\parr H$, $G \notin \dom(\tau')$ and $H\notin \dom(\tau')$. In this case we set:

$$\beta_{\geq i}^\bot(\Delta)=
\begin{prooftree}
\Hypo{\beta_{\geq i+1}^\bot(G)}
\Infer{1}[]{\vdash  G^\bot}

\Hypo{\beta_{\geq i+1}^\bot(\Delta', H)}
\Infer{1}[]{\vdash \Delta'^\bot, H^\bot}
\Infer{2}[\rtensor]{\vdash \Delta'^\bot, F^\bot}
\end{prooftree}$$

Observe now that
$\beta^\bot:=\beta_{\geq 0}^\bot$ is a proof in the truncated proof system
$\muMLLi_{\tau'}$ of conclusion $A^\bot$. Indeed, its threads (which
are necessarily straight threads since no cuts and axioms are involved)
are the duals of the threads of the branch $\beta$, which are by hypothesis
not valid.

Since $\muMLLi_{\tau'}$ is sound, we have that $\interp{A^\bot}=\top$. But the
truncated proof $\theta$ is a $\muMLLi_\tau$ proof of conclusion $A$, and again by soundness
we have that $\interp{A}=\top$: contradiction.

§.§ Extending cut-elimination to the additives

In this appendix, we give details on the proof of cut-elimination theorem for full . First, we provide precise definition for the sliced proof system and the associated partial cut-reduction relation and the introduce persistent slices. We can then formulate precisely the additive validity criterion and prove the cut-elimination theorem.
The proof schema of additive cut-elimination follows the same pattern as in the multiplicative case but we check that the multiplicative result can indeed be lifted. Most of the definitions can be very straightforwardly lifted to the additive but for the soundness result some work has to be done: we show that we do not need a full soundness result but that a soundness result wrt. a specific class of derivations, called $\tau$-adapted proofs, which then allows us to prove productivity of cut-elimination and preservation of validity by fair-reduction sequences.

$  \pi_k = \begin{prooftree}
\Hypo{}
\Infer 1[\rax$\dagger$]{\vdash T\tikzmark{add6},T^\perp\tikzmark{add7}}
\Infer 1[\rbot]{\vdash \bot,T\tikzmark{add5},T^\perp\tikzmark{add8}}
\Hypo{}
\Infer 1[\rax$\ddagger$]{\vdash T,T^\perp}
\Infer 1[\rbot]{\vdash \bot,T,T^\perp}
\Infer 1[\scriptsize{$\color{red}{\rmu^k}$}]{{\vdash \bot, T,T^\perp}}
\Infer 2 [\rwith]{\vdash \bot\with\bot, T\tikzmark{add4},T^\perp\tikzmark{add9}}
\Hypo{\vdash S,\orig{a}T\tikzmark{add10}}
\Infer 2[\rcut]{\vdash \bot\with\bot, S,T\tikzmark{add3}}
\Infer 1[\rmu,\rparr]{\vdash S,T\tikzmark{add2}}
\Infer 1[\rnu]{\vdash S,T\tikzmark{add1}
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (b)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (a.north east) .. controls +(20:1.2cm) and +(0:4.5cm) .. (b.east);
\end{tikzpicture}\;}
\end{prooftree} \begin{tikzpicture}[overlay,remember picture,-,line cap=round,line width=0.1cm]
\draw[rounded corners, smooth=2,cyan, opacity=.25] ($(pic cs:add1)+(0cm,.1cm)$) to ($(pic cs:add2)+(-0.1cm,.1cm)$) to($(pic cs:add3)+(0,.1cm)$) to($(pic cs:add4)+(.1cm,-0.1cm)$) to($(pic cs:add5)+(0,-.1cm)$)to($(pic cs:add6)+(-0.1cm,.3cm)$)to($(pic cs:add7)+(-0.1cm,.3cm)$)to($(pic cs:add8)+(-.2cm,.1cm)$)to($(pic cs:add9)+(0,.1cm)$)to($(pic cs:add9)+(1cm,-.1cm)$)to($(pic cs:add10)+(-0.1cm,-.1cm)$)to($(pic cs:add10)+(0,.3cm)$);
\end{tikzpicture}

With $(\pi_k)_{k\geq 0}$ proofs, one faces three situations for cut-elimination:

(i) from $\pi_0$ it is productive and produces a valid proof;

(ii) from $\pi_1$  it is productive and produces an invalid pre-proof;

(iii) from $\pi_k$, for $k\geq 2$ it is not even productive.

Indeed, in these examples, each $\pi_k$ contains exactly one infinite
branch which is supported by a thread on $T$ bouncing on the left-most
axiom and this thread is valid.
Still, this does not ensure productivity nor validity.
For instance, $\pi_1$ reduces to the following pre-proof:

$$  \begin{prooftree}
\Hypo{\orig{a}\vdash S,T}
\Infer 1[\rbot]{\vdash \bot,S,T}
\Hypo{\vdash S,\orig{aa}T}
\Infer 1[\rbot]{\vdash \bot, S,T}
\Infer 2[\rwith]{\vdash \bot\with\bot, S,T}
\Infer 1[\rmu,\rparr]{\vdash S,T
\begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (bb)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (aa.north east) .. controls +(10:2cm) and +(0:4.5cm) .. (bb.east);
\end{tikzpicture}\;}
\Infer 1[\rnu]{          \begin{tikzpicture}[remember picture,overlay]
\node[inner sep=0pt,outer sep=0pt] (b)  {\ensuremath{}};
%\coordinate(R) at (0,0);
\draw [->,>=latex] (a.north east) .. controls +(160:2cm) and +(180:2.5cm) .. (b.east);
\end{tikzpicture}\;\vdash S,T}
\end{prooftree}

which is not valid since any infinite branch which takes only finitely many times the left back-edge is invalid.

To understand the problem, consider the first step of cut-reduction which is a $\rcut/\rwith$
commutation and copies the right-premiss of the cut (ie. the
non-wellfounded part of the proof): the resulting pre-proof contains two
infinite branches now, but only one thread to validate them.
While the left copy can be validated by the original thread, the
right copy does not contain a residual of the original thread. Of course,
one might consider a thread originated in the cut inference, but that
will not suffice to ensure validity, nor productivity, as $\pi_2$ examplifies: its right-most branch does not produce any rule.

§.§.§ Sliced proof system and its cut-reduction

To solve the previous issue, we will make use of slices, originally introduced by Girard in his seminal paper and later used in the analysis of interaction and cut-elimination of linear logic in the setting of Ludics <cit.> or in the design of additive proof-nets <cit.>.

A sliced pre-proof is a pre-proof built on a variant of $\muMALLi$, $\muSMALLi$, where the inference rule $\rwith$ has been replaced by the following two rules:

\Hypo{\vdash A, \Gamma}
\Infer 1[\rwithl]
{\vdash A\with B, \Gamma}
\end{prooftree}
\qquad \begin{prooftree}
\Hypo{\vdash B, \Gamma}
\Infer 1[\rwithr]
{\vdash A\with B, \Gamma}
\end{prooftree}$$

To a $\muMALLi$ sequent (pre-)proof, one can associate a set of slices
by keeping, for each $\rwith$ inference, only one of its premisses and replacing the $\with$ by the corresponding inference in $\rwithl,\rwithr$. More precisely, a slice of $\pi$ is any $\muSMALLi$ derivation obtained from $\pi$ by applying corecursively one of the following two reductions (the other inferences are treated homomorphically):

$$    \scalebox{.9}{
\begin{prooftree}
\Hypo{\pi_1}
\Infer 1{\vdash A_1, \Gamma}
\Hypo{\pi_2}
\Infer 1{\vdash A_2, \Gamma}
\Infer 2[\rwith]{\vdash A_1\with A_2, \Gamma}
\end{prooftree}
\begin{prooftree}
\Hypo{\pi_1}
\Infer 1{\vdash A_1, \Gamma}
\Infer 1[\rwithl]
{\vdash A_1\with A_2, \Gamma}
\end{prooftree}, \begin{prooftree}
\Hypo{\pi_2}
\Infer 1{\vdash A_2, \Gamma}
\Infer 1[\rwithr]
{\vdash A_1\with A_2, \Gamma}
\end{prooftree}

that is:

\scalebox{.8}{$
\Hypo{\pi_1}
\Infer 1{\vdash A_1, \Gamma}
\Hypo{\pi_2}
\Infer 1{\vdash A_2, \Gamma}
\Infer 2[\rwith]{\vdash A_1\with A_2, \Gamma}
\end{prooftree}
\right) =
%\left\{ \begin{prooftree}
%      \Hypo{\pi'_1}
%      \Infer 1{\vdash A_1, \Gamma}
%      \Infer 1[\rwithl]
%             {\vdash A_1\with A_2, \Gamma}
%        \end{prooftree}, \pi'_1\in Sl(\pi_1)
%\bigcup \left\{\begin{prooftree}
%      \Hypo{\pi'_2}
%      \Infer 1{\vdash A_2, \Gamma}
%      \Infer 1[\rwithr]
%             {\vdash A_1\with A_2, \Gamma}
%        \end{prooftree}, \pi'_2\in Sl(\pi_2)
%\right\}        $$
\left\{\begin{prooftree}
\Hypo{\pi'_i}
\Infer 1{\vdash A_i, \Gamma}
\Infer 1[\rwithi]
{\vdash A_1\with A_2, \Gamma}
\end{prooftree},
\begin{array}{c}
\pi'_i\in Sl(\pi_i),\\
\end{array}
\right\}

§.§.§ Cut-reductions for sliced proofs

Cut-reduction rules for slices of $\muSMALLi$ are identical to
those for $\muMALLi$ except for the sliced additives. In this case,
one may have a problematic situation when a $\rwithl$ shall interact
with a $\roplusr$: cut-elimination cannot be performed.
Among the several ways to cope with this problem, we choose here to

introduce a special inference, $\rdai$, a generalized axiom rule
allowing to derive any sequent,
which denotes the fact that a bad interaction occurred.

\begin{prooftree}
\Hypo{}
\Infer 1[$\rdai$]{\vdash \Gamma}
\end{prooftree}

This does not impact the technical development since this serves essentially the purpose of defining those slices which avoid the mismatch.

Considering the $\rdai$ inference, cut-reductions for slices are specified as follows[This reduction is straightforwardly extended to multicuts and some care shall be taken in treating $\rdai$, in particular any cut involving  is reduced to itself as standard in ludics.]:

The sliced additive principal case is reduced as follows,
\Hypo{\pi_i}
\Infer 1{\vdash A_i, \Gamma}
\Infer 1[\rwithi]
{\vdash A_1\with A_2, \Gamma}
\Hypo{\pi'_j}
\Infer 1{\vdash A^\perp_j, \Gamma}
\Infer 1[\roplusj]
{\vdash A^\perp_1\oplus A^\perp_2, \Delta}
\Infer 2 [\rcut]{\vdash \Gamma, \Delta}
\end{prooftree}
$\rightarrow \left\{
\begin{array}{cc}
\begin{prooftree}\Hypo{}\Infer 1[$\rdai$]{\vdash \Gamma,\Delta}\end{prooftree} & \text{if }i\neq j\\
\begin{prooftree}
\Hypo{\pi_i}
\Infer 1{\vdash A_i, \Gamma}
\Hypo{\pi'_i}
\Infer 1{\vdash A^\perp_i, \Delta}
\Infer 2 [\rcut]{\vdash \Gamma, \Delta}
\end{prooftree}  & \text{if }i = j\\
\end{array}
\right.$

if $\{A^\perp_1\with A^\perp_2, {A'}_1\oplus {A'}_2\}\in\dbot$, with $r = (\mathsf{princ}, \{A^\perp_1\with A^\perp_2, {A'}_1\oplus {A'}_2\})$.

\Hypo{\C C}
\Hypo{\pi_i}
\Infer 1
{\vdash A^\perp_i, \Gamma}
\Infer 1[\rwithi]
{\vdash A^\perp_1\with A^\perp_2, \Gamma}
\Hypo{\pi'_j}
\Infer 1{\vdash {A'}_j, \Gamma}
\Infer 1[\roplusj]
{\vdash {A'}_1\oplus {A'}_2, \Delta}
\Infer 3 [{\scriptsize\ensuremath{\mathsf{mcut(\iota, \perp\!\!\!\perp)}}}\xspace]{\vdash \Sigma}
\end{prooftree}

\left\{
\begin{array}{cc}
\begin{prooftree}\Hypo{}\Infer 1[$\rdai$]{\vdash \Sigma}\end{prooftree} & \text{if }i\neq j\\[12pt]
\begin{prooftree}
\Hypo{\C C}
\Hypo{\pi_i}
\Infer 1{\vdash A^\perp_i, \Gamma}
\Hypo{\pi'_i}
\Infer 1{\vdash A'_i, \Delta}
\Infer 3 [{\scriptsize\ensuremath{\mathsf{mcut(\iota, \perp\!\!\!\perp')}}}\xspace]{\vdash \Sigma}
\end{prooftree}  & \text{if }i = j\\