\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 $\smash(x,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.


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 symbols.
It also states the fundamental algebraic properties, i.e.\ $(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$.
\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.


\begin{definition}
[Quantifier hierarchy]
$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded.
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}


\anupam{Collection principles for prenexing? Otherwise need to add closure under sharply bounded quantifiers.}
\begin{definition}\label{def:polynomialinduction}
[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}


\begin{definition}\label{def:ariththeory}
Define the theory $\arith^i$ consisting of the following axioms:
\begin{itemize}
	\item $\basic$;
	\item $\cpind{\Sigma^\safe_i } $:
\end{itemize}
and an inference rule, called $\rais$, for closed formulas $\exists y^\normal . A$:
\[
 \dfrac{\forall \vec x^\normal . \exists  y^\safe .  A }{ \forall \vec x^\normal .\exists y^\normal . A}
\]
\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.}

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{\mathcal C}$, when $A \in \mathcal C$.
We will freely use this in place of polynomial induction whenever it is convenient.




\subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
%Todo: $+1$,  

We say that a function $f$ is represented by a formula $A_f$ if the arithmetic can prove (in the forthcoming proof system) a formula of the form $\forall ^{\normal} \vec u, \forall ^{\safe} x, \exists^{\safe}! y. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the result of $f(\vec u; \vec x)$.
 
Let us give a few examples of formulas representing basic functions.
\begin{itemize}
\item Projection $\pi_k^{m,n}$: $\forall^{\normal} u_1, \dots, u_m,  \forall^{\safe} x_{m+1}, \dots, x_{m+n}, \exists^{\safe} y. y=x_k$.
\item Successor $\succ{}$: $\forall^{\safe} x, \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$: 
$$\begin{array}{ll}
\forall^{\safe} x, y_{\epsilon}, y_0, y_1, \exists^{\safe} y. & ((x=\epsilon)\cand (y=y_{\epsilon})\\
                                                                                                   & \cor( \exists^{\safe}z.(x=\succ{0}z) \cand (y=y_0))\\
                                                                                                   & \cor( \exists^{\safe}z.(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^{\safe} z, \exists^{\normal} l\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)$  can be
defined by:
$$ \exists^{\safe} y.(\pref(k,x,y) \cand C(y,0,1,0)).$$
\end{itemize}




\subsection{A sequent calculus presentation}

 We denote sequence as $\Gamma \seqar \Delta$ where $\Gamma$, $\Delta$ are multi sets of formulas. The sequent calculus rules are displayed on Fig. \ref{fig:sequentcalculus} in Appendix~\ref{sect:app-sequent-calculus}.

%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 the purely logical calculus with certain non-logical rules and initial sequents corresponding to our theories $\arith^i$.
 For instance the axiom $\pind$ of Def. \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 $I=2$ and  in all cases, $t$ varies over arbitrary terms and the eigenvariable $a$ does not occur in the lower sequent of the $\pind$ rule.

Similarly the $\rais$ inference rule of Def. \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}
%\]
%}

The $\basic$ axioms are equivalent to the following nonlogical rules, that we will also designate by $\basic$:
\[
\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 calculus for $\arith^i$ is that of Fig. \ref{fig:sequentcalculus} extended with the $\basic$,  $\cpind{\Sigma^\safe_i } $ and $\rais$ nonlogical rules.
 
\todo{Present typed variable free-cut free form.}
\anupam{I cut-and-pasted the rest of this section into appendices to save space. Move things back gradually.}