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

\section{An arithmetic for the polynomial hierarchy}

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

The $\basic$ axioms are as follows:

\[

\begin{array}{l}

\safe (0) \\

\forall x^\safe . \safe (\succ{} x) \\

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

\end{array}

\]

\anupam{in fact, we use essentially the same language, so just take Buss' Basic axioms after proper typing. Should also add the symbol $\hlf{\cdot}$ for binary predecessor then we have the full language of bounded arithmetic.}

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

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

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