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

	\begin{proof}

	Let $A(x)$ be a  $\Sigma^\safe_{i-1}$ formula, with $x$ in $\safe$. We define the formula $B(a,b,c)$ as:

	$$ \forall x^{\safe}. (x < |a| \moins b \cimp \zerobit(x,c)) \cand \forall y^{\safe}<c. \neg A(y) \cand \exists y^{\safe} < 2^{|a|\moins b}.A(c+y)$$

	where $a$ is in $\normal$, $b$ in $\normal$ and $c$ in $\safe$.  $B(a,b,c)$ is in $\Sigma^\safe_{i}$.

	The intuitive idea of the proof is to observe that, if $A(a)$ is true for $a\neq 0$, then  $\exists x^{\safe}\leq a. B(a,b,x)$ holds for $b=0$, and to try to prove it for $b=|a|$, by using a length induction on $b$.

	First, one can prove:

	$$ (A(a) \cand a \neq 0) \cimp B(a,0,0).$$ 

	And thus:

	$$ (A(a) \cand a \neq 0) \cimp \exists x^{\safe}\leq a .B(a,0,x).$$ 

	We then can check that the two following statements are provable:

	$$

	\begin{array}{rcl}

	(b<|a| \cand B(a,b,c)\cand \exists y^{\safe}<2^{|a| \moins (b+1)}.A(c+y)) &\cimp& B(a,\succ{} b,c)\\

	(b<|a| \cand B(a,b,c)\cand \forall y^{\safe}<2^{|a| \moins(b+1)}.  A(c+y)) &\cimp & B(a,\succ{} b, c+2^{|a| \moins (b+1)})

        \end{array}

$$

Moreover we have: $A(a) \cand B(a,b,c) \cimp c\leq a$.

From these three statements we deduce:

$$(A(a) \cand a \neq 0 \cand b<|a| \cand \exists x^{\safe} \leq a. B(a,b,x)) \cimp \exists x^{\safe } \leq a.B(a,\succ{} b,x).$$

The formula $\exists x\leq a. B(a,b,c)$ is in $\Sigma^{\safe}_{i}$, so by $\Sigma^{\safe}_{i}$-LIND on the formula $\exists x\leq a. B(a,b,c)$, with the variable $b$ which is in $\normal$,  we obtain:

$$(A(a) \cand a \neq 0 ) \cimp \exists x^{\safe } \leq a.B(a,|a|,x).$$

\patrick{Anupam, is it a valid instance of LIND? I think it is.}

But $B(a,|a|,x)$ implies $(\forall y^{\safe}<x. \neg A(y))\cand A(x)$, so we have proven:

$$(A(a) \cand a \neq 0 ) \cimp (\exists x^{\safe } \leq a. (\forall y^{\safe}<x. \neg A(y))\cand A(x))$$

which is the $\Sigma_{i-1}^{\safe}$ axiom for $A$.

	\end{proof}

%	\patrick{Examining it superficially, I think indeed the proof of Buss can be adapted to our setting. But we should probably look again at that with more scrutiny.}