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

\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}