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

\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 $\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 $\forall u^\normal .\safe(|x|)$

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

%\]

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

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

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

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

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

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

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

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

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

	\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^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x$

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

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

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

\begin{example}

	[Some basic theorems]

	We give proofs of the following, that are sometimes included as basic axioms, in $\arith^1$:

	\[

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

	\forall u^\normal ,x^\safe . u \succ{} x = u + ux

	\end{array}

	\]

	\todo{Proof: Patrick? The final two should require PIND.}

\end{example}

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))$. The latter is a consequence of the former already in $\basic$.

The proof of this result also 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$.

Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers, 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$.