Index: arithmetic.tex
===================================================================
--- arithmetic.tex	(revision 237)
+++ arithmetic.tex	(revision 238)
@@ -8,7 +8,7 @@
 %The formula $A \cimp B$ will be a notation for $\neg A \cor B$.
 %We will also use as shorthand notations:
 %$$ (s=t) = (s\leq t) \cand (t\leq s), \quad (s\neq t) = \neg(s=t).$$ 
-\textit{Atomic formulas} formulas are of the form $(s\leq t)$, for terms $s,t$.
+\textit{Atomic formulas} formulas are of the form $s\leq t$, for terms $s,t$.
  We will assume, without loss of generality, that formulas are in \textit{De Morgan normal form}, that is to say that in formulas negation can only occur on atomic formulas, and that there is not any occurrence of a subformula of the form $\neg \neg A$.
  
  
@@ -20,8 +20,8 @@
 We include a similar set of axioms for direct comparison, although in our setting these are not minimal.
 Indeed, $\#$ can be defined using induction in our setting.
 
-The $\basic$ axioms of bounded arithmetic give the inductive definitions and interrelationships of the various function symbols.
-It also states the fundamental algebraic properties, i.e.\ $(0,\succ{ } )$ is a free algebra, and, for us, it will also give us certain `typing' information for our function symbols based on their $\bc$ specification, with safe inputs ranging over $\safe$ and normal ones over $\normal$.
+The $\basic$ axioms of bounded arithmetic give the inductive definitions and interrelationships of the various function and predicate symbols.
+It also states fundamental algebraic properties, e.g.\ $(0,\succ{ } )$ is a free algebra, and, for us, it will also give us certain `typing' information for our function symbols based on their $\bc$ specification, with safe inputs ranging over $\safe$ and normal ones over $\normal$.
 For instance, we include the following axioms:\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{array}{l}
@@ -107,14 +107,14 @@
 \[
  \dfrac{\proves \forall \vec x^\normal . \exists  y^\safe .  A }{ \proves \forall \vec x^\normal .\exists y^\normal . A}
 \]
-We will write $\arith^i \proves A$ if $A$ is a logical consequence of the axioms of $\arith^i$, in the usual way.
+We will write $\arith^i \proves A$ if $A$ is a logical consequence of the axioms and rules of $\arith^i$, in the usual way.
 \end{definition}
 %\patrick{I think in the definition of  $\arith^i$ we should impose that the formulas considered are \textit{integer positive}, that is to say that the only negative occurrences of atoms $\safe(t)$, $\normal(t)$ are those occurring in $\forall^{\safe}$ and $\forall^{\normal}$.  Indeed I don't think this can be just proved to be a consequence of a kind of 'normal form' of proofs, as we had discussed (see sect 4.4)}
 %
 %\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
 
 \begin{remark}
-Notice that $\rais$ looks similar to the $K$ rule from the calculus for the modal logic $S4$, and indeed we believe there is a way to present these results in such a framework.
+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.
 However, the proof theory of first-order modal logics, in particular free-cut elimination results used for witnessing, is not sufficiently developed to carry out such an exposition.	
 	\end{remark}
 
@@ -125,13 +125,13 @@
 \subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
 %Todo: $+1$,  
 
-We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall ^{\normal} \vec u, \forall ^{\safe} x, \exists^{\safe}! y. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
+We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall \vec u^{\normal} , \forall  x^{\safe}, \exists! y^{\safe}. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
  
-Let us give a few examples for basic functions representable in $\arith^1$:
+Let us give a few examples for basic functions representable in $\arith^1$, wherein proofs of totality are routine:
 \begin{itemize}
-\item Projection $\pi_k^{m,n}$: $\forall^{\normal} u_1, \dots, u_m,  \forall^{\safe} x_{m+1}, \dots, x_{m+n}, \exists^{\safe} y. y=x_k$.
-\item Successor $\succ{}$: $\forall^{\safe} x, \exists^{\safe} y. y=x+1.$. The formulas for the binary successors $\succ{0}$, $\succ{1}$ and the constant functions $\epsilon^k$ are defined in a similar way.
-\item Predecessor $p$:   $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$
+\item Projection $\pi_k^{m,n}$: $\forall u_1^{\normal} , \dots, u_m^{\normal} ,  \forall x_{m+1}^{\safe} , \dots, x^{\safe} _{m+n}, \exists y^{\safe} . y=x_k$.
+%\item Successor $\succ{}$: $\forall x^{\safe} , \exists^{\safe} y. y=x+1.$. The formulas for the binary successors $\succ{0}$, $\succ{1}$ and the constant functions $\epsilon^k$ are defined in a similar way.
+%\item Predecessor $p$:   $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$
 \item Conditional $C$: 
 $$\begin{array}{ll}
 \forall^{\safe} x, y_{\epsilon}, y_0, y_1, \exists^{\safe} y. & ((x=\epsilon)\cand (y=y_{\epsilon})\\
@@ -139,10 +139,9 @@
                                                                                                    & \cor( \exists^{\safe}z.(x=\succ{1}z) \cand (y=y_1)))\
 \end{array}
 $$
-\item Addition:
-$\forall^{\safe} x, y,  \exists^{\safe} z. z=x+y$. 
+%\item Addition:
+%$\forall^{\safe} x, y,  \exists^{\safe} z. z=x+y$. 
 \item Prefix:
-
   This is a predicate that we will need for technical reasons, in the completeness proof. The predicate $\pref(k,x,y)$ holds if the prefix of string $x$
   of length $k$ is $y$. It is defined as:
   $$\begin{array}{ll}
