\documentclass{amsart}
\usepackage{amsthm}
	\usepackage{hyperref}
	\usepackage[dvipsnames]{xcolor}


\input{macros}

\begin{document}



	\section{Extending the basic BC framework}
\begin{itemize}
	\item 	Any polynomial-time predicate can be conservatively added to BC with only safe inputs.
	\item Thus all logical connectives $\neg, \vee, \wedge$ and equality testing $=$ can be implemented as programs with only safe arguments. 
	\item Can add G\"odel's $\beta$ functions with a safe input:
\end{itemize}	

	
\section{QPVBC}

\subsection{Bellantoni's system $\pvbci{}$}

\begin{definition}
	[Hierarchies]
	We define the following:
	\begin{itemize}
		\item $\fphi i$: $i$th level of functional polynomial hierarchy. I.e.\ $\Box_i$ = $\fptime(\Sigma^p_{i-1})$.
		\item $\mubci{i}$: $\mu$BC programs with $i$ nested $\mu$s, i.e., corresponds to $\fphi {i-1}$.
		\item $\pvbci i$: defined as $\pvbci{} + \Sigma^\sigma_i$-induction.
	\end{itemize}
\end{definition}

\begin{definition}
	[Provably total function]	
\end{definition}


\subsection{Extensions by induction principles}



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

\section{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.
\end{document}
