\section{Soundness}
\label{sect:soundness}

The main result of this section is the following:

\begin{theorem}
	\label{thm:soundness}
	If $\arith^i$ proves $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that $\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x))$.
\end{theorem}



The main problem for soundness is that we have predicates, for example equality, that take safe arguments in our theory but do not formally satisfy the polychecking lemma for $\mubc$ functions. 
For this we will use length-bounded witnessing, borrowing a similar idea from Bellantoni's previous work \cite{Bellantoni95}.


\begin{definition}
[Length bounded basic functions]
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 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 $\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}


\begin{proposition}
	$\charfn{}{A} (l, \vec u ; \vec x)$ is the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
\end{proposition}

\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$.
	\[
	\begin{array}{rcl}
	\Wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) & \dfn & \charfn{}{A} (l, \vec u ; \vec x)  \text{ if $A$ is $\Pi_i$} \\
	\smallskip
	\Wit{\vec u ; \vec x}{A \cor B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cor ( ; \Wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B)  )  \\
	\smallskip
	\Wit{\vec u ; \vec x}{A \cand B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cand ( ; \Wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B)  )  \\
	\smallskip
	\Wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (l,\vec u ; \vec x , \vec w , w) & \dfn & \Wit{\vec u ; \vec x , x}{A(x)} ( l,\vec u ; \vec x , w , \vec w )
	\\
	\smallskip
	\Wit{\vec u ; \vec x}{\forall u \leq |t(\vec u;)| . A(x)} (l , \vec u ; \vec x, w) & \dfn & 
	\forall u \leq |t(\vec u;)| . \Wit{u , \vec u ; \vec x}{A(u)} (l, u , \vec u ; \vec x, \beta(u;w) )
	\end{array}
	\]
\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}
	If, for some $w$, $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$, then $A$ is true.
	\anupam{check statement, need proof-theoretic version?}
\end{proposition}

In order to prove Thm.~\ref{thm:soundness} we need the following lemma:


\begin{lemma}
	[Proof interpretation]
	\label{lem:proof-interp}
	For any $\arith^i$ proof of a $\Sigma^\safe_i$ sequent $\Gamma \seqar \Delta$, there is a $\mubci{i-1}$ function $f$ such that, for any $l, \vec u , \vec x  , w$, we have:
	\[
	\wit{\vec u ; \vec x}{ \wedge \Gamma } (l, \vec u ; \vec x , w) 
	\quad \leq \quad
	\wit{\vec u ; \vec x}{\vee \Delta} (l, \vec u ; \vec x , f(l, \vec u ; \vec x , w))
	\]
	\anupam{maybe want $f(\vec u \mode l ; \vec x \mode l , w)$}
\end{lemma}
\begin{proof}
	We assume the proof, say $\pi$, is in integer positive free-cut free form, by the results from the previous section.
	This means that the predicate $\charfn{\vec u ; \vec x}{A}$ is defined for each formula $A(\vec u ; \vec x)$ occurring in a proof, so the theorem is well-stated.
	We define the function $f$ inductively, by considering the various final rules of $\pi$.
	
	\paragraph*{Negation}
	Can assume only on atomic formulae, so no effect.	
	\paragraph*{Quantifiers}
	\anupam{Do $\exists$-right and $\forall$-right, left rules are symmetric.}
	
	\paragraph*{Contraction}
	Left contraction simply duplicates an argument, whereas right contraction requires a conditional on a $\Sigma^\safe_i$ formula.

	\paragraph*{Induction}
	Corresponds to safe recursion on notation.
\end{proof}

We are now ready to prove the soundness theorem.

\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(l, \vec u;) ) =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.
\end{proof}

