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

	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 ; ))$.

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

%\mode b_A(l)

) =1 \\

\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

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.

\begin{proof}[Proof sketch]

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

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

	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}{\Delta} (l, \vec u ; \vec x , \vec f (

	l, (

	\vec u ; \vec x

	) \mode l 

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

	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:

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

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

	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.

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

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

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

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

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

	%

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

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

	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 ))

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

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

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

	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 )

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

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.