Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\section{Soundness}

\label{sect:soundness}

In this section we show that the representable functions of our theories $\arith^i$ are in $\fphi i$ (`soundness').

The main result is the following:

\begin{theorem}

	\label{thm:soundness}

	If $\arith^i$ proves $\forall \vec u^\normal  . \exists y^\safe . A(\vec u ;  y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; )$ such that $\Nat \models A(\vec u ;  f(\vec u ; ))$.

\end{theorem}

The 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, Lemma~\ref{lem:polychecking}. 

For this we will use \emph{length-bounded} witnessing argument, borrowing a similar idea from Bellantoni's work \cite{Bellantoni95}.

\begin{definition}

[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:

\[

\begin{array}{rcl}

\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}

\]

\end{definition}

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 (;\leqfn(l;x,y),\leqfn(l;y,x))$.

%\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.

In the presence of a compatible sorting, we may easily define functions that \emph{evaluate} safe formulae in $\mubc$:

\begin{definition}

	[Length bounded characteristic functions]

	We define $\mubci{}$ programs $\charfn{}{A} (l , \vec u; \vec x)$, parametrised by a formula $A$ and a compatible typing $(\vec u ; \vec x)$ of its varables, as follows.

	%	If $A$ is a $\Pi_{i}$ formula then:

	\[

	\begin{array}{rcl}

	\charfn{\vec u ; \vec x}{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{\vec u ; \vec x}{\neg A} (l, \vec u ; \vec x) & \dfn & \notfn (;\charfn{\vec u ; \vec x}{A}(l , \vec u ; \vec x)) \\

	\smallskip

	\charfn{\vec u ; \vec x}{A\cor B} (l, \vec u ; \vec x ) & \dfn & \orfn(; \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w), \charfn{\vec u ; \vec x}{B} (\vec u ;\vec x) ) \\

	\smallskip

	\charfn{\vec u ; \vec x}{A\cand B} (l, \vec u ; \vec x ) & \dfn & \andfn(; \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w), \charfn{\vec u ; \vec x}{B} (\vec u ;\vec x) )

	%	\end{array}

	%	\quad

	%	\begin{array}{rcl}

	\\	\smallskip

	\charfn{\vec u ; \vec x}{\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{\vec u ; \vec x}{\forall x^\safe . A(x)} (l, \vec u ;\vec x ) & \dfn & 

	\begin{cases}

	0 & \exists x^\sigma. \charfn{\vec u ; \vec x}{ A(x)} (l, \vec u; \vec x , x) = 0 \\

	1 & \text{otherwise}

	\end{cases}

	\end{array}

	\]

\end{definition}

\begin{proposition}

Given a $\Sigma^\safe_i$ formula $A$ and compatible sorting $(\vec u; \vec x)$ of its variables, 

$\charfn{\vec u ;\vec x}{A} (l, \vec u ; \vec x)$ is in $\mubci{i}$ and computes 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 \Sigma^\safe_{i}$.

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'.

Notice that, while we refer to $b_A(l), p(l)$ etc.\ below as a `polynomial', we really mean a \emph{quasipolynomial} (which may also contain $\smsh$), i.e.\ a polynomial in the \emph{length} of $l$, as a slight abuse of notation.

\begin{definition}

	[Length bounded witness function]

	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-1})$ 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 )$ 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

%			\[

%			\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) 

%			\quad \dfn \quad

%			\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)$ we appeal to sharply bounded closure, Lemma~\ref{lem:sharply-bounded-recursion}, to define

		\(

		\wit{\vec u ; \vec x}{A}

		 \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}, 

		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}

		\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 properties,\footnote{Here let us assume that $q$ is formulated as a corresponding quasipolynomial in $l$ as opposed to a polynomial in $|l|$, as in Lemma~\ref{lem:bounded-minimisation}.} 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}

%	\[

%	\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}

%	\]

%	\anupam{need length bounding for sharply bounded quantifiers}

\end{definition}

From Lemmas~\ref{lem:polychecking} and \ref{lem:bounded-minimisation} we have:

\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.

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}

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 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-1})$ functions $ f^\pi_B (\vec u ; \vec x , \vec 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

%	\ \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

	\begin{array}{rl}

&	\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A 

%\mode b_A(l)

) =1 \\

\noalign{\medskip}

\implies & 	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B(l,

(

\vec u ; \vec x 

)	\mode l

, \vec w \mode p^\pi(l))) = 1

	\end{array}

	\]

	for some polynomial $p^\pi$.

%	\anupam{Need $\vec w \mode p(l)$ for some $p$.}

%	\anupam{$l$ may occur freely in the programs $f^\pi_B$}

\end{lemma}

For the implication above, let us simply refer to the LHS as $\Wit{\vec u ; \vec x}{\Gamma} (l , \vec u ; \vec x , \vec w)$ and the RHS as $\Wit{\vec u ; \vec x}{ \Delta} (l, \vec u ; \vec x , \vec f^\pi (

l,(

\vec u ; \vec x 

)\mode l

, \vec w \mode p^\pi(l))  )$, which is a slight abuse of notation: we assume that LHS and RHS are clear from context.

Also let us call $p^\pi$ the \emph{modulus} of $f^\pi$ with respect to $l$.

\begin{proof}[Proof sketch]

	Since the proof is in typed variable normal form we have that each line of the proof is of the same form, i.e.\ $\normal (\vec u), \safe (\vec x) , \Gamma \seqar \Delta$ over free variables $\vec u ; \vec x$.

	We define the function $f^\pi$ inductively, by considering the various final rules of $\pi$.

	\paragraph*{Negation}

Suppose $\pi$ ends with a right negation step:

\[

\vlinf{\rigrul{\cnot}}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \cnot A , \Delta }{\normal (\vec u) , \safe (\vec x) , \Gamma , A\seqar  \Delta}

\]

Notice that, since $\pi$ is in De Morgan form, we have that $A$ is atomic ($s\leq t$) and so, in particular, $\Pi^\safe_{i-1}$.

So we can simply set the witness for both $A$ and $\cnot A$ to $0$.

Namely, if $\vec f (l,\vec u ; \vec x , \vec w , w )$ is obtained by the inductive hypothesis, then we may set $f^\pi_B (l, \vec u ; \vec x , \vec w) \dfn f_B (l,\vec u ;\vec x , \vec w , 0)$ for $B\in \Delta$, and $f^\pi_A (\vec u ; \vec x , \vec w) \dfn 0$. 

The modulus $p^\pi$ remains the same as that of the inductive hypothesis. 

Left negation is similar, relying on a dummy argument.

	\paragraph*{Logical rules}

%	Pairing, depairing. Need length-boundedness.

	Suppose $\pi$ ends with a 

	left conjunction step:

	\[

	\vlinf{\lefrul{\cand}}{}{ \normal (\vec u ), \safe (\vec x) , A\cand B , \Gamma \seqar \Delta }{ \normal (\vec u ), \safe (\vec x) , A, B , \Gamma \seqar \Delta}

	\]

	By inductive hypothesis we have functions $\vec f (l,\vec u ; \vec x , w_A , w_B , \vec w)$ such that,

	\[

	\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , w_A , w_B , \vec w)

	\quad \implies \quad

	\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , \vec f (

	l, (

	\vec u ; \vec x

	) \mode l 

	, (w_A , w_B , \vec w) \mode p(l) ))

	\]

	for some polynomial $p$.

	%

	We define $\vec f^\pi (l,\vec u ; \vec x , w , \vec w) \dfn \vec f (l,\vec u ; \vec x , \beta (p(l),0; w) , \beta(p(l),1;w),\vec w )$ and, by the bounding polynomial for pairing, it suffices to set $|p^\pi| = O(|p|)$.

	Suppose $\pi$ ends with a right disjunction step:

		\[

		\vlinf{\rigrul{\cor}}{}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta , A \cor B}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta, A, B }

		\]

		$\vec f^\pi_\Delta$ remains the same as that of premiss.

		Let $\vec f , f_A, f_B$ be obtained by the inductive hypothesis so that:

		\[

		\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , \vec w)

		\quad \implies \quad

		\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , (\vec f , f_A , f_B) ( 

		l,(

		\vec u ; \vec x

		) \mode l 

		, \vec w \mode p(l) ))		

		\]

		$\vec f^\pi_\Delta$ is defined the same as $\vec f$. 

		Let $q(l)$ be an upper bound for $f_A , f_B$  and define $f^\pi_{A\cor B} (\vec u ; \vec x, \vec w) \dfn \pair{q(l)}{f_A ((\vec u ; \vec x, \vec w))}{f_B ((\vec u ; \vec x, \vec w))}$.

		$p^\pi$ is obtained from $p$, $q$ and the bounding polynomial for pairing.

	The other logical cases use a similar argument.

	\paragraph*{Quantifiers}

	Sharply bounded quantifier steps use a similar argument to the logical rules above, only requiring a larger modulus.

%	If $\pi$ ends with a sharply bounded quantifier step, then we use a similar argument to that for logical rules. 

%	For instance, suppose $\pi$ ends with a $\rigrul{|\forall|}$:

%	\[

%	\vlinf{\rigrul{|\forall|}}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar  \Delta , \forall u^\normal \leq |t(\vec u;)| . A(u) }{ \normal(u) , \normal (\vec u) , \safe (\vec x) , u \leq |t(\vec u;)| , \Gamma \seqar  \Delta, A(u)  }

%	\]

%	By the inductive hypothesis we have functions $\vec f(u , \vec u ; \vec x , w , \vec w)$ such that:

%	\[

%	\Wit{u ,\vec u ; \vec x}{\lhs} ( u , \vec u ;\vec x , w , \vec w )

%	\quad \implies \quad

%	\Wit{u , \vec u ; \vec x}{\rhs} (u, \vec u ; \vec x , \vec f ((\vec u ; \vec x) \mode l , \vec w \mode p(l) ) )

%	\]

%	with $|f|\leq q(|l|)$.

%	

%	By Lemma~\ref{lem:sequence-creation}, we have a function $F (l , u , \vec u ; \vec x , w , \vec w) $ such that....

%	

%	We set $f^\pi_{\forall u^\normal \leq t . A} (\vec u ; \vec x , \vec w) \dfn F(q(|l|), t(\vec u;), \vec u ; \vec x , 0, \vec w  )$.

%	

%		\anupam{Do $\exists$-right and $\forall$-right, left rules are symmetric.}

Suppose $\pi$ ends with a right existential step:\footnote{	Here we assume the variables of $t$ are amongst $(\vec u ; \vec x)$, since we are in typed variable normal form.}

	\[

	\vlinf{\rigrul{\exists}}{}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x . A(x)}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , A(t (\vec u ; \vec x))}

	\]

By the inductive hypothesis we have functions $\vec f , f$ such that:

\[

\Wit{\vec u ;\vec x}{\Gamma} ( l , \vec u ; \vec x , \vec w )

\quad \implies \quad

\Wit{\vec u ; \vec x}{\Delta, A(t)} ( l, \vec u ; \vec x , (\vec f , f) (l, (\vec u ; \vec x) \mode l , \vec w \mode p(l) ) )

\]

We let $\vec f^\pi_\Delta \dfn \vec f$ and define $f^\pi_{\exists x . A } ( l, \vec u ; \vec x , \vec w ) \dfn \pair{p(l) + t(\vec l ; \vec l)}{f(l, \vec u ; \vec x , \vec w)}{t(\vec u ; \vec x)}$.

$p^\pi$ is hence obtained from $t$, $p$ and the bounding polynomial for pairing.

	Other quantifier steps are routine.

	\paragraph*{Contraction}

	Left contraction simply duplicates an argument,\footnote{We ignore here the cases when contraction is on a $\normal (u) $ or $\safe (x)$ formula, treating these formulae form as forming a set rather than a multiset.} whereas right contraction requires a conditional on a $\Sigma^\safe_i$ formula.

	This is the reason why we need to the witness function encoded itself into $\mubc$ rather than simply using a predicate.

	Suppose $\pi$ ends with a right contraction step:

	\[

	\vlinf{\cntr}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A }{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A , A}

	\]

	By the inductive hypothesis we have functions $\vec f_\Delta , f_0, f_1$ corresponding to the RHS $\Delta , A ,A$.

	We may define $\vec f^\pi_\Delta = \vec f_\Delta$ and:

	\[

	f^\pi_A (l, \vec u ; \vec x , \vec w  )

	\quad \dfn \quad

	\cond (; \wit{\vec u ; \vec x}{A} ( l , \vec u ; \vec x , f_0(l,\vec u ; \vec x , \vec w) ) , f_1(l,\vec u ; \vec x , \vec w) , f_0(\vec u ; \vec x , \vec w)  )

	\]

%	\anupam{For $\normal (\vec u), \safe (\vec x)$ in antecedent, we always consider as a set, so do not display explicitly contraction rules. }

	\paragraph*{Induction}

Suppose $\pi$ ends with a polynomial induction step:

	\[

	\vlinf{\pind}{}{ \normal (\vec u), \safe (\vec x) , \Gamma, A(0) \seqar A(t(\vec u ;)) , \Delta}{ \left\{\normal (u) , \normal (\vec u) , \safe (\vec x) , \Gamma,  A(u) \seqar A(\succ i u ) , \Delta \right\}_{i=0,1} }

	\]

%	\anupam{need to say in normal form part that can assume induction of this form}

	For simplicity we will assume $\Delta $ is empty.\footnote{Note that a proof can always be put into this form by the right disjunction rules. The criterion on logical complexity for typed variable normal form proofs is preserved due to free-cut freeness.}

	%

	Now, by the inductive hypothesis, we have functions $h_i$ such that:

	\[

	\Wit{u , \vec u ; \vec x}{\Gamma, A(0)} (l , u , \vec u ; \vec x ,  \vec w , w)

	\quad \implies \quad

	\Wit{u , \vec u ; \vec x}{A(\succ i u)} (l , u , \vec u ; \vec x ,  h_i (l,(u , \vec u ; \vec x ) \mode l , (\vec w , w) \mode p(l) ) )

	\]

	First let us define $ f$ by safe recursion as follows:

	\[

	\begin{array}{rcl}

	f (l,0 , \vec u ; \vec x, \vec w,  w ) & \dfn &  w\\

	f(l, \succ i u , \vec u ; \vec x , \vec w, w) & \dfn & 

	h_i (l,u , \vec u ; \vec x , \vec w , f(l,u , \vec u ; \vec x , \vec w , w ))

	\end{array}

	\]

%	where $\vec w$ corresponds to $\Gamma $ and $w$ corresponds to $A(0)$.

%	\anupam{Wait, should $\normal (t)$ have a witness? Also there is a problem like Patrick said for formulae like: $\forall x^\safe . \exists y^\safe. (\normal (z) \cor \cnot \normal (z))$, where $z$ is $y$ or otherwise.}

	Now we let $f^\pi (\vec u ; \vec x , \vec w) \dfn f(t(\vec u ; ) , \vec u ; \vec x , \vec w)$.

	It suffices to let $|p^\pi| = O(|p|^2)$.

	\paragraph*{Cut}

	If $\pi$ ends with a cut on an induction formula, which is $\Sigma^\safe_i$, then $f^\pi$ is obtained from the inductive hypothesis by simply substituting already defined functions into a safe position.

	The other possibility is that $\pi$ ends with a `raisecut':

	\[

	\vliinf{\rais\cut}{}{\normal (\vec u ) , \normal (\vec v) , \safe (\vec x) ,\Gamma \seqar \Delta }{ \normal (\vec u) \seqar \exists x^\safe  . A(x) }{ \normal (u)  , \normal (\vec v) , \safe (\vec x) , A(u), \Gamma \seqar \Delta }

	\]

	In this case, by the inductive hypothesis, we have functions $f(l,\vec u ; )$ from the left premiss and $\vec g (l,u, \vec v ; \vec x , w , \vec w )$ from the right premiss, so we may define:

	\[

	\vec f^\pi ( l ,  \vec u , \vec v ; \vec x , \vec w )

	\quad \dfn \quad

	\vec g ( l, \beta (1 ; f(l,\vec u ;) ) , \vec v ; \vec x , \beta(0;f(l,\vec u ;)) , \vec w )

	\]

	Again, $p^\pi$ is obtained from $p$ and the bounding polynomial for pairing.

\end{proof}

Now we can prove the soundness result:

	\begin{proof}

		[Proof sketch of Thm.~\ref{thm:soundness} from Lemma~\ref{lem:proof-interp}]

		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^\pi(l,\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(l, \vec u \mode l;) ))$ is true, where $q(l)$ is an upper bound for $f^\pi (l, \vec u \mode l ; )$.

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;) ))$ indeed witnesses the required existential.

	\end{proof}