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

PVBC+FCA+ safe induction characterises PHcd

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

\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 \proves \forall \vec u^\normal , \vec x^\sigma . \exists \vec y^\sigma. A(\vec u , \vec x , \vec y)$, then there are $\mubci i $ programs $\vec f (\vec u ; \vec x)$ such that $\pvbci i \proves\forall \vec u^\normal , \vec x^\sigma . A(\vec u , \vec x , \vec f (\vec u ; \vec x) )  $.

\end{theorem}

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

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

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