\section{Proofs and further remarks for Sect.~\ref{sect:arithmetic}}
\label{sect:app-arithmetic}

\begin{proof}[Proof of Prop.~\ref{prop:equiv-rules}]
We give only the case for induction, the others being routine.

First, let us assume the induction axiom and derive the rule:
\[
\hspace{-2.5em}
\small
\vlderivation{
\vliq{\cntr}{}{ !\word (t) , !\Gamma, A(\epsilon) \seqar A(t) , ?\Delta }{
\vlin{2\cdot\cut}{}{!\word(t) , !\Gamma,  !\Gamma, A(\epsilon) \seqar A(t) , ?\Delta, ?\Delta }{
\vlhy{
{
\left\{
\vlderivation{
\vlin{\rigrul{!}}{}{ !\Gamma \seqar ! \forall x^{!\word} . ( A(x) \limp A(\succ_i x) ) , ?\Delta }{
\vlin{\rigrul{\forall}}{}{ !\Gamma \seqar  \forall x^{!\word} . ( A(x) \limp A(\succ_i x) ) , ?\Delta }{
\vlin{2\cdot\rigrul{\limp}}{}{ !\Gamma \seqar !\word (a) \limp A(a) \limp A(\succ_i a) , ?\Delta }{\vlhy{ !\word (a) ,!\Gamma , A(a) \seqar A(\succ_i a) , ?\Delta }}
}
}
}
\right\}_{i=0,1}
}
\qquad
{
\vlderivation{
\vliq{\inv{\forall} }{}{ !\word (t), A(\epsilon) ,\{!\forall x^{!\word} . ( A(x) \limp A(\succ_0 x) )\}_{i=0,1} \seqar A(t) }{
\vliq{\inv{\limp}}{}{ A(\epsilon) , \{!\forall x^{!\word} . ( A(x) \limp A(\succ_0 x) )\}_{i=0,1}  \seqar \forall x^{!\word} .A(x) }{
\vlhy{
\seqar 
%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)
\ind
}
}
}
}
}
}
}
}
}
\]
Now we assume the induction rule and derive the axiom,
\[
\vlderivation{
\vlin{3\cdot\rigrul{\limp}}{}{\seqar \ind }{
\vlin{\rigrul{\limp},\rigrul{\forall}}{}{\{ !\forall x^{!\word} . ( A(x) \limp A(\succ_i x) ) \}_{i=0,1} , A(\epsilon) \seqar \forall x^{!\word} . A(x) }{
\vlin{\ind}{}{!\word (t) , \{ !\forall x^{!\word} . ( A(x) \limp A(\succ_i x) ) \}_{i=0,1} \seqar A(b) }{
\vlhy{
\left\{
\vltreeder{\pi_i}{ !\word (a) , \{ !\forall x^{!\word} . ( A(x) \limp A(\succ_i x) ) \}_{i=0,1} , A(a) \seqar A(\succ_i a) }{\quad}{}{\quad }
\right\}_{i=0,1}
}
}
}
}
}
\]
where the proofs $\pi_i$ are obtainable from just logical rules.
\end{proof}

\paragraph*{Formulation of induction with designated premise for base case}
Here is the induction rule when there is 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}
As mentioned, this is not equivalent to the formulation given, due to the linear logic setting. From an axiomatic point of view, it is equivalent to the $\ind$ axiom with $!A(\epsilon)$ in place of $A(\epsilon)$.

%Proof that coherent ESs have a model:
%\begin{proof}[Proof of Prop.~\ref{prop:eq-spec-model}]
%	%\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}

%Proof that guarded quantifiers are compatible with free-cut elimination:
\begin{proof}[Proof of Cor.~\ref{cor:free-cut-elim-guarded-quants}]
	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}