Index: arithmetic.tex
===================================================================
--- arithmetic.tex	(revision 266)
+++ arithmetic.tex	(revision 267)
@@ -26,14 +26,14 @@
 
 Namely, in addition to usual axioms, our $\basic$ includes the following:\footnote{Later some of these will be redundant, for instance $\safe (u \times x) $ and $\safe (u \smsh v)$ are consequences of $\Sigma^\safe_i$-$\pind$, but $\safe (x + y)$ is not since both inputs are safe and so we cannot induct.}
 \begin{enumerate}[(a)]
-	\item $\forall u^\normal. \safe(u) $
+	\item\label{ax:a} $\forall u^\normal. \safe(u) $
 	\item $\safe (0) $
 	\item $\forall x^\safe . \safe (\succ{} x) $
 	\item $\forall u^\safe .\safe(\hlf{u})$
 	\item $\forall x^\safe, y^\safe . \safe(x+y)$
 	\item $\forall u^\normal, x^\safe . \safe(u\times x) $
 	\item $\forall u^\normal , v^\normal . \safe (u \smsh v)$
-	\item $\forall u^\normal .\safe(|u|)$
+	\item\label{ax:h} $\forall u^\normal .\safe(|u|)$
 \end{enumerate}
 %\[
 %\begin{array}{l}
@@ -50,7 +50,7 @@
 %\forall u^\normal .\safe(|x|)
 %\end{array}
 %\]
-\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. }
+%\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. }
 
 Notice in particular that we have $\normal \subseteq \safe$.
 %
@@ -211,7 +211,7 @@
 %
 %\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
 
-\anupam{Need vector $\vec y^\safe$?}
+%\anupam{Need vector $\vec y^\safe$?}
 
 \begin{remark}
 Notice that $\rais$ looks similar to the $K$ rule from the calculus for the modal logic $S4$ (which subsumes necessitation), and indeed we believe there is a way to present these results in such a framework.
@@ -219,40 +219,45 @@
 	\end{remark}
 
 
+Let us consider some basic examples of theorems of our
 \begin{example}
 	[Some basic theorems]
 	We give proofs of the following, that are sometimes included as basic axioms, in $\arith^1$:
-	\[
-	\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.}
+	\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 )$. }
+%	\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 )$. }
 	\end{example}
 \begin{proof}
-\begin{itemize}
- \item For the first statement, 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.
- \item For statement 2 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.
- \item For statement 3 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.
-\item Statement 4:
-%For statement 4 we just use axiom  \ref{axiom27} followed by the $+$ commutativity axiom \ref{axiom21}.
- 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$.
-\end{itemize}
+	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$.	
 \end{proof}
 It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:
 \begin{proposition}
@@ -485,10 +490,19 @@
 	where $\Gamma \seqar \Delta$ contains only $\Sigma^\safe_i$ formulae for which the sorting $(\vec u ;\vec x)$ is compatible.
 \end{theorem}
 
-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))$. The latter is a consequence of the former already in $\basic$.
-The proof of this result also 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.
+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$.
+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}
+\]
 
 Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers \cite{Buss86book}, although we use ones that satisfy the aforementioned constraints. For instance, we include the following rules, from which the remaining ones are similar:
 \[
