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

		\[

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

		\]

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

	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}

	\begin{equation}

	\label{eqn:ih-wop}

	\end{equation}

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

\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$. (In fact, why not $\beta(;i,x) $?)

Therefore need 'sharply bounded' quantification for normal variables?

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}