Index: arithmetic.tex
===================================================================
--- arithmetic.tex	(revision 226)
+++ arithmetic.tex	(revision 227)
@@ -10,7 +10,10 @@
 %$$ (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$.
  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$.
- We write $\exists x^{N_i} . A$ or $\forall x^{N_i} . A$ for $\exists x . (N_i (x) \cand A)$ and $\forall x . (N_i (x) \cimp A)$ respectively.
+ 
+ 
+ We write $\exists x^{N_i} . A$ or $\forall x^{N_i} . A$ for $\exists x . (N_i (x) \cand A)$ and $\forall x . (N_i (x) \cimp A)$ respectively. We refer to these as \emph{safe} quantifiers.
+ We also write $\exists x^\normal \leq |t| . A$ for $\exists x^\normal . ( x \leq |t| \cand A )$ and $\forall x^\normal \leq |t|. A $ for $\forall x^\normal. (x \leq |t| \cimp A )$. We refer to these as \emph{sharply bounded} quantifiers, as in bounded arithmetic.
 
 
 The theories we introduce are directly inspired from bounded arithmetic, namely the theories $S^i_2$.
@@ -19,96 +22,112 @@
 
 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$.
-\begin{definition}
-	[Basic theory]
-	The theory $\basic$ consists of the axioms from Appendix \ref{appendix:arithmetic}.
-	\end{definition}
+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}
+\forall u^\normal. \safe(u) \\
+\safe (0) \\
+\forall x^\safe . \safe (\succ{} x) \\
+\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   )  
+\end{array}
+\qquad
+\begin{array}{l}
+\forall x^\safe, y^\safe . \safe(x+y)\\
+\forall u^\normal, x^\safe . \safe(u\times x) \\
+\forall u^\normal , v^\normal . \safe (u \smsh v)\\
+\forall u^\safe .\safe(\hlf{u})\\
+\forall u^\normal .\safe(|x|)
+\end{array}
+\]
+Notice that we have $\normal \subseteq \safe$.
+A full list of our $\basic$ axioms can be found in Appendix \ref{appendix:arithmetic}.
 
+%\begin{definition}
+%	[Basic theory]
+%	The theory $\basic$ consists of the axioms from Appendix \ref{appendix:arithmetic}.
+%	\end{definition}
 
-Notation: if $\vec t=t_0,\dots, t_k$, we will denote as $\safe(\vec t)$ the sequence of formulas $\safe(t_0),\dots, \safe(t_k)$. Similarly for $\normal(\vec t)$.
+
+%Notation: if $\vec t=t_0,\dots, t_k$, we will denote as $\safe(\vec t)$ the sequence of formulas $\safe(t_0),\dots, \safe(t_k)$. Similarly for $\normal(\vec t)$.
   
-\begin{definition}
-[Derived functions and notations]
-We write $1,2,3,\dots$ for the terms $\succ{} 0, \succ{} \succ{} 0, \succ{} \succ{} \succ{} 0 \dots$, and frequently omit the $\times$ symbol.
-We define the functions $\succ 0 x , \succ 1 x$ as $2 x$ and $2x +1$ respectively.
+%\begin{definition}
+%[Derived functions and notations]
+%We write $1,2,3,\dots$ for the terms $\succ{} 0, \succ{} \succ{} 0, \succ{} \succ{} \succ{} 0 \dots$, and frequently omit the $\times$ symbol.
+%We define the functions $\succ 0 x , \succ 1 x$ as $2 x$ and $2x +1$ respectively.
+%
+%Need $bit$, $\beta$ , $\pair{}{}{}$.
+%\end{definition}
+%
+%(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers)
+%
+%Use base theory + sharply bounded quantifiers.
 
-Need $bit$, $\beta$ , $\pair{}{}{}$.
-\end{definition}
 
-(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers)
-
-Use base theory + sharply bounded quantifiers.
-
-
 \begin{definition}
 [Quantifier hierarchy]
-$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded.
+$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded and where $\safe , \normal$ do not occur free.
 We define $\Sigma^\safe_{i+1}$ as the closure of $\Pi^\safe_i $ under $\cor, \cand $, safe existentials and sharply bounded quantifiers.
 We define $\Pi^\safe_{i+1}$ as the closure of $\Sigma^\safe_i $ under $\cor, \cand $, safe universals and sharply bounded quantifiers.
 \end{definition}
 
 
-\anupam{Collection principles for prenexing? Otherwise need to add closure under sharply bounded quantifiers.}
-\begin{definition}\label{def:polynomialinduction}
+Notice that the criterion that $\safe$ does not occur free is not a real restriction, since we can write $\safe (x)$ as $\exists y^\safe . y=x$.
+The criterion is purely to give an appropriate definition of the hierarchy above.
+
+%\anupam{Collection principles for prenexing? Otherwise need to add closure under sharply bounded quantifiers.}
+
+
+\begin{definition}
 [Polynomial induction]
-The \emph{polynomial induction} axiom schema, $\pind$, consists of the following axioms,
+\label{def:polynomialinduction}
+The \emph{polynomial induction} axiom schema, $\pind$, consists of the following axioms, for each formula $A(x)$:
 \[
+\left(
 A(0) 
-\cimp (\forall x^{\normal} . ( A(x) \cimp A(\succ{0} x) ) )
-\cimp  (\forall x^{\normal} . ( A(x) \cimp A(\succ{1} x) ) ) 
+\cand (\forall x^{\normal} . ( A(x) \cimp A(\succ{0} x) ) )
+\cand  (\forall x^{\normal} . ( A(x) \cimp A(\succ{1} x) ) ) 
+\right)
 \cimp  \forall x^{\normal} . A(x)
 \]
-for each formula $A(x)$.
+For a class $\Xi$ of formulae, $\cax{\Xi}{\pind}$ denotes the set of $\pind$ axioms where $A(x) \in \Xi$. 
 
-For a class $\Xi$ of formulae, $\cax{\Xi}{\pind}$ denotes the set of induction axioms when $A(x) \in \Xi$. 
-
 %We write $I\Xi$ to denote the theory consisting of $\basic$ and $\cax{\Xi}{\ind}$.
 \end{definition}
 
 
 \begin{definition}\label{def:ariththeory}
-Define the theory $\arith^i$ consisting of the following axioms:
-\begin{itemize}
-	\item $\basic$;
-	\item $\cpind{\Sigma^\safe_i } $:
-\end{itemize}
-and an inference rule, called $\rais$, for closed formulas $\exists y^\normal . A$:
+Define the theory $\arith^i$ consisting of the $\basic$ axioms, $\cpind{\Sigma^\safe_i } $,
+%\begin{itemize}
+%	\item $\basic$;
+%	\item $\cpind{\Sigma^\safe_i } $:
+%\end{itemize}
+and a particular inference rule, called $\rais$, for closed formulas $\forall x. \exists y. A$:
 \[
- \dfrac{\forall \vec x^\normal . \exists  y^\safe .  A }{ \forall \vec x^\normal .\exists y^\normal . A}
+ \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.
 \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)}
+%\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.}
 
-\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.
+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}
 
-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}
-	[Length induction]
-	The axiom schema of formulae,
-\begin{equation}
-\label{eqn:lind}
-	( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)
-\end{equation}
-	for formulae $A \in \Sigma^\safe_i$
-	is equivalent to $\cpind{\Sigma^\safe_i}$.
-\end{proposition}
-\begin{proof}
-	Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.
-	Then, by $\basic$, we have that $A(|a|) \cimp A(|2a|)$ and $A(|a|) \cimp A(|2a+1|)$ for each $a \in \normal$, whence we may conclude $\forall x. A(|x|)$ by polynomial induction on $A(|x|)$.
-\end{proof}
 
-Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\mathcal C}$, when $A \in \mathcal C$.
-We will freely use this in place of polynomial induction whenever it is convenient.
 
 
 
-
 \subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
 %Todo: $+1$,  
 
-We say that a function $f$ is represented by a formula $A_f$ if the arithmetic can prove (in the forthcoming proof system) 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 result of $f(\vec u; \vec x)$.
+We say that a function $f$ is \emph{represented} by a formula $A_f$ 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)$.
  
-Let us give a few examples of formulas representing basic functions.
+Let us give a few examples for basic functions representable in $\arith^1$:
 \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.
@@ -143,9 +162,90 @@
 
 
 \subsection{A sequent calculus presentation}
+\begin{figure}
+	\[
+	\small
+	\begin{array}{l}
+	\begin{array}{cccc}
+	%\vlinf{\lefrul{\bot}}{}{p, \lnot{p} \seqar }{}
+	%& \vlinf{\id}{}{p \seqar p}{}
+	%& \vlinf{\rigrul{\bot}}{}{\seqar p, \lnot{p}}{}
+	%& \vliinf{\cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta, A }{\Sigma, A \seqar \Pi}
+	\vlinf{id}{}{\Gamma, p \seqar p, \Delta }{}
+	& \vliinf{cut}{}{\Gamma \seqar \Delta }{ \Gamma \seqar \Delta, A }{\Gamma, A \seqar \Delta}
+	&&
+	\\
+	\noalign{\bigskip}
+	%\noalign{\bigskip}
+	\vliinf{\lefrul{\cor}}{}{\Gamma, A \cor B \seqar \Delta}{\Gamma , A \seqar \Delta}{\Gamma, B \seqar \Delta}
+	&
+	\vlinf{\lefrul{\cand}}{}{\Gamma, A\cand B \seqar \Delta}{\Gamma, A , B \seqar \Delta}
+	&
+	%\vlinf{\lefrul{\laand}}{}{\Gamma, A\laand B \seqar \Delta}{\Gamma, B \seqar \Delta}
+	%\quad
+	\vlinf{\rigrul{\cor}}{}{\Gamma \seqar \Delta, A \cor B}{\Gamma \seqar \Delta, A, B}
+	&
+	%\vlinf{\rigrul{\laor}}{}{\Gamma \seqar \Delta, A\laor B}{\Gamma \seqar \Delta, B}
+	%\quad
+	\vliinf{\rigrul{\cand}}{}{\Gamma \seqar \Delta, A \cand B }{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta, B}
+	\\
+	\noalign{\bigskip}
+	
+	\vlinf{\lefrul{\neg}}{}{\Gamma, \neg A \seqar \Delta}{\Gamma \seqar A, \Delta}
+	&
+	
+	\vlinf{\lefrul{\neg}}{}{\Gamma, \seqar \neg A, \Delta}{\Gamma, A \seqar  \Delta}
+	&
+	&
+	%\vliinf{\lefrul{\cimp}}{}{\Gamma, A \cimp B \seqar \Delta}{\Gamma \seqar A, \Delta}{\Gamma, B \seqar \Delta}
+	%&
+	%
+	%\vlinf{\rigrul{\cimp}}{}{\Gamma \seqar \Delta, A \cimp B}{\Gamma, A \seqar \Delta,  B}
+	
+	
+	\\
+	
+	\noalign{\bigskip}
+	%\text{Structural:} & & & \\
+	%\noalign{\bigskip}
+	
+	%\vlinf{\lefrul{\wk}}{}{\Gamma, A \seqar \Delta}{\Gamma \seqar \Delta}
+	%&
+	\vlinf{\lefrul{\cntr}}{}{\Gamma, A \seqar \Delta}{\Gamma, A, A \seqar \Delta}
+	%&
+	%\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, A }{\Gamma \seqar \Delta}
+	&
+	\vlinf{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta, A, A}
+	&
+	&
+	\\
+	\noalign{\bigskip}
+	\vlinf{\lefrul{\exists}}{}{\Gamma, \exists x . A(x) \seqar \Delta}{\Gamma, A(a) \seqar \Delta}
+	&
+	\vlinf{\lefrul{\forall}}{}{\Gamma, \forall x. A(x) \seqar \Delta}{\Gamma, A(t) \seqar \Delta}
+	&
+	\vlinf{\rigrul{\exists}}{}{\Gamma \seqar \Delta, \exists x . A(x)}{ \Gamma \seqar \Delta, A(t)}
+	&
+	\vlinf{\rigrul{\forall}}{}{\Gamma \seqar \Delta, \forall x . A(x)}{ \Gamma \seqar \Delta, A(a) } \\
+	%\noalign{\bigskip}
+	% \vliinf{mix}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta}{\Sigma \seqar \Pi} &&&
+	\end{array}
+	\end{array}
+	\]
+	\caption{Sequent calculus rules, where $p$ is atomic, $i \in \{ 1,2 \}$, $t$ is a term and the eigenvariable $a$ does not occur free in $\Gamma$ or $\Delta$.}\label{fig:sequentcalculus}
+\end{figure}
 
- We denote sequence as $\Gamma \seqar \Delta$ where $\Gamma$, $\Delta$ are multi sets of formulas. The sequent calculus rules are displayed on Fig. \ref{fig:sequentcalculus} in Appendix~\ref{sect:app-sequent-calculus}.
+In order to carry out witness extraction for proofs of $\arith^i$, it will be useful to work with a \emph{sequent calculus} representation of proofs.
+Such systems exhibit strong normal forms, notably `free-cut free' proofs, and so are widely used for the `witness function method' for extracting programs from proofs.
+We introduce the required technical material here only briefly, due to space constraints.
 
+A \emph{sequent} is an expression $\Gamma \seqar \Delta$ where $\Gamma$ and $\Delta$ are multisets of formulas. 
+The inference rules of the sequent calculus $\LK$ are displayed in Fig.~\ref{fig:sequentcalculus}.
+Of course, we have the following:
+\begin{proposition}
+	$A$ is a first-order theorem if and only if there is an $\LK$ proof of $\seqar A$.
+\end{proposition}
+
 %We consider \emph{systems} of `nonlogical' rules extending this sequent calculus, which we write as follows,
 % \[
 % \begin{array}{cc}
@@ -181,16 +281,16 @@
 %
 %As an example any axiom can be represented by such a nonlogical rule $(R)$, with no premise ($I=\emptyset$), $\Delta'$ equal to the axiom and $\Gamma=\Sigma'=\Pi$.
 
-We extend the purely logical calculus with certain non-logical rules and initial sequents corresponding to our theories $\arith^i$.
+We extend this purely logical calculus with certain non-logical rules and initial sequents corresponding to our theories $\arith^i$.
  For instance the axiom $\pind$ of Def. \ref{def:polynomialinduction} is represented by the following rule:
 \begin{equation}
 \label{eqn:ind-rule}
 \small
 \vliinf{\pind}{}{ \normal(t) , \Gamma , A(0) \seqar A(t), \Delta }{ \normal(a) , \Gamma, A(a) \seqar A(\succ{0} a) , \Delta }{ \normal(a) , \Gamma, A(a) \seqar A(\succ{1} a) , \Delta  }
 \end{equation}
-where $I=2$ and  in all cases, $t$ varies over arbitrary terms and the eigenvariable $a$ does not occur in the lower sequent of the $\pind$ rule.
-
-Similarly the $\rais$ inference rule of Def. \ref{def:ariththeory} is represented by the nonlogical rule:
+where $t$ varies over arbitrary terms and the eigenvariable $a$ does not occur in the lower sequent.
+%
+Similarly the $\rais$ inference rule of Dfn.~\ref{def:ariththeory} is represented by the nonlogical rule,
  \[
  \begin{array}{cc}
     \vlinf{\rais}{}{  \normal(t_1), \dots, \normal(t_k) \seqar  \exists  y^\normal .  A }{  \normal(t_1), \dots, \normal(t_k) \seqar \exists  y^\safe .  A}
@@ -204,8 +304,9 @@
 %\end{array}
 %\]
 %}
-
-The $\basic$ axioms are equivalent to the following nonlogical rules, that we will also designate by $\basic$:
+%
+and the $\basic$ axioms are represented by designated initial sequents.
+For instance here are some initial sequents corresponding to some of the $\basic$ axioms:
 \[
 \small
 \begin{array}{l}
@@ -226,12 +327,21 @@
 \end{array}
 \]
 
- The sequent calculus for $\arith^i$ is that of Fig. \ref{fig:sequentcalculus} extended with the $\basic$,  $\cpind{\Sigma^\safe_i } $ and $\rais$ nonlogical rules.
+The sequent system for $\arith^i$ extends $\LK$ by the $\basic$,  $\cpind{\Sigma^\safe_i } $ and $\rais$ nonlogical rules.
+ Naturally, by completeness, we have that $\arith^i \proves A$ if and only if there is a sequent proof of $\seqar A$.
+ In fact, by \emph{free-cut elimination} results \cite{Takeuti87,Cook:2010:LFP:1734064} we may actually say something much stronger.
  
-\todo{Present typed variable free-cut free form.}
-\anupam{I cut-and-pasted the rest of this section into appendices to save space. Move things back gradually.}
-
+ Let us say that a sorting $(\vec u ; \vec x)$ of the variables $\vec u , \vec x$ is \emph{compatible} with a formula $A$ if each variable of $\vec x$ occurs hereditarily safe with respect to the $\bc$-typing of terms, i.e.\ never under $\smsh, |\cdot|$ and to the right of $\times$.
+ 
 \begin{theorem}
 	[Typed variable normal form]
 	\label{thm:normal-form}
-\end{theorem}
\ No newline at end of file
+	If $\arith^i\proves  A$ then there is a $\arith^i$ sequent proof $\pi$ of $A$ such that each line has the form:
+	\[
+	\normal(\vec u), \safe (\vec x), \Gamma \seqar \Delta
+	\]
+	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 typing 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.
\ No newline at end of file
