Index: qpvbc.tex
===================================================================
--- qpvbc.tex	(revision 149)
+++ qpvbc.tex	(revision 150)
@@ -140,12 +140,17 @@
 		\]
 		(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]
 	\[
@@ -153,15 +158,120 @@
 	\]
 \end{theorem}
 \begin{proof}
-	We work in $\pvbci{i+1}$ and show the contrapositive. Suppose $\forall x^\safe. (A(x) \cimp \exists y^\safe . A(y) \cand y<x )$.
+	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 $c \leq a - 2x$ such that $\cnot A(c)$. Then $c\leq a-x$ so by the inductive hypothesis we have that TOFINISH
+	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$. (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}
 \end{document}
