Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\section{A variant of arithmetic in linear logic}

\label{sect:arithmetic}

For the remainder of this article we will consider an implementation of arithmetic in the sequent calculus based on the theory $\bharith$ of Bellantoni and Hofmann in \cite{BelHof:02}. The axioms that we present are obtained from $\bharith$ by using linear logic connectives in place of their classical analogues, calibrating the use of additives or multiplicatives in order to be compatible with the completeness and witnessing arguments that we present in Sects.~\ref{sect:bc-convergence} and \ref{sect:wfm}. We also make use of free variables and the structural delimiters of the sequent calculus to control the logical complexity of nonlogical rules.

We will work in the \emph{affine} variant of linear logic, which validates weakening: $(A \land B )\limp A$. There are many reasons for this; essentially it does not have much effect on complexity while also creating a more robust proof theory. For example it induces the equivalence:

\(

!(A\land B) \equiv (!A \land !B)

\).\footnote{Notice that the right-left direction is already valid in usual linear logic, but the left-right direction requires weakening.}

%We define a variant of arithmetic inspired by Bellantoni and Hofmann's $A^1_2$. We describe later some connections to bounded arithmetic.

\newcommand{\lang}{\mathcal L}

\subsection{Axiomatisation and an equivalent rule system}

%\begin{definition}

%[Language]

We consider the language $\lang$ consisting of the constant symbol $\epsilon$, unary function symbols $\succ_0 , \succ_1$ and the predicate symbol  $\word$, together with function symbols $f,g,h$ etc.

%\end{definition}

$\lang$-structures are typically extensions of $\Word = \{ 0,1 \}^*$, in which $\epsilon, \succ_0, \succ_1$ are intended to have their usual interpretations. The $\word$ predicate is intended to indicate those elements of the model that are binary words (in the same way as Peano's $N$ predicate indicates those elements that are natural numbers).

As an abbreviation, we write $\word (\vec t)$ for $\bigotimes^{|\vec t|}_{i=1} \word(t_i)$.

\begin{remark}

[Interpretation of natural numbers]

Notice that the set $\Nat^+$ of positive integers is $\lang$-isomorphic to $\Word$ under the interpretation $\{ \epsilon \mapsto 1 , \succ_0 (x) \mapsto 2x , \succ_1 (x) \mapsto 2x+1 \}$, so we could equally consider what follows as theories over $\Nat^+$.

\end{remark}

The `basic' axioms are essentially the axioms of Robinson arithmetic (or Peano Arithmetic without induction) without axioms for addition and multiplication.

%\footnote{They are also similar to the `generative' axioms of Leivant's intrinsic theories [cite] for this signature.}

Let us write $\forall x^\word . A$ for $\forall x . ( \word(x) \limp A )$ and $\exists x^\word . A$ for $\exists x . ( \word(x) \land A )$. We use the abbreviations $\forall x^{!\word}$ and $\exists x^{!\word}$ similarly.

\newcommand{\wordcntr}{\word_\cntr}

\newcommand{\natcntr}{\nat_\cntr}

\newcommand{\geneps}{\word_{\epsilon}}

\newcommand{\genzer}{\word_{0}}

\newcommand{\genone}{\word_{1}}

\newcommand{\sepeps}{\epsilon}

\newcommand{\sepzer}{\succ_{0}}

\newcommand{\sepone}{\succ_{1}}

\newcommand{\inj}{\mathit{inj}}

\newcommand{\surj}{\mathit{surj}}

\newcommand{\basic}{\mathit{BASIC}}

\begin{definition}

[Basic axioms]

The theory $\basic$ consists of the following axioms:

\[

\small

\begin{array}{rl}

%\wk & (A \land B )\limp A \\

%\geneps

& \word(\epsilon) \\

%\genzer

& \forall x^\word . \word(\succ_0 x) \\

%\genone

& \forall x^\word . \word(\succ_1 x) \\

%\sepeps & \forall x^\word . (\epsilon \neq \succ_0 x \land \epsilon \neq \succ_1 x) \\

%\sepzer & \forall x^\word , y^\word. ( \succ_0 x = \succ_0 y \limp x=y ) \\

%\sepone & \forall x^\word , y^\word. ( \succ_1 x = \succ_1 y \limp x=y ) \\

%\inj & \forall x^\word . \succ_0 x \neq \succ_1 x \\

%\surj & \forall x^\word . (x = \epsilon \laor \exists y^\word . x = \succ_0 y \laor \exists y^\word . x = \succ_1 y ) \\

%\noalign{\smallskip}

%\wordcntr & \forall x^\word . (\word(x) \land \word(x))

\end{array}

%\quad

\begin{array}{rl}

%\wk & (A \land B )\limp A \\

%\geneps & \word(\epsilon) \\

%\genzer & \forall x^\word . \word(\succ_0 x) \\

%\genone & \forall x^\word . \word(\succ_1 x) \\

%\sepeps

& \forall x^\word . (\epsilon \neq \succ_0 x \land \epsilon \neq \succ_1 x) \\

%\sepzer

& \forall x^\word , y^\word. ( \succ_0 x = \succ_0 y \limp x=y ) \\

%\sepone

& \forall x^\word , y^\word. ( \succ_1 x = \succ_1 y \limp x=y ) \\

%\inj & \forall x^\word . \succ_0 x \neq \succ_1 x \\

%\surj & \forall x^\word . (x = \epsilon \laor \exists y^\word . x = \succ_0 y \laor \exists y^\word . x = \succ_1 y ) \\

%\noalign{\smallskip}

%\wordcntr & \forall x^\word . (\word(x) \land \word(x))

\end{array}

%\quad

\begin{array}{rl}

%\wk & (A \land B )\limp A \\

%\geneps & \word(\epsilon) \\

%\genzer & \forall x^\word . \word(\succ_0 x) \\

%\genone & \forall x^\word . \word(\succ_1 x) \\

%\sepeps & \forall x^\word . (\epsilon \neq \succ_0 x \land \epsilon \neq \succ_1 x) \\

%\sepzer & \forall x^\word , y^\word. ( \succ_0 x = \succ_0 y \limp x=y ) \\

%\sepone & \forall x^\word , y^\word. ( \succ_1 x = \succ_1 y \limp x=y ) \\

%\inj

& \forall x^\word . \succ_0 x \neq \succ_1 x \\

%\surj

& \forall x^\word . (x = \epsilon \laor \exists y^\word . x = \succ_0 y \laor \exists y^\word . x = \succ_1 y ) \\

%\noalign{\smallskip}

%\wordcntr

& \forall x^\word . (\word(x) \land \word(x))

\end{array}

\]

\end{definition}

These axioms insist that, in any model, the set induced by $\word (x)$ has the free algebra $\Word$ as an initial segment.

Importantly, there is also a form of contraction for the $\word$ predicate.

We will consider theories over $\basic$ extended by induction schemata:

\begin{definition}

[Induction]

The \emph{(polynomial) induction} axiom schema, $\ind$, consists of the following axioms,

\[

%\begin{array}{rl}

%& A(\epsilon) \\

%\limp & !(\forall x^{!\word} . ( A(x) \limp A(\succ_0 x) ) ) \\

%\limp & !(\forall x^{!\word} . ( A(x) \limp A(\succ_1 x) ) ) \\

%\limp & \forall x^{!\word} . A(x)

%\end{array}

A(\epsilon)

\limp !(\forall x^{!\word} . ( A(x) \limp A(\succ_0 x) ) )

\limp  !(\forall x^{!\word} . ( A(x) \limp A(\succ_1 x) ) )

\limp  \forall x^{!\word} . A(x)

\]

for each formula $A(x)$.

For a class $\Xi$ of formulae, $\cax{\Xi}{\ind}$ denotes the set of induction axioms when $A(x) \in \Xi$.

We write $I\Xi$ to denote the theory consisting of $\basic$ and $\cax{\Xi}{\ind}$.

\end{definition}

We use the terminology `polynomial induction' to maintain consistency with the bounded arithmetic literature, e.g.\ in \cite{Buss86book}, where it is distinguished from induction on the \emph{value} of a string (construed as a natural number). The two forms have different computational behaviour, specifically with regards to complexity, but we will restrict attention to $\ind$ throughout this work, and thus may simply refer to it as `induction'.

%\anupam{in fact just give general case for a universal closed formula. Then remark about invertibility of negation giving purely positive initial steps. These occur in section 6 so no need to write them out here.}

\begin{proposition}

[Equivalent rules]

\label{prop:equiv-rules}

$\basic$ is equivalent to the following set of rules,

\[

\small

\begin{array}{l}

\begin{array}{cccc}

\vlinf{\geneps}{}{\seqar \word (\epsilon)}{}&

\vlinf{\genzer}{}{\word(t) \seqar \word(\succ_0 t)}{}&

\vlinf{\sepeps_0}{}{ \word (t)   \seqar \epsilon \neq \succ_0 t}{} &

\vlinf{\sepzer}{}{\word (s) , \word (t)  , \succ_0 s = \succ_0 t\seqar s = t }{}\\

\vlinf{\inj}{}{\word(t) \seqar\succ_0 t \neq \succ_1 t}{}&

\vlinf{\genone}{}{\word(t) \seqar \word(\succ_1 t)}{}&

\vlinf{\sepeps_1}{}{ \word (t)   \seqar \epsilon \neq \succ_1 t }{}&

\vlinf{\sepone}{}{\word (s) , \word (t)  , \succ_1 s = \succ_1 t\seqar s = t }{}

\end{array}

\\

\vlinf{\surj}{}{\word (t) \seqar t = \epsilon \laor \exists y^\word . t = \succ_0 y \laor \exists y^\word . t = \succ_1 y }{}

\qquad

\vlinf{\wordcntr}{}{\word(t) \seqar \word(t) \land \word(t) }{}

\end{array}

\]

%\[

%\vlinf{}{}{\seqar \word (\epsilon)}{}

%\quad

%\vlinf{}{}{\word(t) \seqar \word(\succ_0 t)}{}

%\quad

%\vlinf{}{}{\word(t) \seqar \word(\succ_1 t)}{}

%\qquad \qquad

%\vlinf{}{}{\word(t) \seqar \word(t) \land \word(t) }{}

%\]

%\[

%\vlinf{}{}{ \word (t)  , \epsilon = \succ_0 t \seqar }{}

%\quad

%\vlinf{}{}{ \word (t)  , \epsilon = \succ_1 t \seqar }{}

%\quad

%\vlinf{}{}{\word (s) , \word (t)  , \succ_0 s = \succ_0 t\seqar s = t }{}

%\quad

%\vlinf{}{}{\word (s) , \word (t)  , \succ_1 s = \succ_1 t\seqar s = t }{}

%\]

%\[

%\vlinf{}{}{\word(t), \succ_0 t = \succ_1 t \seqar}{}

%\quad

%\vlinf{}{}{\word (t) \seqar t = \epsilon \laor \exists y^\word . t = \succ_0 y \laor \exists y^\word . t = \succ_1 y }{}

%\]

%\vspace{1em}

and $\ind$ is equivalent to,

\begin{equation}

\label{eqn:ind-rule}

\small

\vliinf{\ind}{}{ !\word(t) , !\Gamma , A(\epsilon) \seqar A(t), ?\Delta }{ !\word(a) , !\Gamma, A(a) \seqar A(\succ_0 a) , ?\Delta }{ !\word(a) , !\Gamma, A(a) \seqar A(\succ_1 a) , ?\Delta  }

\end{equation}

where, in all cases, $t$ varies over arbitrary terms and the eigenvariable $a$ does not occur in the lower sequent of the $\ind$ rule.

\end{proposition}

Note, in particular, that since this system of rules is closed under substitution of terms for free variables, free-cut elimination, Thm.~\ref{thm:free-cut-elim}, applies.

When converting from a $\ind$ axiom instance to a rule instance (or vice-versa) the induction formula remains the same. For this reason when we consider theories that impose logical restrictions on induction we can use either interchangeably.

\begin{remark}

%\anupam{Mention that two induction rules are not the same. This is crucial in, e.g.\ the completeness section for the case of PRN.}

Usually the induction axiom is also equivalent to a formulation with a designated premise for the base case:

\begin{equation}

\label{eqn:ind-rul-base-prem}

\vliiinf{}{}{ !\word(t) , !\Gamma  \seqar A(t), ?\Delta }{!\Gamma \seqar A(\epsilon)}{ !\word(a) , !\Gamma, A(a) \seqar A(\succ_0 a) , ?\Delta }{ !\word(a) , !\Gamma, A(a) \seqar A(\succ_1 a) , ?\Delta  }

\end{equation}

However,

%but

this is not true in the linear logic setting since the proof that \eqref{eqn:ind-rul-base-prem} simulates \eqref{eqn:ind-rule} above relies on contraction on the formula $A(\epsilon)$, which is not in general available. Therefore \eqref{eqn:ind-rul-base-prem} is somewhat weaker than \eqref{eqn:ind-rule}, and is in fact equivalent to a version of the induction axiom with $!A(\epsilon)$ in place of $A(\epsilon)$. This distinction turns out to be crucial in Sect.~\ref{sect:bc-convergence}, namely when proving the convergence of functions defined by predicative recursion on notation.

\end{remark}

%

%\subsection{Equivalent rule systems}

%Instead of weakening and induction axioms, we consider the following rules, which are provably equivalent:

%

%\[

%\vlinf{\lefrul{\wk}}{}{\Gamma, A \seqar \Delta}{\Gamma \seqar \Delta}

%\quad

%\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta}

%\quad

%\vliinf{\pind}{}{ !N(t) , !\Gamma , A(\epsilon) \seqar A(t), ?\Delta }{ !N(a) , !\Gamma, A(a) \seqar A(\succ_0 a) , ?\Delta }{ !N(a) , !\Gamma, A(a) \seqar A(\succ_0 a) , ?\Delta  }

%\]

%

%\todo{provable equivalence, if necessary.}

%

%The inclusion of the first two rules places us in an \emph{affine} setting, whereas the induction rule allows better proof theoretic manipulation.

%

%Finally, for each universally quantified axiom, we consider instead the schema of initial rules with unbound terms in place of universally quantified variables, again for proof theoretic reasons:

%\[

%\vlinf{\natcntr}{}{\nat(t) \seqar \nat(t) \land \nat(t) }{}

%\quad

%\vlinf{\nat_\epsilon}{}{\seqar \nat (\epsilon)}{}

%\quad

%\vlinf{\nat_0}{}{\nat(t) \seqar \nat(\succ_0 t)}{}

%\quad

%\vlinf{\nat_1}{}{\nat(t) \seqar \nat(\succ_1 t)}{}

%\]

%\[

%\vlinf{\epsilon^0}{}{ \nat (t)  , \epsilon = \succ_0 t \seqar }{}

%\quad

%\vlinf{\epsilon^1}{}{ \nat (t)  , \epsilon = \succ_1 t \seqar }{}

%\quad

%\vlinf{\succ_0}{}{\nat (s) , \nat (t)  , \succ_0 s = \succ_0 t\seqar s = t }{}

%\quad

%\vlinf{\succ_1}{}{\nat (s) , \nat (t)  , \succ_1 s = \succ_1 t\seqar s = t }{}

%\]

%\[

%\vlinf{\inj}{}{\nat(t), \succ_0 t = \succ_1 t \seqar}{}

%\quad

%\vlinf{\surj}{}{\nat (t) \seqar t = \epsilon , \exists y^\nat . t = \succ_0 y , \exists y^\nat . t = \succ_1 y }{}

%\]

%%in place of their corresponding axioms.

%

%%\todo{in existential above, is there a prenexing problem?}

%

%

%\anupam{

%NEW INDUCTION STEP:

%\[

%\vliiinf{\pind}{}{!\Gamma, !\nat(t) , \nat (\vec x) \seqar A(t, \vec x) }{!\Gamma , \nat (\vec x) \seqar A(\epsilon, \vec x) }{ !\Gamma, !\nat (a) , \nat (\vec x) , A(a, \vec x) \seqar A(\succ_i a, \vec x) }{!\Gamma, !\nat (a) , \nat (\vec x) , A(a, \vec x) \seqar A(\succ_i a, \vec x)}

%\]

%

%Need to examine strength of this: somewhat weaker since needs actual premiss for base case (only significant because of linear logic), but somewhat stronger because of use of $\nat(\vec x)$ on the left in context.

%}

\subsection{Provably convergent functions}

%

%\anupam{Herbrand-G\"odel equational programs from Kle52, cited in Lei94b.}

%

%\anupam{`coherent' programs, defined by Leivant. = consistent so has a model.}

As in the work of Bellantoni and Hofmann \cite{BelHof:02} and Leivant before \cite{Leivant94:found-delin-ptime}, our model of computation is that of Herbrand-G\"odel style \emph{equational specifications}. These are expressive enough to define every partial recursive function, which is the reason why we also need the $\word$ predicate to have a meaningful notion of `provably convergent function'.

\begin{definition}

	[Equational specifications and convergence]

	An \emph{equational specification} (ES) is a set of equations between terms. We say that an ES is \emph{coherent} if the equality between any two distinct ground terms cannot be proved by equational logic.

%	\footnote{This is the quantifier-free fragment of first-order logic with equality and no other predicate symbols.}

	The \emph{convergence statement} $\conv (f , \eqspec)$ for an equational specification $\eqspec$ and a function symbol $f$ (that occurs in $\eqspec$) is the following formula:

	\[

	\bigotimes_{A \in \eqspec} ! \forall \vec x . A

	\ \limp \

	\forall \vec x^{! \word} .  \word (f (\vec x) )

	\]

	\end{definition}

The notion of coherence appeared in \cite{Leivant94:found-delin-ptime} and it is important to prevent a convergence statement from being a vacuous implication. In this work we will typically consider only coherent ESs, relying on the following result which is also essentially in \cite{Leivant94:found-delin-ptime}:

\begin{proposition}

	\label{prop:eq-spec-model}

%	For every equational specification $\eqspec$, its universal closure has a model.

The universal closure of a coherent ES $\eqspec$ has a model satisfying $\basic + \ind$.

\end{proposition}

%\begin{proof}

%%\todo{ take $\Word \cup \{\bot\}$ or use completeness? Omit if no time. }

%Consider the standard model $\Word $ extended by an element $\infty$ with $\succ_0 \infty = \succ_1 \infty = \infty$. Setting $\word = \Word$ means this model satisfies $\basic$. Now, for each function symbol $f$, define $f(\sigma) = \tau$ for every $\sigma, \tau \in \Word$ for which this equation is forced by $\eqspec$. Otherwise define $f(\sigma) = f(\infty) = \infty$.

%\todo{replace with argument using completeness.}

%\end{proof}

	One issue is that a convergence statement contains universal quantifiers, which is problematic for the extraction of functions by the witness function method later on.

%	\footnote{Intuitively universal quantifiers can be interpreted by type 1 functions. From here, in an intuitionistic setting, a $\forall$-right step can be directly realised, but in the classical setting the presence of side-formulae on the right can cause issues for constructivity.}

	We avoid this problem by appealing to the deduction theorem and further invertibility arguments:

	Let us write $\closure{\eqspec}$ for the closure of a specification $\eqspec$ under substitution of terms for free variables.

	\begin{lemma}

		\label{lemma:spec-norm-form}

	A system $\system$ proves $\conv (f , \eqspec)$ if and only if $\system \cup \closure{\eqspec}$ proves $!\word (\vec a) \seqar \word ( f (\vec a) )$.

	\end{lemma}

	\begin{proof}[Proof sketch]

		By deduction, Thm.~\ref{thm:deduction}, and invertibility arguments.

	\end{proof}

	Notice that the initial rules from $ \closure{\eqspec}$ are also closed under term substitution, and so compatible with free-cut elimination, and that $\closure{\eqspec}$ and $\word (\vec a) \seqar \word ( f (\vec a) )$ are free of negation and universal quantifiers.

\subsection{$\word$-guarded quantifiers, rules and cut-reduction cases}

We consider a quantifier hierarchy here analogous to the arithmetical hierarchy, where each class is closed under positive multiplicative operations. In the scope of this work we are only concerned with the first level:

%We now introduce a quantifier hierarchy of formulae so we can identify the theories that we will be concerned with for the remainder of this article.

%

%

\begin{definition}

%[Quantifier hierarchy]

	We define $\sigzer $ as the class of multiplicative formulae that are free of quantifiers where $\word$ occurs positively.\footnote{Since our proof system is in De Morgan normal form, this is equivalent to saying that there is no occurrence of $\word^\bot$.}

	The class $\sigone$ is the closure of $\sigzer$ by $\exists$, $\lor$ and $\land$.

%	For $i> 0$ we define $\Sigma^\word_i$ and $\Pi^\word_i$ as follows:

%	\begin{itemize}

%		\item If $A \in \Sigma^\word_{i-1} \cup \Pi^\word_{i-1}$ then $A \in \Sigma^\word_i$ and $A \in \Pi^\word_i$.

%		\item If $A \in \Sigma^\word_i$ then $\exists x^\word . A \in \Sigma^\word_i$.

%		\item If $A \in \Pi^\word_i$ then $\forall x^\word . A \in \Pi^\word_i$.

%		\item If $A,B \in \Sigma^\word_i$ then $A \lor B$ and $A\land B \in \Sigma^\word_i$.

%		\item If $A,B \in \Pi^\word_i$ then $A \lor B$ and $A\land B \in \Pi^\word_i$.

%	\end{itemize}

%	We add $+$ in superscript to a class to restrict it to formulae where $\word$ occurs in only positive context.

\end{definition}

For the remainder of this article we mainly work with the theory $\arith$, i.e.\ $\basic + \cax{\sigone}{\ind}$.

%\vspace{1em}

It will be useful for us to work with proofs using the `guarded' quantifiers $\forall x^\word$ and $\exists x^\word$ in place of their unguarded counterparts, in particular to carry out the argument in Sect.~\ref{sect:wfm}.

%To this end we introduce rules for these guarded quantifiers and show that they are compatible with free-cut elimination.

%

%For the quantifiers $\exists x^N $ and $\forall x^N$ we introduce the following rules, which are compatible with free-cut elimination:

%For the quantifiers $\exists x^\word $ and $\forall x^\word$ we

Therefore we define the following rules, which are already derivable:

\[

%\begin{array}{cc}

%\vlinf{}{}{\Gamma \seqar \Delta, \forall x^\word . A(x)}{\Gamma, \word(a) \seqar \Delta , A(a)}

%\quad & \quad

%\vlinf{}{}{\Gamma, \word(t),\forall x^\word A(x) \seqar \Delta}{\Gamma,  A(t) \seqar \Delta}

%\\

%\noalign{\bigskip}

%\vlinf{}{}{\Gamma , \exists x^\word A(x) \seqar \Delta}{\Gamma, \word(a), A(a) \seqar \Delta}

%\quad &\quad

%\vlinf{}{}{\Gamma, \word(t) \seqar \Delta , \exists x^\word . A(x)}{\Gamma  \seqar \Delta, A(t)}

%\end{array}

\vlinf{}{}{\Gamma \seqar \Delta, \forall x^\word . A(x)}{\Gamma, \word(a) \seqar \Delta , A(a)}

\quad

\vlinf{}{}{\Gamma, \word(t),\forall x^\word A(x) \seqar \Delta}{\Gamma,  A(t) \seqar \Delta}

\quad

\vlinf{}{}{\Gamma , \exists x^\word A(x) \seqar \Delta}{\Gamma, \word(a), A(a) \seqar \Delta}

\quad

\vlinf{}{}{\Gamma, \word(t) \seqar \Delta , \exists x^\word . A(x)}{\Gamma  \seqar \Delta, A(t)}

\]

%\begin{proposition}

%	Any principal cut between the quantifier rules above and a logical step is reducible.

%	\end{proposition}

We now show that these rules are compatible with free-cut elimination.

\begin{proposition}\label{prop:logicalstepguardedquantifer}

	Any cut between the principal formula of a quantifier rule above and the principal formula of  a logical step is reducible.

	\end{proposition}

\begin{proof}

 For a cut on $\forall x^\word . A(x)$, the reduction is obtained by performing successively the two reduction steps for the $\forall$ and $\limp$ connectives. The case of $\exists x^\word A(x)$ is similar.

\end{proof}

		\begin{corollary}

		[Free-cut elimination for guarded quantifiers]

		\label{cor:free-cut-elim-guarded-quants}

		  Given a system  $\system$, any  $\system$-proof $\pi$ using $\exists x^\word $ and $\forall x^\word$  rules can be transformed into free-cut free form.

\end{corollary}

%\begin{proof}

%  First translate the proof $\pi$ into the proof $\pi_0$ where all guarded quantifiers rules have been replaced by their derivation, and say that two rule instances in $\pi_0$ are \textit{siblings} if they come from the same derivation of a guarded quantifier rule. So in $\pi_0$ any two sibling rules are consecutive. Now observe that in the free-cut elimination procedure:

%  \begin{itemize}

%  \item when we do a commutation step of a cut with a $\forall$ (resp. $\exists$ rule) that has a sibling, we can follow it by another commutation of cut with its sibling,

%  \item when we do a logical cut-elimination step on a $\forall$ (resp. $\exists$ rule) that has a sibling, we can follow it by a logical cut-elimination step on its sibling, as illustrated by Prop. \ref{prop:logicalstepguardedquantifer}.

%  \end{itemize}

%  In this way sibling rules remain consecutive in the proof-tree throughout the reduction, and the procedure transforms the proof into one with only anchored cuts.

%\end{proof}

As a consequence of this Corollary observe that any $I\Sigma^{\word^+}_{1}$-proof can be transformed into a proof which is free-cut free and whose formulas contain only $\exists x^\word$ quantifiers.