\section{An arithmetic for the polynomial hierarchy}\label{sect:arithmetic}
%Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$. 
Our base language consists of constant and function symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|, \hlf{}.\}$ and predicate symbols 
 $\{\leq, \safe, \normal \}$. The function symbols are interpreted in the intuitive way, with $|x|$ denoting the length of $x$ seen as a binary string, and $x\smsh y$ denoting $2^{|x||y|}$, so a string of length $|x||y|+1$.
 We may write $\succ{0}(x)$ for $2\cdot x$, $\succ{1}(x)$ for $\succ{}(2\cdot x)$, and $\pred (x)$ for $\hlf{x}$, to better relate to the $\bc$ setting.
 
We consider formulas of classical first-order logic, over $\neg$, $\cand$, $\cor$, $\forall$, $\exists$, along with usual shorthands and abbreviations. 
%The formula $A \cimp B$ will be a notation for $\neg A \cor B$.
%We will also use as shorthand notations:
%$$ (s=t) = (s\leq t) \cand (t\leq s), \quad (s\neq t) = \neg(s=t).$$ 
\textit{Atomic formulas} formulas are of the form $s\leq t$, for terms $s,t$.
 We will assume, without loss of generality, that formulas are in \textit{De Morgan normal form}, that is to say that in formulas negation can only occur on atomic formulas, and that there is not any occurrence of a subformula of the form $\neg \neg A$.
 
 
 We write $\exists x^{N_i} . A$ or $\forall x^{N_i} . A$ for $\exists x . (N_i (x) \cand A)$ and $\forall x . (N_i (x) \cimp A)$ respectively. We refer to  $\exists x^{N_0}$,  $\forall x^{N_0}$ as \emph{safe} quantifiers.
 We also write $\exists x^\normal \leq |t| . A$ for $\exists x^\normal . ( x \leq |t| \cand A )$ and $\forall x^\normal \leq |t|. A $ for $\forall x^\normal. (x \leq |t| \cimp A )$. We refer to these as \emph{sharply bounded} quantifiers, as in bounded arithmetic.


The theories we introduce are directly inspired from bounded arithmetic, namely the theories $S^i_2$.
We include a similar set of axioms for direct comparison, although in our setting these are not minimal.
Indeed, $\#$ can be defined using induction in our setting.

The $\basic$ axioms of bounded arithmetic give the inductive definitions and interrelationships of the various function and predicate symbols.
It also states fundamental algebraic properties, e.g.\ $(0,\succ{ } )$ is a free algebra, and, for us, it will also give us certain `typing' information for our function symbols based on their $\bc$ specification, with safe inputs ranging over $\safe$ and normal ones over $\normal$.


Namely, in addition to usual axioms, our $\basic$ includes the following:\footnote{Later some of these will be redundant, for instance $\safe (u \times x) $ and $\safe (u \smsh v)$ are consequences of $\Sigma^\safe_i$-$\pind$, but $\safe (x + y)$ is not since both inputs are safe and so we cannot induct.}
\begin{enumerate}[(a)]
	\item\label{ax:a} $\forall u^\normal. \safe(u) $
	\item $\safe (0) $
	\item $\forall x^\safe . \safe (\succ{} x) $
	\item $\forall u^\safe .\safe(\hlf{u})$
	\item $\forall x^\safe, y^\safe . \safe(x+y)$
	\item $\forall u^\normal, x^\safe . \safe(u\times x) $
	\item $\forall u^\normal , v^\normal . \safe (u \smsh v)$
	\item\label{ax:h} $\forall u^\normal .\safe(|u|)$
\end{enumerate}
%\[
%\begin{array}{l}
%\forall u^\normal. \safe(u) \\
%\safe (0) \\
%\forall x^\safe . \safe (\succ{} x) \\
%\forall u^\safe .\safe(\hlf{u})
%\end{array}
%\qquad
%\begin{array}{l}
%\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(|x|)
%\end{array}
%\]
%\patrick{Actually I guess that we could replace the last one by $\forall x^\normal .\safe(|x|)$, as $|x|$ has smaller size as $x$? But I am not sure this would be needed anywhere. }

Notice in particular that we have $\normal \subseteq \safe$.
%
Apart from these, the remaining $\basic$ axioms mimic those of Buss in \cite{Buss86book}:
\begin{enumerate}[(1)]
	\item $\forall x^{\safe}, y^{\safe}.  (y\leq x\cimp  y \leq \succ{} x) $ \label{axiom1}
	\item $\forall x^{\safe}. x \neq \succ{} x$       \label{axiom2}
	\item $\forall x^{\safe}.0 \leq x$       \label{axiom3}
	\item $\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) $ \label{axiom4}
	\item $\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)$
	\item $\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)$  \label{axiom6}
	\item $\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)$
	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)$ \label{axiom<=transitivity}
	\item $|0|=0$
	\item $\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp  (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) $
	\item $|\succ{}0|=\succ{} 0$
	\item $\forall x^{\safe}, y^{\safe}.   (x\leq y \cimp   |x|\leq  |y|)$
	\item $\forall x^{\normal}, y^{\normal}.    |x\smsh y|=\succ{}( |x|\cdot  |y|)$
	\item $\forall y^{\normal}.    0 \smsh y=\succ{} 0$
	\item $\forall x^{\normal}.    (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)))$
	\item $\forall x^{\normal}, y^{\normal}.    x \smsh y = y \smsh x$
	\item $\forall x^{\normal}, y^{\normal}, z^{\normal}. (   |x|= |y| \cimp x\smsh z = y\smsh z)$
	\item $\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}.      (|x|= |u|+  |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))$
	\item $\forall x^{\safe}, y^{\safe}.      x\leq x+y$
	\item $\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))$
	\item $\forall x^{\safe}, y^{\safe}.     x+y=y+x$ \label{axiom21}
	\item $\forall x^{\safe}.       x+0=x$                    \label{axiom22}
	\item $\forall x^{\safe}, y^{\safe}.       x+\succ{}y=\succ{}(x+y)$ \label{axiom23}
	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}.      (x+y)+z=x+(y+z)$
	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. (    x+y \leq x+z \ciff y\leq z)$
	\item $\forall x^{\safe}       0\cdot x =0$
	%\item $\forall x^{\normal}, y^{\safe}.  x\cdot(\succ{}y)=(x\cdot y)+x$  \label{axiom27}  %% version with alternative sorting
	\item $\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x$  \label{axiom27}
          \item $\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x$
	\item $\forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)$ \label{axiom29}
	\item $\forall x^{\normal}, y^{\safe}, z^{\safe}.      (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))$
	\item $\forall x^{\normal}  .     (x\neq 0 \cimp  |x|=\succ{}(\hlf{x}))$
	\item $\forall x^{\safe}, y^{\safe}.   (  x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))$
\end{enumerate}


%$$
%%\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) \ciff \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{1}x|= \succ{}(|x|))) \\
%|\succ{}0|=\succ{} 0\\
%\forall x^{\safe}, y^{\safe}.   (x\leq y \cimp   |x|\leq  |y|)\\
%\forall x^{\normal}, y^{\normal}.    |x\smsh y|=\succ{}( |x|\cdot  |y|)\\
%\forall y^{\normal}.    0 \smsh y=\succ{} 0\\
%\forall x^{\normal}.    (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^{\normal}, y^{\normal}, z^{\normal}. (   |x|= |y| \cimp x\smsh z = y\smsh z)\\
%\forall x^{\normal}, u^{\normal}, v^{\normal}, 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 \ciff y\leq z)\\
%\forall x^{\safe}       0\cdot x =0\\
%\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x\\
%%\text{\anupam{check above normal/safe! Pretty sure should be other way around.}}\\
%\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 \ciff y\leq z))\\
%\forall x^{\normal}  .     (x\neq 0 \cimp  |x|=\succ{}(\hlf{x}))\\
%\forall x^{\safe}, y^{\safe}.   (  x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))
%\end{array}
%%\end{equation}
%$$
%







%\begin{definition}
%	[Basic theory]
%	The theory $\basic$ consists of the axioms from Appendix \ref{appendix:arithmetic}.
%	\end{definition}


%Notation: if $\vec t=t_0,\dots, t_k$, we will denote as $\safe(\vec t)$ the sequence of formulas $\safe(t_0),\dots, \safe(t_k)$. Similarly for $\normal(\vec t)$.
  
%\begin{definition}
%[Derived functions and notations]
%We write $1,2,3,\dots$ for the terms $\succ{} 0, \succ{} \succ{} 0, \succ{} \succ{} \succ{} 0 \dots$, and frequently omit the $\times$ symbol.
%We define the functions $\succ 0 x , \succ 1 x$ as $2 x$ and $2x +1$ respectively.
%
%Need $bit$, $\beta$ , $\pair{}{}{}$.
%\end{definition}
%
%(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers)
%
%Use base theory + sharply bounded quantifiers.

In addition to these axioms, our theories will contain forms of induction, defined below.

%\anupam{Collection principles for prenexing? Otherwise need to add closure under sharply bounded quantifiers.}


\begin{definition}
[Polynomial induction]
\label{def:polynomialinduction}
The \emph{polynomial induction} axiom schema, $\pind$, consists of the following axioms, for each formula $A(x)$:
\[
\left(
A(0) 
\cand (\forall x^{\normal} . ( A(x) \cimp A(\succ{0} x) ) )
\cand  (\forall x^{\normal} . ( A(x) \cimp A(\succ{1} x) ) ) 
\right)
\cimp  \forall x^{\normal} . A(x)
\]
For a class $\Xi$ of formulae, $\cax{\Xi}{\pind}$ denotes the set of $\pind$ axioms where $A(x) \in \Xi$. 

%We write $I\Xi$ to denote the theory consisting of $\basic$ and $\cax{\Xi}{\ind}$.
\end{definition}

We will introduce in fact a hierarchy of theories calibrated by the complexity of induction formulae, so we now introduce the appropriate quantifier hierarchy.

\begin{definition}
	[Quantifier hierarchy]
	$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded and where $\safe , \normal$ do not occur free.
	We define $\Sigma^\safe_{i+1}$ as the closure of $\Pi^\safe_i $ under $\cor, \cand $, safe existentials and sharply bounded quantifiers.
	We define $\Pi^\safe_{i+1}$ as the closure of $\Sigma^\safe_i $ under $\cor, \cand $, safe universals and sharply bounded quantifiers.
\end{definition}


Notice that the criterion that $\safe$ does not occur free is not a real restriction, since we can write $\safe (x)$ as $\exists y^\safe . y=x$.
The criterion is purely to give an appropriate definition of the hierarchy above.


\begin{definition}\label{def:ariththeory}
Define the theory $\arith^i$ consisting of the $\basic$ axioms, $\cpind{\Sigma^\safe_i } $,
%\begin{itemize}
%	\item $\basic$;
%	\item $\cpind{\Sigma^\safe_i } $:
%\end{itemize}
and a particular inference rule, called $\rais$, for closed formulas $\forall \vec x. \exists y. A$:
\[
 \dfrac{\proves \forall \vec x^\normal . \exists  y^\safe .  A }{ \proves \forall \vec x^\normal .\exists y^\normal . A}
\]
We will write $\arith^i \proves A$ if $A$ is a logical consequence of the axioms and rules of $\arith^i$, in the usual way.
\end{definition}
%\patrick{I think in the definition of  $\arith^i$ we should impose that the formulas considered are \textit{integer positive}, that is to say that the only negative occurrences of atoms $\safe(t)$, $\normal(t)$ are those occurring in $\forall^{\safe}$ and $\forall^{\normal}$.  Indeed I don't think this can be just proved to be a consequence of a kind of 'normal form' of proofs, as we had discussed (see sect 4.4)}
%
%\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}

%\anupam{Need vector $\vec y^\safe$?}

\begin{remark}
Notice that $\rais$ looks similar to the $K$ rule from the calculus for the modal logic $S4$ (which subsumes necessitation), and indeed we believe there is a way to present these results in such a framework.
However, the proof theory of first-order modal logics, in particular free-cut elimination results used for witnessing, is not sufficiently developed to carry out such an exposition.	
	\end{remark}


Let us consider some basic examples of theorems of our
\begin{example}
	[Some basic theorems]
	We give proofs of the following, that are sometimes included as basic axioms, in $\arith^1$:
	\begin{enumerate}[(i)]
		\item\label{item:i} $\forall x^\safe . 0 \neq \succ{} (x)$
		\item\label{item:ii} $\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) $
		\item\label{item:iii} $\forall u^\normal . (u = 0 \cor \exists y^\safe.  u = \succ{} v  ) $
		\item\label{item:iv} $\forall u^\normal ,x^\safe . u \cdot \succ{} x = u + ux$
	\end{enumerate}
%	\[
%	\begin{array}{l}
%	\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   )  \\        %% version 1: Anupam
%	%\forall u^\normal . (u = 0 \cor \exists v^\normal.\  u = \succ{} v  )  %%  version 2: Patrick
%	\forall u^\normal . (u = 0 \cor \exists y^\safe.  u = \succ{} v  )  \\        %% version 3: after discussion
%	\forall u^\normal ,x^\safe . u \cdot \succ{} x = u + ux
%	\end{array}
%	\]
%	\todo{Proof: Patrick? The final two should require PIND.}
	
%	\patrick{Actually statement 4 is nearly trivial from axiom 27 (for which I corrected the sorts). Maybe you meant something else?
%		\anupam{I actually changed those sorts from the submitted version: I really think axiom 27 should be $\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x$, i.e.\ with the recursion on the normal variable. That way we can do induction on it. Statement 4 is meant to state the recursive property for the safe argument, which we can prove by induction on the normal argument, $u$.}
%	
%	For statement 3 I replaced the quantifications $\safe$ by $\normal$, otherwise I don't know how to prove it. But I think we need the stronger statement with $\safe$, so probably we should add it as an additional axiom.}
%\anupam{Rather, I do not know how you would prove the current version: we cannot induct on $\exists v^\normal$ from axiom 27 as I state it. For the previous version I would just do induction on $u$ in $(u = 0 \cor \exists x^\safe.\  u = \succ{} x )$. }
	\end{example}
\begin{proof}
	For \eqref{item:i}, assume  $\succ{} (x)=0$ in order to derive a contradiction. From axiom \ref{axiom1} we deduce $x \leq x$, and so by transitivity (axiom \ref{axiom<=transitivity}) we have $x\leq 0$. So axiom \ref{axiom3} gives us $x=0$, and so $x=\succ{} (x)$. Finally with axiom  \ref{axiom2} we conclude with a contradiction.
	
	For \eqref{item:ii} assume $\succ{} x= \succ{} y$ and, in view of a contradiction, $x\neq y$. Let us apply axiom \ref{axiom6} and assume we are in the case where $x\leq y$ (the case $y\leq x$ is symmetric). By axiom \ref{axiom4}, using the assumption $x\neq y$ we deduce $\succ{} x \leq y$. So as $\succ{} x = \succ{} y$ we can derive that $\succ{} y \leq y$. So by using axiom \ref{axiom1} we obtain that $\succ{} y = y$, hence axiom \ref{axiom2} gives us a contradiction, so we are done.
	
	For \eqref{item:iii} we proceed by induction on $u$ on the formula %$A(u)= (u=0) \cup \exists^{\normal} v. u=\succ{} v$.
	$A(u)= (u=0) \cup \exists^{\safe} v. u=\succ{} v$. Note that this formula is in $\Sigma^{\safe}_1$, so we can do induction on it in  $\arith^1$. 
	The formula $A(0)$ obviously holds. Let us assume $A(u)$ and prove $A(\succ{0} u)$ (the case for $A(\succ{1} u)$ will be similar).  By $A(u)$ we deduce that either $u=0$, in which case we also have $\succ{0} u=0$, hence  $A(\succ{0} u)$ also holds, or there is a $y$ such that $u=\succ{} y$. In this latter case we have $\succ{0} u=2\cdot(\succ{} y)=2 v +2$ (by axiom \ref{axiom29}), hence have $\succ{0} u=\succ{} (\succ{} (2\cdot y))$, and so $A(\succ{0} u)$ holds.
	By induction we conclude that $\forall^{\normal} u. A(u)$ holds.
	
	 For \eqref{item:iv} let $u$ be in $\normal$ and $x$ in $\safe$, and try to prove $u\succ{} x=u+ux$. We have $\succ{} x=x+1$ by axioms \ref{axiom23} and \ref{axiom22} , so $u\succ{} x= u(x+1)$, so from axiom \ref{axiom29} we deduce $ u\succ{} x= u(x+1)=ux+u$, and by axiom \ref{axiom21} we conclude that $ u\succ{} x=u+ux$.	
\end{proof}
It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:
\begin{proposition}
	[Length induction]
	The axiom schema of formulae,
	\begin{equation}
	\label{eqn:lind}
	( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)
	\end{equation}
	for formulae $A \in \Sigma^\safe_i$
	is equivalent to $\cpind{\Sigma^\safe_i}$.
\end{proposition}
\begin{proof}
	Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.
	Then, by $\basic$, we have that $A(|a|) \cimp A(|2a|)$ and $A(|a|) \cimp A(|2a+1|)$ for each $a \in \normal$, whence we may conclude $\forall x. A(|x|)$ by polynomial induction on $A(|x|)$.
\end{proof}

Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\Xi}$, when $A \in \Xi$.
We will freely use this in place of polynomial induction whenever it is convenient.


\subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}

We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall \vec u^{\normal} , \forall  \vec x^{\safe}, \exists! y^{\safe}. A_f (\vec u , \vec x , y)$, such that $\Nat \models A_f (\vec u , \vec x , f(\vec u , \vec x))$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
We sometimes explicitly delimit variables as such when it is helpful, writing $A_f (\vec u ; \vec x , y)$.
 
Let us give a few examples for basic functions representable in $\arith^1$, wherein proofs of totality are routine:
\begin{itemize}
\item Projection $\pi_k^{m,n}$: $\forall u_1^{\normal} , \dots, u_m^{\normal} ,  \forall x_{m+1}^{\safe} , \dots, x^{\safe} _{m+n}, \exists y^{\safe} . y=x_k$ if $k\geq m+1$ (resp. $u_k$ if $k\leq m$).
%\item Successor $\succ{}$: $\forall x^{\safe} , \exists^{\safe} y. y=x+1.$. The formulas for the binary successors $\succ{0}$, $\succ{1}$ and the constant functions $\epsilon^k$ are defined in a similar way.
%\item Predecessor $p$:   $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$
\item Conditional $C$: 
$$
\forall x^{\safe} ,  y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. 
\left( 
\begin{array}{rl}
&\exists z^{\safe}.x=\succ{0}z \cand y=y_0 \\
\cor&  \exists z^{\safe}.x=\succ{1}z \cand y=y_1
\end{array}
\right)
$$
%$$\begin{array}{ll}
%\forall x^{\safe} ,  y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=0)\cand (y=y_0)\\
%                                                                                                   & \cor( \exists z^{\safe}.(x=\succ{0}z) \cand (y=y_0))\\
%                                                                                                   & \cor( \exists z^{\safe}.(x=\succ{1}z) \cand (y=y_1)))\
%\end{array}
%$$
%\item Addition:
%$\forall^{\safe} x, y,  \exists^{\safe} z. z=x+y$. 
\item Prefix:
  This is a predicate that we will need for technical reasons, in the completeness proof. The predicate $\pref(k,x,y)$ holds if the prefix of string $x$
  of length $k$ is $y$. It is defined as:
  $$\begin{array}{ll}
\exists z^{\safe} , \exists l^{\normal} \leq |x|. & (k+l= |x|\\
                                                                                                   & \cand \; |z|=l\\
                                                                                                   & \cand \; x=y\smsh(2,l)+z)
                                                                                                   \end{array}
$$
\item The following predicates will also be needed in proofs:

$\zerobit(x,k)$ (resp. $\onebit(x,k)$) holds iff the $k$th bit of $x$ is 0 (resp. 1). The predicate $\zerobit(x,k)$  for instance can be
defined by:
$$ \exists y^{\safe} .(\pref(k,x,y) \cand \exists z^{\safe} . y=\succ{0}z).$$
\end{itemize}

\subsection{A sequent calculus presentation}
\begin{figure}
	\[
	\small
	\hspace{-4em}
	\begin{array}{cccc}
	%\vlinf{\lefrul{\bot}}{}{p, \lnot{p} \seqar }{}
	%& \vlinf{\id}{}{p \seqar p}{}
	%& \vlinf{\rigrul{\bot}}{}{\seqar p, \lnot{p}}{}
	%& \vliinf{\cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta, A }{\Sigma, A \seqar \Pi}
	\vlinf{id}{}{\Gamma, p \seqar p, \Delta }{}
	& \vliinf{cut}{}{\Gamma, \Sigma \seqar \Delta, \Pi }{ \Gamma \seqar \Delta, A }{\Sigma, A \seqar \Pi}
	&	\vlinf{\lefrul{\neg}}{}{\Gamma, \neg A \seqar \Delta}{\Gamma \seqar A, \Delta}
	&
	
	\vlinf{\rigrul{\neg}}{}{\Gamma, \seqar \neg A, \Delta}{\Gamma, A \seqar  \Delta}
		\\
		
		\noalign{\bigskip}
		%\text{Structural:} & & & \\
		%\noalign{\bigskip}
		
		\vlinf{\lefrul{\wk}}{}{\Gamma, A \seqar \Delta}{\Gamma \seqar \Delta}
		&
		\vlinf{\lefrul{\cntr}}{}{\Gamma, A \seqar \Delta}{\Gamma, A, A \seqar \Delta}
		&
		\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, A }{\Gamma \seqar \Delta}
		&
		\vlinf{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta, A, A}
		\\
		\noalign{\bigskip}
		\vlinf{\lefrul{\exists}}{}{\Gamma, \exists x . A(x) \seqar \Delta}{\Gamma, A(a) \seqar \Delta}
		&
		\vlinf{\lefrul{\forall}}{}{\Gamma, \forall x. A(x) \seqar \Delta}{\Gamma, A(t) \seqar \Delta}
		&
		\vlinf{\rigrul{\exists}}{}{\Gamma \seqar \Delta, \exists x . A(x)}{ \Gamma \seqar \Delta, A(t)}
		&
		\vlinf{\rigrul{\forall}}{}{\Gamma \seqar \Delta, \forall x . A(x)}{ \Gamma \seqar \Delta, A(a) }
	\\
	\noalign{\bigskip}
	%\noalign{\bigskip}
	\vliinf{\lefrul{\cor}}{}{\Gamma, \Sigma, A \cor B \seqar \Delta, \Pi}{\Gamma , A \seqar \Delta}{\Sigma, B \seqar \Pi}
	&
	\vlinf{\lefrul{\cand}}{}{\Gamma, A\cand B \seqar \Delta}{\Gamma, A , B \seqar \Delta}
	&
	%\vlinf{\lefrul{\laand}}{}{\Gamma, A\laand B \seqar \Delta}{\Gamma, B \seqar \Delta}
	%\quad
	\vlinf{\rigrul{\cor}}{}{\Gamma \seqar \Delta, A \cor B}{\Gamma \seqar \Delta, A, B}
	&
	%\vlinf{\rigrul{\laor}}{}{\Gamma \seqar \Delta, A\laor B}{\Gamma \seqar \Delta, B}
	%\quad
	\vliinf{\rigrul{\cand}}{}{\Gamma, \Sigma \seqar \Delta, \Pi, A \cand B }{\Gamma \seqar \Delta, A}{\Sigma \seqar \Pi, B}
	%\noalign{\bigskip}
	% \vliinf{mix}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta}{\Sigma \seqar \Pi} &&&
	\end{array}
	\]
	\caption{Sequent calculus rules, where $p$ is atomic, $i \in \{ 1,2 \}$, $t$ is a term and the eigenvariable $a$ does not occur free in $\Gamma$ or $\Delta$.}\label{fig:sequentcalculus}
\end{figure}

In order to carry out witness extraction for proofs of $\arith^i$, it will be useful to work with a \emph{sequent calculus} representation of proofs.
Such systems exhibit strong normal forms, notably `free-cut free' proofs, and so are widely used for the `witness function method' for extracting programs from proofs \cite{Buss86book,Buss98:intro-proof-theory}.
We state the required technical material here only briefly, due to space constraints.

A \emph{sequent} is an expression $\Gamma \seqar \Delta$ where $\Gamma$ and $\Delta$ are multisets of formulas. 
The inference rules of the sequent calculus $\LK$ are displayed in Fig.~\ref{fig:sequentcalculus}.
Of course, we have the following:
\begin{proposition}
	$A$ is a first-order theorem if and only if there is an $\LK$ proof of $\seqar A$.
\end{proposition}

%We consider \emph{systems} of `nonlogical' rules extending this sequent calculus, which we write as follows,
% \[
% \begin{array}{cc}
%    \vlinf{(R)}{}{ \Gamma , \Sigma' \seqar \Delta' , \Pi  }{ \{\Gamma , \Sigma_i \seqar \Delta_i , \Pi \}_{i \in I} }
%\end{array}
%\]
% where, in each rule $(R)$, $I$ is a finite possibly empty set (indicating the number of premises) and we assume the following conditions and terminology:
% \begin{enumerate}
% \item In $(R)$ the formulas of $\Sigma', \Delta'$  are called \textit{principal}, those of $\Sigma_i, \Delta_i$ are called \textit{active}, and those of   
%$ \Gamma,  \Pi$ are called \textit{context formulas}. 
%\item Each rule $(R)$ comes with a list $a_1$, \dots, $a_k$ of eigenvariables such that each $a_j$ appears in exactly one $\Sigma_i, \Delta_i$ (so in some active formulas of exactly one premise)  and does not appear in  $\Sigma', \Delta'$ or $ \Gamma,  \Pi$.
%    \item A system $\mathcal{S}$ of rules must be closed under substitutions of free variables by terms (where these substitutions do not contain the eigenvariables $a_j$ in their domain or codomain).  
%   \end{enumerate}
% 
%%The distinction between modal and nonmodal formulae in $(R)$ induces condition 1
% Conditions 2 and 3 are standard requirements for nonlogical rules, independently of the logical setting, cf.\ \cite{Beckmann11}. Condition 2 reflects the intuitive idea that, in our nonlogical rules, we often need a notion of \textit{bound} variables in the active formulas (typically for induction rules), for which we rely on eigenvariables. Condition 3 is needed for our proof system to admit elimination of cuts on quantified formulas.
%
%%\begin{definition}
%%[Polynomial induction]
%%The \emph{polynomial induction} axiom schema, $\pind$, consists of the following axioms,
%%\[
%%A(0) 
%%\cimp (\forall x^{\normal} . ( A(x) \cimp A(\succ{0} x) ) )
%%\cimp  (\forall x^{\normal} . ( A(x) \cimp A(\succ{1} x) ) ) 
%%\cimp  \forall x^{\normal} . A(x)
%%\]
%%for each formula $A(x)$.
%%
%%For a class $\Xi$ of formulae, $\cax{\Xi}{\pind}$ denotes the set of induction axioms when $A(x) \in \Xi$. 
%%
%%We write $I\Xi$ to denote the theory consisting of $\basic$ and $\cax{\Xi}{\ind}$.
%%\end{definition}
%
%As an example any axiom can be represented by such a nonlogical rule $(R)$, with no premise ($I=\emptyset$), $\Delta'$ equal to the axiom and $\Gamma=\Sigma'=\Pi$.

We extend this purely logical calculus with certain non-logical rules and initial sequents corresponding to our theories $\arith^i$.
 For instance the axiom $\pind$ of Dfn.~\ref{def:polynomialinduction} is represented by the following rule:
\begin{equation}
\label{eqn:ind-rule}
\small
\vliinf{\pind}{}{ \normal(t) , \Gamma , A(0) \seqar A(t), \Delta }{ \normal(a) , \Gamma, A(a) \seqar A(\succ{0} a) , \Delta }{ \normal(a) , \Gamma, A(a) \seqar A(\succ{1} a) , \Delta  }
\end{equation}
where $t$ varies over terms and the eigenvariable $a$ does not occur in the lower sequent.
%
Similarly the $\rais$ inference rule of Dfn.~\ref{def:ariththeory} is represented by the nonlogical rule,
 \[
 \begin{array}{cc}
    \vlinf{\rais}{}{  \normal(t_1), \dots, \normal(t_k) \seqar  \exists  y^\normal .  A }{  \normal(t_1), \dots, \normal(t_k) \seqar \exists  y^\safe .  A}
\end{array}
\]
%
%\patrick{In fact, I think we rather need the following nonlogical rule, which implies the previous one but is I guess more general:
%\[
% \begin{array}{cc}
%    \vlinf{\rais}{}{  \normal(t_1), \dots, \normal(t_k) \seqar  \normal(t) }{  \normal(t_1), \dots, \normal(t_k) \seqar \safe(t)}
%\end{array}
%\]
%}
%
$\basic$ axioms are represented by designated initial sequents.
For instance here are some initial sequents corresponding to some of the $\basic$ axioms:
\[
\small
\begin{array}{l}
\begin{array}{cccc}
\vlinf{}{}{\seqar \safe (0)}{}&
\vlinf{}{}{\safe(t) \seqar \safe(\succ{} t)}{}&
\vlinf{}{}{ \safe (t)   \seqar 0 \neq \succ{} t}{} &
\vlinf{}{}{\safe (s) , \safe (t)  , \succ{} s = \succ{} t\seqar s = t }{}\\
\end{array}
\\
\vlinf{}{}{\safe (t) \seqar t = 0 \cor \exists y^\safe . t = \succ{} y  }{}
\qquad
\vlinf{}{}{\safe(s), \safe(t) \seqar \safe(s+t) }{}\\
\vlinf{}{}{\normal (s), \safe(t) \seqar \safe(s \times t)  }{}
\qquad
\vlinf{}{}{\normal (s), \normal(t) \seqar \safe(s \smsh t)  }{}\\
\vlinf{}{}{\normal(t) \seqar \safe(t)  }{}
\end{array}
\]

The sequent system for $\arith^i$ extends $\LK$ by the $\basic$,  $\cpind{\Sigma^\safe_i } $ and $\rais$ rules.
 Naturally, by completeness, we have that $\arith^i \proves A$ if and only if there is a sequent proof of $\seqar A$ in the corresponding system.
 In fact, by \emph{free-cut elimination} results \cite{Takeuti87,Cook:2010:LFP:1734064} we may actually say something much stronger.
 
 Let us say that a sorting $(\vec u ; \vec x)$ of the variables $\vec u , \vec x$ is \emph{compatible} with a formula $A$ if each variable of $\vec x$ occurs hereditarily safe with respect to the $\bc$-typing of terms, i.e.\ never under $\smsh, |\cdot|$ and to the right of $\times$.
 
\begin{theorem}
	[Typed variable normal form]
	\label{thm:normal-form}
	If $\arith^i\proves  A$ then there is a $\arith^i$ sequent proof $\pi$ of $A$ such that each line has the form:
	\[
	\normal(\vec u), \safe (\vec x), \Gamma \seqar \Delta
	\]
	where $\Gamma \seqar \Delta$ contains only $\Sigma^\safe_i$ formulae for which the sorting $(\vec u ;\vec x)$ is compatible.
\end{theorem}

Strictly speaking, we must alter some of the sequent rules a little to arrive at this normal form. For instance the $\pind$ rule would have $\normal(\vec u)$ in its lower sequent rather than $\normal (t(\vec u))$:
\[
\small
\vliinf{}{}{ \normal(\vec u) , \safe (\vec x) , \Gamma , A(0) \seqar A(t(\vec u)), \Delta }{ \normal(u), \normal (\vec u) , \safe (\vec x) , \Gamma, A(u) \seqar A(\succ{0} u) , \Delta }{ \normal(u) ,, \normal(\vec u ) , \safe (\vec x) , \Gamma, A(u) \seqar A(\succ{1} u) , \Delta  }
\] 
Notice that $\normal(t(\vec u))$ is a consequence of $\normal (\vec u)$ already in $\basic$, due to the axioms \eqref{ax:a}-\eqref{ax:h}.
That the variables of $t$ can be assumed to occur already in the premisses is due to weakening.
Indeed, the proof of this result relies on a heavy use of the structural rules, contraction and weakening, to ensure that we always have a complete and compatible sorting of variables on the LHS of a sequent. This is similar to what is done in \cite{OstrinWainer05} where they use a $G3$ style calculus to manage such structural manipulations.

As we mentioned, the fact that only $\Sigma^\safe_i$ formulae occur is due to the free-cut elimination result for first-order calculi \cite{Takeuti87,Cook:2010:LFP:1734064}, which gives a form of proof where every $\cut$ step has one of its cut formulae `immediately' below a non-logical step. Again, we have to adapt the $\rais$ rule a little to achieve our result, due to the fact that it has a $\exists x^\normal$ in its lower sequent. For this we consider a merge of $\rais$ and $\cut$, which allows us to directly cut the upper sequent of $\rais$ against a sequent of the form $\normal(u), A(u), \Gamma \seqar \Delta$:
\[
\vliinf{\rais\cut}{}{\normal (\vec u) , \Gamma \seqar \Delta}{\normal (\vec u) \seqar \exists x^\safe . A(x)}{\normal (u) , A(u) , \Gamma \seqar \Delta}
\]

Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers \cite{Buss86book}, although we use ones that satisfy the aforementioned constraints. For instance, we include the following rules, from which the remaining ones are similar:
\[
\vlinf{\rigrul{\forall}}{}{ \normal(\vec u) , \safe (\vec x), \Gamma \seqar \Delta , \forall x^\safe . A(x)}{\normal(\vec u ) , \safe (\vec x), \safe (x) , \Gamma \seqar \Delta, A(x)}
\quad
\vlinf{\rigrul{\exists}}{}{\normal(\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x^\safe . A(x)}{ \normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A(t) }
\]
\[
\vlinf{\lefrul{|\forall|}}{}{\normal (\vec u ) , \safe (\vec x) , s(\vec u) \leq |t(\vec u)| , \forall u^\normal \leq |t(\vec u)| . A(u) , \Gamma \seqar \Delta }{\normal (\vec u ) , \safe (\vec x) , A(s(\vec u)  ) , \Gamma \seqar \Delta  }
\]
with the usual side conditions and where, in $\rigrul{\exists}$, $(\vec u ; \vec x)$ is compatible with $t$.
