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

\section{An arithmetic for the polynomial hierarchy}\label{appendix:arithmetic}

We give here the  list of remaining  axioms of $\basic$, which are directly inspired by the $\basic$ theory of Buss's bounded arithmetic \cite{Buss86book}:

%$\succ{0}(x)$ stand for $2\cdot x$ and $\succ{1}(x)$ stand for $\succ{}(2\cdot x)$,

 \[

 \begin{array}{l}

 \safe (0) \\

 \forall x^\safe . \safe (\succ{} x) \\

 \forall x^\safe . 0 \neq \succ{} (x) \\

 \forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\

 \forall x^\safe . (x = 0 \cor \exists y^\safe.\  x = \succ{} y   )\\

 \forall x^\safe, y^\safe . \safe(x+y)\\

 \forall u^\normal, x^\safe . \safe(u\times x) \\

 \forall u^\normal , v^\normal . \safe (u \smsh v)\\

 \forall u^\normal \safe(u) \\

 \forall u^\safe \safe(\hlf{u})\\

 \forall u^\normal \safe(|x|)

 \end{array}

 \]

$$

%\begin{equation}

\begin{array}{l}

 \forall x^{\safe}, y^{\safe}.  (y\leq x) \cimp (y \leq \succ{} x) \\

\forall x^{\safe}. x \neq \succ{} x\\

 \forall x^{\safe}.0 \leq x\\

 \forall x^{\safe}, y^{\safe}.(x\leq y \cand x \neq y) \leftrightarrow \succ{} x \leq y\\

\forall x^{\safe}. x\neq 0 \cimp \succ{0}x \neq 0\\

\forall x^{\safe}, y^{\safe}. y\leq x \cor x \leq y\\

\forall x^{\safe}, y^{\safe}. x\leq y \cand y\leq x \cimp x=y\\

\forall x^{\safe}, y^{\safe}, z^{\safe}. x\leq y \cand y\leq z \cimp x\leq z\\

  |0|=0\\

  \forall x^{\safe}, y^{\safe}.x\neq 0 \cimp  |\succ{0}x|=\succ{}( |x|) \cand |\succ{0}x|= \succ{}(|x|) \\

   |\succ{}0|=\succ{} 0\\

\forall x^{\safe}, y^{\safe}.   x\leq y \cimp   |x|\leq  |y|\\

\forall x^{\safe}, y^{\normal}.    |x\smsh y|=\succ{}( |x|\cdot  |y|)\\

\forall y^{\normal}.    0 \smsh y=\succ{} 0\\

\forall x^{\safe}.    x\neq 0 \cimp 1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)\\

\forall x^{\normal}, y^{\normal}.    x \smsh y = y \smsh x\\

  \forall x^{\safe}, y^{\safe}, z^{\normal}.    |x|= |y| \cimp x\smsh z = y\smsh z\\

  \forall x^{\safe}, u^{\safe}, v^{\safe}, y^{\normal}.      |x|= |u|+  |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y)\\

  \forall x^{\safe}, y^{\safe}.      x\leq x+y\\

 \forall x^{\safe}, y^{\safe}.       x\leq y \cand x\neq y \cimp \succ{}(\succ{0}x) \leq \succ{0}y \cand  \succ{}(\succ{0}x) \neq \succ{0}y\\

   \forall x^{\safe}, y^{\safe}.     x+y=y+x\\

 \forall x^{\safe}.       x+0=x\\

 \forall x^{\safe}, y^{\safe}.       x+\succ{}y=\succ{}(x+y)\\

  \forall x^{\safe}, y^{\safe}, z^{\safe}.      (x+y)+z=x+(y+z)\\

   \forall x^{\safe}, y^{\safe}, z^{\safe}.     x+y \leq x+z \leftrightarrow y\leq z\\

 \forall x^{\normal}       x\cdot 0=0\\

      \forall x^{\normal}, y^{\safe}.  x\cdot(\succ{}y)=(x\cdot y)+x\\

       \forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x\\

      \forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)\\

  \forall x^{\normal}, y^{\safe}, z^{\safe}.      x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \leftrightarrow y\leq z)\\

 \forall x^{\normal}       x\neq 0 \cimp  |x|=\succ{}(\hlf{x})\\

   \forall x^{\safe}, y^{\normal}.     x= \hlf{y} \leftrightarrow (\succ{0}x=y \cor \succ{}(\succ{0}x)=y)

 \end{array}

%\end{equation}

$$