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

PVBC+FCA+ safe induction characterises PH?

We differ slightly from Bellantoni's theory, using  a mismatch of pvbc and qpvbc.

This is for simplicity, since 

\subsection{Base theory}

Let us begin with a variation of the base theory of $\pvbci{(0)}$.

	[Basic theory]

	We have two types/sorts: $\normal$ (normal) and $\safe$ (safe).

	Our language consists of the following:

	\begin{itemize}

		\item Normal and safe variables $x^\normal_i , x^\safe_i$. (sometimes write $u$, $x$ , or $\vec u; \vec x$ without superscripts).

%		\item Constant symbol $0^\safe$.

%		\item Function symbols $\succ{i}^{\safe \to \safe}$, for $i = 0,1$. (Simply written $\succ i^\safe (;x)$.

		\item (all initial symbols from BC with their natural typing, plus a recursion scheme. Have the defining axioms too.)

		\item The following interrelations between safe and normal terms:

		\begin{itemize}

			\item For each normal variable $x^\normal$ a safe variable $x^{\normal\safe}$.

			\item For each normal function symbol $f^\normal$ a safe function symbol $f^{\normal\safe}$.

			\item For each normal term $t = f^\normal (\vec s ; \vec t)$, we define $t^\safe$ as $f^{\normal\safe} (\vec s ; \vec t)$, and if $t$ is $x^\normal$ then $t^\safe$ as $x^{\normal\safe}$.

			\item We have the axioms $t^\safe = t$.

		\end{itemize}

		\item We have function symbols for the characteristic functions of each quantifier-free predicate. I.e.,

		\[

		f_A (\vec u ; \vec x) = 1

		\quad \ciff \quad

		A(\vec u ; \vec x)

		\]

		where $A$ is quantifier-free. (this is just $\wit{}{}$ for q.f.\ formulae.)

		(maybe use $\chi[A]$ for characteristic, to avoid subscripts)

		\item Open induction, i.e.\ quantifier-free induction, on normal variables:

		\[

		\forall \vec u ; \vec x.

		(A(0) \cand \forall u^\normal . ( A(u) \cimp  A(\succ 0 u ) \cand \forall u^\normal . ( A(u) \cimp  A(\succ 1 u ) ))

		\cimp \forall u^\normal . A( u ))

		\]

		where $\vec u ; \vec x $ are all the free variables of $A(0)$.

	\end{itemize}

The following was essentially proved by Bellantoni in his thesis:

\begin{theorem}

	[Bellantoni]

	$\pvbci{0}$ proves the totality of just the polynomial-time functions.

\end{theorem}

\nb{Notice that induction can be assumed to be simply functional, due to comprehension function symbols. This is more in the spirit of, say, 2nd order subsystems of arithmetic, like in reverse mathematics.}

\anupam{Hold on, the above should be fairly immediate, the interesting result is for $\pvbci 1$, which we should perhaps state later.}

\subsection{Extensions to theories for the polynomial hierarchy}

We now will associate a rank to new function symbols based on the complexity of formulae they characterise.

\anupam{Ranks are necessary since we do not have sharply bounded quantifiers to reason about sequences. Check what Krajicek does, probably has the latter.}

\begin{definition}

[Quantifier hierarchy and functional comprehension]

We mutually define the \emph{safe arithmetical hierarchy} and functions of rank $i$ as follows:

	\begin{itemize}

		\item All functions from the basic theory have \emph{rank} 0.

		\item $\Sigma^\safe_0 = \Pi^\safe_0$ is the set of quantifier-free formulae with just functions symbols of rank $0$.

		\item The functions symbols of rank $i$ are the characteristic functions of $\Sigma^\safe_i$ formulae.

		\item $\Sigma^\safe_{i+1}$ is the least class containing:

		\begin{itemize}

			\item $\Pi^\safe_i$.

			\item Atomic formulae $s=t$ where $s$ and $t$ contain only function symbols of rank $\leq i+1$.

			\item Closed under $\cor , \cand , \exists^\safe$.

		\end{itemize}

		\item $\Pi^\safe_{i+1} $ is...

	\end{itemize}

\end{definition}

\anupam{check the parameters/subscripts above! Aim for:

	rank = $\mu$ nesting = quant alt = level - 1

	}

Over the next two sections we will show that the provably total functions of $\pvbci i+1$ are just 

	If $\pvbci {i+1} \proves \forall \vec u^\normal , \vec x^\sigma . \exists \vec y^\sigma. A(\vec u , \vec x , \vec y)$, then there are rank $i $ functions $\vec f (\vec u ; \vec x)$ such that $\pvbci {i+1} \proves\forall \vec u^\normal , \vec x^\sigma . A(\vec u , \vec x , \vec f (\vec u ; \vec x) )  $.

\begin{corollary}

The provably total functions of $\pvbci i+1$ are in $\fphi i$.

\end{corollary}

Here we show that every $\mubci{i}$ function is definable in $\pvbci {i+1}$:

\begin{theorem}

	Every $\mubci i$ function is definable in $\pvbci {i+1}$.

\end{theorem}

\anupam{This should be simple, right?}

\begin{theorem}

\end{theorem}

\subsection{Delineating levels using function ranks}

\subsection{A second-order theory}

From here we can rather simply define a theory complete for PH.

However, delineating the levels is a little cumbersome, due to the formal necessity of infinitely many ranks.

\begin{definition}

	[Axioms]

	The \emph{functional comprehension} schema is the following:

	\[

	\exists f . \forall \vec u; \vec x . ( \exists y^\safe . A(\vec u ; \vec x , y) \ciff A(\vec u ; \vec x , f(\vec u ; \vec x) )

	\]

	(can parametrise by which $A$ permitted)

	The \emph{recursion} schema is:

	\[

	\forall g , h_0 , h_1 . \exists f . \forall u , \vec u ; \vec x .

	\left(

	\begin{array}{rl}

	& f(0 , \vec u ; \vec x) = g(\vec u ; \vec x) \\

	\cand & f(\succ 0 u , \vec u ; \vec x) = h_0 (u , \vec u ; \vec x , f(u , \vec u ; \vec x)) \\

	\cand & f(\succ 1 u , \vec u ; \vec x) = h_1 (u , \vec u ; \vec x , f(u , \vec u ; \vec x)) 

	\end{array}

	\right)

	\]

	(should be well typed. Cannot avoid due to sequentiality problem.)

	\end{definition}

	\anupam{Original PV has explicit recursion symbols. Also, Krajicek's PVi has explicit symbols for the characteristic functions of each $\Sigma^b_i$ predicate.}