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

	%\begin{proof}

	%\end{proof}

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

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

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}

	Now, working in $\arith^i$, let $\vec u \in \normal , \vec x \in \safe$ and let us prove:

	\[

To some extent there is a distinction between various notions of `representability', namely between logics that \emph{type} terms computing functions of a given complexity class, and theories that prove the \emph{totality} or \emph{convergence} of programs computing functions in a given complexity class.

But a perhaps more important distinction is whether the constraints on the logic or theory are

 Bounded arithmetic is a deep and well-established field, and one of its advantages is its great versatility, allowing a characterization of a wide range of complexity classes, such as $\ptime$, the polynomial hierarchy $\ph$, $\pspace$, $\mathbf{NC}^i$ etc. 

 %It is also closely related to \textit{proof complexity}, the research field investigating the size of propositional proofs in various proof systems. Finally it is also employed for the research direction of \textit{bounded reverse mathematics}. 

%\anupam{Should add $+(;x,y)$ as a basic function (check satisfies polychecking lemma!), since otherwise not definable with safe input. Then define unary successor $\succ{} (;x)$ as $+(;x,\succ 1 0)$. }

\begin{example}

	[Some simple functions]

	\label{ex:simple-bc-fns}

	%\item $\bit(l;x)$ returns the $\mode l$th bit of $x$.

	\item We can define the function $\bit(l;x)$ which returns the $|l|$th least significant bit of $x$. For instance $\bit(11;1101)=0$.

	\begin{eqnarray*}

	\shorten(0;x) &=&x\\

	\shorten(\succ{i}l;x) &=&p(;\shorten(l;x))

	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|$ prefix of $x$, as follows:

	\begin{eqnarray*}

	\shorten(0;x) &=&x\\

	\end{eqnarray*}

	Then we define $\bit(l;x)$  as follows:

	$$\bit(l;x)=C(;\shorten(l;x),0,1).$$