\section{An arithmetic for the polynomial hierarchy}
Our base language is $\{ 0, \succ 0, \succ 1, \pred, + , \times, \smsh , |\cdot| , \leq \}$.


(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers)

Use base theory + sharply bounded quantifiers.

\anupam{Perhaps use prefix quantifier instead of sharply bounded (a la Ignatovic?), since plays nicer with sharply bounded lemma?}



\begin{definition}
[Quantifier hierarchy]
We define:
\begin{itemize}
	\item $\Sigma^\safe_0 = \Pi^\safe_0 $ = sharply bounded formulae. 
	\item (Increase with predicative quantifiers)
\end{itemize}	
\end{definition}


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


\begin{definition}
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:
\[
 \dfrac{\forall \vec x^\normal . \exists  y^\safe .  A }{ \forall \vec x^\normal .\exists y^\normal . A}
\]
\end{definition}
\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}

\begin{lemma}
[Sharply bounded lemma]
Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$.
Then the characteristic functions of $\forall u \prefix v . A(u,\vec u ; \vec x)$ and $\exists u \prefix v . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$.
\end{lemma}
\begin{proof}
	We give the $\forall$ case, the $\exists$ case being dual.
	The characteristic function $f(v , \vec u ; \vec x)$ is defined by predicative recursion on $v$ as:
	\[
	\begin{array}{rcl}
	f(0, \vec u ; \vec x) & \dfn & f_A (0 , \vec u ; \vec x) \\
	f(\succ i v , \vec u ; \vec x) & \dfn & \cond ( ; f_A (\succ i v, \vec u ; \vec x) , 0 , f(v , \vec u ; \vec x) )
	\end{array}
	\]
\end{proof}

Notice that $\prefix$ suffices to encode usual sharply bounded inequalities,
since $\forall u \leq |t| . A(u , \vec u ; \vec x) \ciff \forall u \prefix t . A(|u|, \vec u ; \vec x)$.


\subsection{Graphs of some basic functions}
Todo: $+1$,  

\subsection{Encoding sequences in the arithmetic}
\todo{}

\anupam{Assume we have a $\Sigma^\safe_1$ predicate $\beta(i,x,y)$, expressing that the $i$th element of the sequence $x$ is $y$, such that $\arith^1 \proves \forall i^\normal , x^\safe . \exists ! y^\safe . \beta (i,x,y)$.}


\subsection{A sequent calculus presentation}
\todo{Write out usual first-order sequent calculus}

\subsection{Free-cut free normal form of proofs}
\todo{State theorem, with references (Takeuti, Cook-Nguyen) and present the important corollaries for this work.}