\section{An arithmetic for the polynomial hierarchy}

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

\begin{definition}
Define the theory $\arith^i$ consisting of the following axioms:
\begin{itemize}
	\item $\basic$;
	\item $\cpind{\Sigma^\safe_i } $:
	\item $\forall \vec x \in \normal . \exists  y \in \safe .  A \cimp \forall \vec x \in \normal .\exists y\in \normal . A$ (raising) .
\end{itemize}
\end{definition}


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