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

\section{An extension of Bellantoni's theory PV for PH}

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

\begin{definition}

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

\end{definition}

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

	}

\nb{Wait, check: do we want characteristic functions or functional-comprehension functions? Compare with Krajicek.}

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

\subsection{Soundness}

We show that provably total functions of $\pvbci i$ are in $\fphi i$.

The following is our main result:

\begin{theorem}

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

\end{theorem}

\begin{corollary}

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

\end{corollary}

\begin{definition}

	[Witness predicate]

	The \emph{witness predicate} is a $\mubci{}$ program $\wit{\vec a}{A}$, parametrised by variables $\vec a$ and a formula $A$ whose free variables are amongst $\vec a$, defined as follows.

	If $A$ is a $\Pi_{i}$ formula then:

	\[

	\begin{array}{rcl}

	\wit{\vec u; \vec x}{s=t} (\vec u ; \vec x, w) & \dfn & =(;s,t) \\

	\smallskip

	\wit{\vec u; \vec x}{s\neq t} (\vec u ; \vec x, w) & \dfn & \neg (;=(;s,t)) \\

	\smallskip

	\wit{\vec u ; \vec x}{A\cor B} (\vec u ; \vec x , w) & \dfn & \cor (; \wit{\vec u , \vec x}{A} (\vec u ; \vec x , w), \wit{\vec u , \vec x}{B} (\vec u ;\vec x, w) ) \\

	\smallskip

	\wit{\vec u ; \vec x}{A\cand B} (\vec u ; \vec x , w) & \dfn & \cand(; \wit{\vec u , \vec x}{A} (\vec u ; \vec x , w), \wit{\vec u , \vec x}{B} (\vec u ;\vec x, w) ) \\

	\smallskip

	\wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (\vec u ;\vec x,  w) & \dfn & \begin{cases}

	1 & \exists x^\safe . \wit{\vec u; \vec x, x }{A(x)} (\vec u ;\vec x , x, w) = 1 \\

	0 & \text{otherwise} 

	\end{cases} \\

	\smallskip

	\wit{\vec u; \vec x}{\forall x^\safe . A(x)} (\vec u ;\vec x , w) & \dfn & 

	\begin{cases}

	0 & \exists x^\sigma. \wit{\vec u ; \vec x , x}{ A(x)} (\vec u; \vec x , x) = 0 \\

	1 & \text{otherwise}

	\end{cases}

	\end{array}

	\]

	We now define $\Wit{\vec a}{A}$ for a $\Sigma_{i+1}$-formula $A$ with free variables amongst $\vec a$.

	\[

	\begin{array}{rcl}

	\Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , w) & \dfn & \wit{\vec u ; \vec x}{A} (\vec u ; \vec x)  \text{ if $A$ is $\Pi_i$} \\

	\smallskip

	\Wit{\vec u ; \vec x}{A \cor B} (\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cor ( ; \Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (\vec u ; \vec x , \vec w^B)  )  \\

	\smallskip

	\Wit{\vec u ; \vec x}{A \cand B} (\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cand ( ; \Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (\vec u ; \vec x , \vec w^B)  )  \\

	\smallskip

	\Wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (\vec u ; \vec x , \vec w , w) & \dfn & \Wit{\vec u ; \vec x , x}{A(x)} ( \vec u ; \vec x , w , \vec w )

	\end{array}

	\]

\end{definition}

\nb{use (de)pairing to make sure only $i$ $\mu$s are used to express a $\Pi_i$ predicate.}

\begin{proposition}

	For $\Sigma_{i+1}$ formulae $A$, $\Wit{\vec u ; \vec x}{A}$ is a $\mubci{i} $ program.

\end{proposition}

\nb{In fact, need that $\wit{}{}$ is $\mubci{i}$ and $\Wit{}{}$ and the witness functions $\vec f$ are $\bc (\wit{}{})$}

Before proving the main theorem, we will need the following `witnessing lemma':

\begin{lemma}

	If $\pvbci{i+1} $ proves a $\Sigma^\safe_{i+1}$-sequent $\Gamma \seqar \Delta$ with free variables $\vec u^\normal , \vec x^\safe$ then there are $\mubci {i}$ functions $\vec f$ such that 

	\[

	\pvbci {i+1} \proves \Wit{\vec u , \vec x}{\bigwedge \Gamma} (\vec u ; \vec x , \vec w) \cimp \Wit{\vec u  , \vec x}{\bigvee \Delta } (\vec u ; \vec x, \vec f (\vec u ; \vec x , \vec w) )

	\]

	(we simply write $\Wit{\vec u ; \vec x}{A}(\vec u ; \vec x , \vec w)$, instead of $\Wit{\vec u ; \vec x}{A}(\vec u ; \vec x , \vec w) =1 $.

\end{lemma}

\begin{proof}

	By induction on the size of a $\pvbci{i+1} $ proof. 

	Interesting steps below:

	\begin{itemize}

		\item $\neg$-right. (Can assume only applies to atomic formulae, and so no effect.)

		\item $\exists$-right.

		\[

		\dfrac{\Gamma \seqar \Delta , A(t^\safe )}{ \Gamma \seqar \Delta, \exists x^\safe . A(x) }

		\]

		By the inductive hypothesis, have functions $\vec f(\vec u ; \vec x), \vec g (\vec u ; \vec x)$ such that,

		\[

		\pvbci{i+1} \proves 

		\Wit{\vec u ; \vec x}{\bigwedge \Gamma } (\vec u ; \vec x , \vec w)

		\cimp

		\left(

		\Wit{\vec u ; \vec x}{\bigvee \Delta} (\vec u ; \vec x , \vec f (\vec u ; \vec x , \vec w) )

		\cor

		\Wit{\vec u ; \vec x}{A(t)} (\vec u ; \vec x , \vec g (\vec u ; \vec x , \vec w))

		\right)

		\]

		(just use $t$ as one of the witness functions)

		\item $\forall$-right. (Must be a $\Pi_i$ formula, so forget witness and compute $\wit{}{}$)

		\item Contraction-right:

		\[

		\dfrac{\Gamma  \seqar \Delta , A ,A}{\Gamma \seqar \Delta, A}

		\]

		By infuctive hypothesis have functions $\vec f, \vec g^1 , \vec g^2$ such that:

		\[

		todo

		\]

		(just use conditional with a call to $\Wit{}{}$)

		\item induction

		\[

		\dfrac{\{\Gamma , A(a) \seqar A(s_i a) , \Delta\}_{i=0,1} }{\Gamma, A(0) \seqar A(t) , \Delta}

		\]

	\end{itemize}

\end{proof}

\subsection{Completeness}

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

\nb{WoP known as `minimization' principles in bounded arithmetic}

\begin{theorem}

	[Well ordering property]

	\[

	\pvbci{i+1} \proves \exists x^\safe . A(x) \cimp \exists  x^\safe . (A(x) \cand \forall y^\safe . (A(y) \cimp x \leq y ) )

	\]

\end{theorem}

\begin{proof}

	We work in $\pvbci{i+1}$ and show the contrapositive. 

	Suppose:

	\begin{equation}

	\label{eqn:no-least}

	\forall x^\safe. (A(x) \cimp \exists y^\safe . A(y) \cand y<x )

	\end{equation}

	We show that,

	\begin{equation}

	\label{eqn:ih-wop}

	\forall x. \forall y \leq a - x. (\cnot A(y) \cimp \cnot A(y + x))

	\end{equation}

	by polynomial induction on $x$.

	Let $B(x)$ be such that \eqref{eqn:ih-wop} is $\forall x . B(x)$.

	\nb{If $A \in \Sigma^\safe_i \cup \Pi^\safe_i$ then $B \in \Pi^\safe_{i+1}$.}

	When $x=0$, notice that \eqref{eqn:ih-wop} is just a generalised identity.

	Suppose that $B(x)$ and let us show that $B(2x)$.

	Let $y \leq a - 2x$ such that $\cnot A(y)$. 

	Then $y\leq a-x$ so by $B(x)$ we have that $\cnot A(y+x)$.

	We also have that $y+x \leq a-x$ so by $B(x)$ we have that $\cnot A(y+2x)$, as required.

	Now suppose that $B(x)$ and let us show that $B(2x+1)$.

	Let $y \leq a - 2x - 1$ such that $\cnot A(y)$.

	By similar reasoning to the $2x$ case, we have that $\cnot A(y + 2x )$.

\end{proof}

\begin{theorem}

\end{theorem}

\subsection{What we want for WoP}

From bounded arithmetic:

$\Sigma_{i+1}$-LMIN $ \iff$ $\Sigma_{i+1}$-PIND $\implies$ $\Sigma_i$-IND $\iff$ $\Sigma_i$-MIN $ \iff$ $\Pi_{i+1}$-MIN.

\subsection{Completeness proof idea}

For each $\mubci i$ function $f(\vec u ; \vec x)$ we $\Sigma_i$-define a formula $A_f (\vec u ; \vec x  , y )$ in $\pvbci{i+1}$ such that:

\[

\proves A_f (\vec u ; \vec x , y)

\quad 

\iff

\quad

f(\vec u ; \vec x) = y

\]

and $A_f$ is provably total in $\pvbci{i+1}$.

For the $\mu$ case, say we have the function:

\[

\mu x^{+1} . f(\vec u ; \vec x , x) =_2 0

\]

Let $A_f (\vec u ; \vec x , y)$ be given by the inductive hypothesis.

We define $A(\vec u ; \vec x , z)$ as:

\[

\begin{array}{rl}

&\left(

z=0 \  \cand \ \forall x^\safe , y^\safe . (A_f (\vec u ; \vec x , x, y) \cimp y=_2 1)

\right) \\

\cor & \left(

\begin{array}{ll}

z\neq 0 

& \cand\   \forall y^\safe . (A_f (\vec u ; \vec x , z , y) \cimp y=_2 0 ) \\

& \cand\ \forall x^\safe < p(;z) . (\forall y^\safe . A_f (\vec u ; \vec x , x , y) \cimp y=_2 1) 

\end{array}

\right)

\end{array}

\]

Notice that $A$ is $\Pi_k$, since $A_f$ is $\Sigma_k$.

What about, say recursion on a formula? Need a form of `ranked comprehension'?

E.g., when $A$ is $\Sigma_k$ then we can introduce a rank $k$ symbol (a sort?) such that:

\[

\forall \vec u^\normal, \vec x^\safe . \exists ! y^\safe . A(\vec u ; \vec x , y)

\implies

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

\]

Otherwise, can we use definability of computations? E.g., if:

\[

\begin{array}{rcl}

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

f(s_i u , \vec u ; \vec x) & \dfn & h_i (u , \vec u ; \vec x , f(u,\vec u ; \vec x))

\end{array}

\]

Suppose we have $A_g (\vec u ; \vec x,y)$ and $A_i (u , \vec u ; \vec x , y , z)$ defining $g$ and $h_i$ respectively.

We define $A_f (u ,\vec u ; \vec x , y)$ as:

\[

\exists z^\safe . \left(

\begin{array}{ll}

& Seq(z) \cand \exists y_0 . ( A_g (\vec u ; \vec x , y_0) \cand \beta_0 (z , y_0) ) \cand \beta_{|u|} ( z,y ) \\

\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta_k (z, y_i) \cand \beta_{k+1} (z, y_{k+1})  \cand A_i (u , \vec u ; \vec x , y_k , y_{k+1}) )

\end{array}

\right)

\]

(Can we really assume $z$ is safe here?)

POINT: for whatever formulation, we need to prove:

\[

\exists y^\safe . A_f (a , \vec u ; \vec x , y) 

\quad \seqar \quad

\exists y^\safe . A_f (s_i a, \vec u ; \vec x , y)

\]

SHOULD HAVE: $\beta (i;x)$ for $i$th element of sequence $x$. 

Therefore need 'sharply bounded' quantification for normal variables?

In fact, why not $\beta(;i,x) $? Should be fine. So only safe quantification is needed for PH, but lose level-by-level delineation.

GOALS:

\begin{enumerate}

	\item PVBC + FCA + $\safe$-IND characterises PH. (Recursion included in PVBC)

	\item Refinement of above with `ranks' to delineate levels (definitions of $\pvbci{i}$).

	\item Arithmetic including both safe and sharply bounded normal quantification. (for sequences)

	\item (if time) allow both bounded and safe quantifiers?

\end{enumerate}

FCA:

\[

\exists f^\safe . \forall \vec u ; \vec x .

\left(

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

\right)

\]

(with typing information)

This could be enough with open induction if we introduce ranks later? Yup, seems like a good idea. Can then make into a real `open' theory.

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