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

	\item\label{ax:a} $\forall u^\normal. \safe(u) $

	\item\label{ax:h} $\forall u^\normal .\safe(|u|)$

%\patrick{Actually I guess that we could replace the last one by $\forall x^\normal .\safe(|x|)$, as $|x|$ has smaller size as $x$? But I am not sure this would be needed anywhere. }

%\anupam{Need vector $\vec y^\safe$?}

Let us consider some basic examples of theorems of our

	\begin{enumerate}[(i)]

		\item\label{item:i} $\forall x^\safe . 0 \neq \succ{} (x)$

		\item\label{item:ii} $\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) $

		\item\label{item:iii} $\forall u^\normal . (u = 0 \cor \exists y^\safe.  u = \succ{} v  ) $

		\item\label{item:iv} $\forall u^\normal ,x^\safe . u \cdot \succ{} x = u + ux$

	\end{enumerate}

%	\[

%	\begin{array}{l}

%	\forall x^\safe . 0 \neq \succ{} (x) \\

%	\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\

%	%\forall x^\safe . (x = 0 \cor \exists y^\safe.\  x = \succ{} y   )  \\        %% version 1: Anupam

%	%\forall u^\normal . (u = 0 \cor \exists v^\normal.\  u = \succ{} v  )  %%  version 2: Patrick

%	\forall u^\normal . (u = 0 \cor \exists y^\safe.  u = \succ{} v  )  \\        %% version 3: after discussion

%	\forall u^\normal ,x^\safe . u \cdot \succ{} x = u + ux

%	\end{array}

%	\]

%	\todo{Proof: Patrick? The final two should require PIND.}

%	\patrick{Actually statement 4 is nearly trivial from axiom 27 (for which I corrected the sorts). Maybe you meant something else?

%		\anupam{I actually changed those sorts from the submitted version: I really think axiom 27 should be $\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x$, i.e.\ with the recursion on the normal variable. That way we can do induction on it. Statement 4 is meant to state the recursive property for the safe argument, which we can prove by induction on the normal argument, $u$.}

%	

%	For statement 3 I replaced the quantifications $\safe$ by $\normal$, otherwise I don't know how to prove it. But I think we need the stronger statement with $\safe$, so probably we should add it as an additional axiom.}

%\anupam{Rather, I do not know how you would prove the current version: we cannot induct on $\exists v^\normal$ from axiom 27 as I state it. For the previous version I would just do induction on $u$ in $(u = 0 \cor \exists x^\safe.\  u = \succ{} x )$. }

	For \eqref{item:i}, assume  $\succ{} (x)=0$ in order to derive a contradiction. From axiom \ref{axiom1} we deduce $x \leq x$, and so by transitivity (axiom \ref{axiom<=transitivity}) we have $x\leq 0$. So axiom \ref{axiom3} gives us $x=0$, and so $x=\succ{} (x)$. Finally with axiom  \ref{axiom2} we conclude with a contradiction.

	For \eqref{item:ii} assume $\succ{} x= \succ{} y$ and, in view of a contradiction, $x\neq y$. Let us apply axiom \ref{axiom6} and assume we are in the case where $x\leq y$ (the case $y\leq x$ is symmetric). By axiom \ref{axiom4}, using the assumption $x\neq y$ we deduce $\succ{} x \leq y$. So as $\succ{} x = \succ{} y$ we can derive that $\succ{} y \leq y$. So by using axiom \ref{axiom1} we obtain that $\succ{} y = y$, hence axiom \ref{axiom2} gives us a contradiction, so we are done.

	For \eqref{item:iii} we proceed by induction on $u$ on the formula %$A(u)= (u=0) \cup \exists^{\normal} v. u=\succ{} v$.

	$A(u)= (u=0) \cup \exists^{\safe} v. u=\succ{} v$. Note that this formula is in $\Sigma^{\safe}_1$, so we can do induction on it in  $\arith^1$. 

	The formula $A(0)$ obviously holds. Let us assume $A(u)$ and prove $A(\succ{0} u)$ (the case for $A(\succ{1} u)$ will be similar).  By $A(u)$ we deduce that either $u=0$, in which case we also have $\succ{0} u=0$, hence  $A(\succ{0} u)$ also holds, or there is a $y$ such that $u=\succ{} y$. In this latter case we have $\succ{0} u=2\cdot(\succ{} y)=2 v +2$ (by axiom \ref{axiom29}), hence have $\succ{0} u=\succ{} (\succ{} (2\cdot y))$, and so $A(\succ{0} u)$ holds.

	By induction we conclude that $\forall^{\normal} u. A(u)$ holds.

	 For \eqref{item:iv} let $u$ be in $\normal$ and $x$ in $\safe$, and try to prove $u\succ{} x=u+ux$. We have $\succ{} x=x+1$ by axioms \ref{axiom23} and \ref{axiom22} , so $u\succ{} x= u(x+1)$, so from axiom \ref{axiom29} we deduce $ u\succ{} x= u(x+1)=ux+u$, and by axiom \ref{axiom21} we conclude that $ u\succ{} x=u+ux$.	

Strictly speaking, we must alter some of the sequent rules a little to arrive at this normal form. For instance the $\pind$ rule would have $\normal(\vec u)$ in its lower sequent rather than $\normal (t(\vec u))$:

\[

\small

\vliinf{}{}{ \normal(\vec u) , \safe (\vec x) , \Gamma , A(0) \seqar A(t(\vec u)), \Delta }{ \normal(u), \normal (\vec u) , \safe (\vec x) , \Gamma, A(u) \seqar A(\succ{0} u) , \Delta }{ \normal(u) ,, \normal(\vec u ) , \safe (\vec x) , \Gamma, A(u) \seqar A(\succ{1} u) , \Delta  }

\] 

Notice that $\normal(t(\vec u))$ is a consequence of $\normal (\vec u)$ already in $\basic$, due to the axioms \eqref{ax:a}-\eqref{ax:h}.

That the variables of $t$ can be assumed to occur already in the premisses is due to weakening.

Indeed, the proof of this result relies on a heavy use of the structural rules, contraction and weakening, to ensure that we always have a complete and compatible sorting of variables on the LHS of a sequent. This is similar to what is done in \cite{OstrinWainer05} where they use a $G3$ style calculus to manage such structural manipulations.

As we mentioned, the fact that only $\Sigma^\safe_i$ formulae occur is due to the free-cut elimination result for first-order calculi \cite{Takeuti87,Cook:2010:LFP:1734064}, which gives a form of proof where every $\cut$ step has one of its cut formulae `immediately' below a non-logical step. Again, we have to adapt the $\rais$ rule a little to achieve our result, due to the fact that it has a $\exists x^\normal$ in its lower sequent. For this we consider a merge of $\rais$ and $\cut$, which allows us to directly cut the upper sequent of $\rais$ against a sequent of the form $\normal(u), A(u), \Gamma \seqar \Delta$:

\[

\vliinf{\rais\cut}{}{\normal (\vec u) , \Gamma \seqar \Delta}{\normal (\vec u) \seqar \exists x^\safe . A(x)}{\normal (u) , A(u) , \Gamma \seqar \Delta}

\]