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

\section{An arithmetic for the polynomial hierarchy}

Our base language is $\{ 0, \succ 0, \succ 1, \pred, + , \times, \smsh , |\cdot| , \leq \}$.

The $\basic$ axioms are as follows:

\[

\begin{array}{l}

\safe (0) \\

\succ 0 = 0 \\

\safe (x) \cimp \safe (\succ i x) \\

\end{array}

\]

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