Index: soundness.tex
===================================================================
--- soundness.tex	(revision 224)
+++ soundness.tex	(revision 225)
@@ -15,81 +15,60 @@
 
 
 \begin{definition}
-[Length bounded basic functions]
-We define \emph{length-bounded equality}, $\eq(l;x,y)$ as the characteristic function of the predicate:
+[Length bounded (in)equality]
+%We define \emph{length-bounded equality}, $\eq(l;x,y)$ as the characteristic function of the predicate:
+%\[
+%x \mode l = y \mode l
+%\]
+%which is definable by safe recursion on $l$:
+%\[
+%\begin{array}{rcl}
+%\eq (0 ; x,y) & \dfn & \equivfn (;\bit (0;x),\bit(0;y) ) \\
+%\eq (\succ i l; x,y) & \dfn & \cond (; \eq ( u;x,y ) , 0, \equivfn (; \bit (\succ i u ; x ) , \bit (\succ i l ; y ))  )
+%\end{array}
+%\]
+We define \emph{length-bounded inequality} as:
 \[
-x \mode l = y \mode l
-\]
-which is definable by safe recursion on $l$:
-\[
 \begin{array}{rcl}
-\eq (0 ; x,y) & \dfn & \equivfn (;\bit (0;x),\bit(0;y) ) \\
-\eq (\succ i l; x,y) & \dfn & \cond (; \eq ( u;x,y ) , 0, \equivfn (; \bit (\succ i u ; x ) , \bit (\succ i l ; y ))  )
+\leqfn (0 ; x ,y) & \dfn & \cond(; \bit (0;x), 1, \bit (0;y) ) \\
+\leqfn (\succ i l ; x,y) & \dfn & \orfn ( ; \cond(;\bit (\succ i l ; x) , \bit(\succ i l ; y),0 ) , \andfn (; \equivfn (\bit (\succ i l ; x) , \bit(\succ i l ; y)) , \leqfn (l;x,y ) ) )
 \end{array}
 \]
-We also define length-bounded inequality as:
-\[
-\begin{array}{rcl}
-\leqfn (0 ; x ,y) & \dfn & \cimp (; \bit (0;x), \bit (0;y) ) \\
-\leqfn (\succ i l ; x,y) & \dfn & \orfn ( ; <(\bit (\succ i l ; x) , \bit(\succ i l ; y) ) , \andfn (; \equivfn (\bit (\succ i l ; x) , \bit(\succ i l ; y)) , \leqfn (l;x,y ) ) )
-\end{array}
-\]
 \end{definition}
 
-\anupam{Do we need the general form of length-boundedness? E.g. the $*$ functions from Bellantoni's paper? Put above if necessary. Otherwise just add sequence manipulation functions as necessary.}
+Notice that $\leqfn (l; x,y) = 1$ just if $x \mode l \leq y \mode l$.
+We can also define $\eq( l; x,y)$ as $\andfn (;\leq(l;x,y),\leq(l;y,x))$.
 
-Notice that $\eq$ is a polymax bounded polyomial checking function on its normal input, and so can be added to $\mubc$ without problems.
+%\anupam{Do we need the general form of length-boundedness? E.g. the $*$ functions from Bellantoni's paper? Put above if necessary. Otherwise just add sequence manipulation functions as necessary.}
+%
+%Notice that $\eq$ is a polymax bounded polyomial checking function on its normal input, and so can be added to $\mubc$ without problems.
 
-\begin{definition}
-	[Length bounded characteristic functions]
-	We define $\mubci{}$ programs $\charfn{}{A} (l , \vec u; \vec x)$, parametrised by a formula $A(\vec u ; \vec x)$, as follows.
-%	If $A$ is a $\Pi_{i}$ formula then:
-	\[
-	\begin{array}{rcl}
-	\charfn{}{s\leq t} (l, \vec u ; \vec x) & \dfn & \leqfn(l;s,t) \\
-	\smallskip
-	\charfn{}{s=t} (l, \vec u ; \vec x) & \dfn & \eq(l;s,t) \\
-	\smallskip
-	\charfn{}{\neg A} (l, \vec u ; \vec x) & \dfn & \neg (;\charfn{}{A}(l , \vec u ; \vec x)) \\
-	\smallskip
-	\charfn{}{A\cor B} (l, \vec u ; \vec x ) & \dfn & \cor (; \charfn{}{A} (l, \vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x) ) \\
-	\smallskip
-	\charfn{}{A\cand B} (l, \vec u ; \vec x ) & \dfn & \cand(; \charfn{}{A} (l, \vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x) ) \\
-	\smallskip
-	\charfn{}{\exists x^\safe . A(x)} (l, \vec u ;\vec x) & \dfn & \begin{cases}
-	1 & \exists x^\safe . \charfn{}{A(x)} (l, \vec u ;\vec x , x) = 1 \\
-	0 & \text{otherwise} 
-	\end{cases} \\
-	\smallskip
-	\charfn{}{\forall x^\safe . A(x)} (l, \vec u ;\vec x ) & \dfn & 
-	\begin{cases}
-	0 & \exists x^\sigma. \charfn{}{ A(x)} (l, \vec u; \vec x , x) = 0 \\
-	1 & \text{otherwise}
-	\end{cases}
-	\end{array}
-	\]
-\end{definition}
+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$-types of terms (see App.~\ref{appendix:arithmetic}). 
+In the presence of a compatible sorting, we may easily define functions that \emph{evaluate} safe formulae in $\mubc$:
 
-\anupam{Above and below definitions need to be with respect to a typing of variables which terms respect.}
 
-
 \begin{proposition}
-	$\charfn{}{A} (l, \vec u ; \vec x)$ is the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
+Given a $\Sigma^\safe_i$ formula $A$ and compatible sorting $(\vec u; \vec x)$ of its variables, there is a $\mubci{i-1}$ program $\charfn{\vec u ;\vec x}{A} (l, \vec u ; \vec x)$ computing the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
 \end{proposition}
 
+
+We will use the programs $\charfn{}{}$ in the witness functions we define below.
+Let us write $\charfn{}{i}$ to denote the class of functions $\charfn{}{A}$ for $A \in \Pi^\safe_{i-1}$.
+For the notion of bounding polynomial below we are a little informal with bounds, using `big-oh' notation, since it will suffice just to be `sufficiently large'.
+
+
 \begin{definition}
 	[Length bounded witness function]
-	We now define $\Wit{\vec u ; \vec x}{A} (l , \vec u ; \vec x)$ for a $\Sigma_{i+1}$-formula $A$ with free variables amongst $\vec u; \vec x$.
-	For a $\Sigma^\safe_i$ formula $A$ with free variables amongst $(\vec u ; \vec x)$, with $\vec x$ occurring only hereditarily safe in terms, we define the \emph{length-bounded witness function} $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w)$ and its \emph{bounding polynomial} $b_A (l)$ as follows:
+	For a $\Sigma^\safe_{i}$ formula $A$ with a compatible sorting $(\vec u ; \vec x)$, we define the \emph{length-bounded witness function} $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w)$ in $\bc (\charfn{}{i})$ and its \emph{bounding polynomial} $b_A (l)$ as follows:
 	\begin{itemize}
-		\item If $A$ is $\Pi^\safe_{i-1}$ then $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) \dfn \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x )$.
-		\item If $A$ is $B \cor C$ then 
-		\[
-		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) 
-		\quad \dfn \quad
-		\orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )
-		\]
-		and we may set $b_A = O(b_B + b_C)$.
+		\item If $A$ is $\Pi^\safe_{i-1}$ then $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) \dfn \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x )$ and we set $b_A (l) = 1$.
+		\item If $A$ is $B \cor C$ then we may set $b_A = O(b_B + b_C)$ and define $		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) \dfn		\orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )$.
+%		\[
+%		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) 
+%		\quad \dfn \quad
+%		\orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )
+%		\]
+%		and we may set $b_A = O(b_B + b_C)$.
 		\item Similarly if $A $ is $B \cand C$, but with $\andfn$ in place of $\orfn$.
 %		\item If $A$ is $B \cand C$ then
 %			\[
@@ -98,22 +77,25 @@
 %			\andfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )
 %			\]
 %			and we may set $b_A = O(b_B + b_C)$.
-		\item If $A$ is $\forall u \leq |t(\vec u;)| . B(u)$ then 
-		\[
+		\item If $A$ is $\forall u \leq |t(\vec u;)| . B(u)$ we appeal to sharply bounded closure, Lemma~\ref{lem:sharply-bounded-recursion}, to define
+		\(
 		\wit{\vec u ; \vec x}{A}
-		\quad \dfn\quad
-		\forall u\normal \leq |t|.
+		 \dfn
+		\forall u \leq |t|.
 		\wit{u, \vec u ; \vec x}{B(u)} (l, u, \vec u ; \vec x , \beta( b_{B(t)} (l) , u ; w ) )
-		\]
-		appealing to Lemma~\ref{lem:sharply-bounded-recursion}, where we may set $b_A = O(b_{B(t)}^2 )$.
+		\)
+		%appealing to Lemma~\ref{lem:sharply-bounded-recursion}, 
+		and 
+		we set 
+		$b_A = O(b_{B(t)}^2 )$.
 		\item Similarly if $A$ is $\exists u^\normal \leq |t(\vec u;)|. A'(u)$, but with $\exists u \leq |t|$ in place of $\forall u \leq |t|$.
 		\item If $A$ is $\exists x^\safe . B(x) $ then
-		\[
+		\(
 		\wit{\vec u ; \vec x}{A}
-		\quad \dfn \quad
+		\dfn 
 		\wit{\vec u ; \vec x , x}{B(x)} ( l, \vec u ; \vec x , \beta( b_{B} (l) , 0;w ) , \beta (q(l) , 1 ;w ))
-		\]
-		where $q$ is obtained by the polychecking and bounded minimisation lemmata for $\wit{\vec u ; \vec x , x}{B(x)}$.
+		\)
+		where $q$ is obtained by the polychecking and bounded minimisation properties, Lemmas~\ref{lem:polychecking} and \ref{lem:bounded-minimisation}, for $\wit{\vec u ; \vec x , x}{B(x)}$.
 		We may set $b_A = O(b_B + q )$.
 	\end{itemize}
 %	\[
@@ -134,56 +116,45 @@
 %	\anupam{need length bounding for sharply bounded quantifiers}
 \end{definition}
 
-\anupam{may as well use a single witness variable since need it for sharply bounded quantifiers anyway.}
 
-\anupam{sharply bounded case obtained by sharply bounded lemma}
 
-
 \begin{proposition}
+	\label{prop:wit-rfn}
 	If, for some $w$, $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$, then $A (\vec u \mode l ; \vec x \mode l)$ is true.
-	\anupam{check statement, need proof-theoretic version?}
+Conversely, if $A (\vec u \mode l ; \vec x \mode l)$ is true then there is some $w \leq b_A(l)$ such that $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$.
 \end{proposition}
 
-By the polychecking lemma, we can assume that such a $w$ is bounded by some polynomial in $l$.
 
-In order to prove Thm.~\ref{thm:soundness} we need the following lemma:
+In order to prove Thm.~\ref{thm:soundness} we need the following lemma, essentially giving an interpretation of $\arith^i$ proofs into $\mubci{i-1}$:
 
 
 \begin{lemma}
 		[Proof interpretation]
 		\label{lem:proof-interp}
-	From a normal form \todo{define, prove exists} $\arith^i$ proof $\pi$ of a $\Sigma^\safe_i$ sequent $\normal(\vec u), \safe(\vec x) , \Gamma  \seqar \Delta$
-	there are $\mubci{i-1}$ functions $\vec f^\pi (\vec u ; \vec x , w)$ (where $\vec f^\pi = (f^\pi_B)_{B\in\Delta}$) such that, for any $l, \vec u ; \vec x  , w$, we have:
+	From a typed-variable normal form $\arith^i$ proof $\pi$ of a $\Sigma^\safe_i$ sequent $\normal(\vec u), \safe(\vec x) , \Gamma  \seqar \Delta$
+	there are $\bc (\charfn{}{i})$ functions $ f^\pi_B (\vec u ; \vec x , w)$ for $B\in\Delta$ such that
+	% such that, for any $l, \vec u ; \vec x  , w$, we have:
 	\[
 %	\vec a^\nu = \vec u ,
 %	\vec b^\sigma = \vec u, 
 	\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A) =1
-	\quad \implies \quad
-	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B(\vec u \mode l ; \vec x \mode l, \vec w)) = 1
+	\ \implies \
+	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B((\vec u ; \vec x )\mode l, \vec w \mode p(l))) = 1
 	\]
-	\anupam{Need $\vec w \mode p(l)$ for some $p$.}
-	\anupam{$l$ may occur freely in the programs $f^\pi_B$}
+	for some polynomial $p$.
+%	\anupam{Need $\vec w \mode p(l)$ for some $p$.}
+%	\anupam{$l$ may occur freely in the programs $f^\pi_B$}
 \end{lemma}
 
 
-\todo{Make statement above proper, with all bounds and moduli. I cut the proof to the appendix, maybe add sketch if space.}
 
-From this lemma we can readily prove the soundness result:
+
+Now we can prove the soundness result:
 	
 	\begin{proof}
 		[Proof of Thm.~\ref{thm:soundness} from Lemma~\ref{lem:proof-interp}]
-		(watch out for dependence on $l$, try do without)
-		
-		Suppose $\arith^i \proves \forall \vec u^\normal . \exists x^\normal . A(\vec u ; x)$. Then by raising, inversion, free-variable normal forms, we have a proof of,
-		\[
-		\normal (\vec u ) \seqar \exists x^\normal . A(\vec u , x ;)
-		\]
-		whence, by Lemma~\ref{lem:proof-interp}, we have a $\mubci{i-1}$ function $f$ such that:
-		\[
-		\vec u \mode l = \vec a \mode l
-		\quad \implies \quad
-		\wit{\vec u ; }{A} ( l , \vec u , f(\vec u \mode l;) ) =1
-		\]
-		
-		Now it suffices to choose an $l$ bigger that both all the $\vec u$ and $f(\vec u)$, which is a polynomial in $\vec u$ by the polymax bounding lemma.
+		Suppose $\arith^i \proves \forall \vec u^\normal . \exists x^\safe . A(\vec u ; x)$. By inversion and Thm.~\ref{thm:normal-form} there is a $\arith^i$ proof $\pi$ of $\normal (\vec u ) \seqar \exists x^\safe. A(\vec u ; x )$ in typed variable normal form.
+By Lemma~\ref{lem:proof-interp}, we have a $\mubci{i-1}$ function $f^\pi$ with $\wit{\vec u ;}{\exists x^\safe . A} (l, \vec u ; f(\vec u \mode l;)) =1$.
+By the definition of $\wit{}{}$ and Prop.~\ref{prop:wit-rfn} we have that $\exists x . A(\vec u \mode l; x)$ is true just if $A(\vec u \mode l ; \beta (q(l), 1 ; f(\vec u \mode l;) ))$ is true.
+Now, since all $\vec u$ are normal, we may simply set $l$ to have a longer length than all of these arguments, so the function $f(\vec u;) \dfn \beta (q(\sum \vec u), 1 ; f(\vec u \mode \sum \vec u;) ))$ suffices.
 	\end{proof}
