Index: CSL17/arithmetic.tex
===================================================================
--- CSL17/arithmetic.tex	(revision 167)
+++ CSL17/arithmetic.tex	(revision 168)
@@ -1,11 +1,15 @@
 \section{An arithmetic for the polynomial hierarchy}
+Our base language is $\{ 0, \succ 0, \succ 1, \pred, + , \times, \smsh , |\cdot| , \leq \}$.
 
+
 (Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers)
 
 Use base theory + sharply bounded quantifiers.
 
 \anupam{Perhaps use prefix quantifier instead of sharply bounded (a la Ignatovic?), since plays nicer with sharply bounded lemma?}
 
+
+
 \begin{definition}
 [Quantifier hierarchy]
 We define:
@@ -15,16 +19,23 @@
 \end{itemize}	
 \end{definition}
 
+
+\anupam{Collection principles for prenexing? Otherwise need to add closure under sharply bounded quantifiers.}
+
+
 \begin{definition}
 Define the theory $\arith^i$ consisting of the following axioms:
 \begin{itemize}
 	\item $\basic$;
 	\item $\cpind{\Sigma^\safe_i } $:
-	\item $\forall \vec x \in \normal . \exists  y \in \safe .  A \cimp \forall \vec x \in \normal .\exists y\in \normal . A$ (raising) .
 \end{itemize}
+and an inference rule:
+\[
+ \dfrac{\forall \vec x^\normal . \exists  y^\safe .  A }{ \forall \vec x^\normal .\exists y^\normal . A}
+\]
 \end{definition}
+\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
 
-
 \begin{lemma}
 [Sharply bounded lemma]
 Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$.
@@ -42,4 +53,20 @@
 \end{proof}
 
 Notice that $\prefix$ suffices to encode usual sharply bounded inequalities,
-since $\forall u \leq |t| . A(u , \vec u ; \vec x) \ciff \forall u \prefix t . A(|u|, \vec u ; \vec x)$.
\ No newline at end of file
+since $\forall u \leq |t| . A(u , \vec u ; \vec x) \ciff \forall u \prefix t . A(|u|, \vec u ; \vec x)$.
+
+
+\subsection{Graphs of some basic functions}
+Todo: $+1$,  
+
+\subsection{Encoding sequences in the arithmetic}
+\todo{}
+
+\anupam{Assume we have a $\Sigma^\safe_1$ predicate $\beta(i,x,y)$, expressing that the $i$th element of the sequence $x$ is $y$, such that $\arith^1 \proves \forall i^\normal , x^\safe . \exists ! y^\safe . \beta (i,x,y)$.}
+
+
+\subsection{A sequent calculus presentation}
+\todo{Write out usual first-order sequent calculus}
+
+\subsection{Free-cut free normal form of proofs}
+\todo{State theorem, with references (Takeuti, Cook-Nguyen) and present the important corollaries for this work.}
\ No newline at end of file
Index: CSL17/ph-macros.tex
===================================================================
--- CSL17/ph-macros.tex	(revision 167)
+++ CSL17/ph-macros.tex	(revision 168)
@@ -20,6 +20,8 @@
 \newcommand{\pind}{\mathit{PIND}}
 \newcommand{\cind}[1]{#1\text{-}\ind}
 \newcommand{\cpind}[1]{#1\text{-}\pind}
+\renewcommand{\min}{\mathit{MIN}}
+\newcommand{\cmin}[1]{#1\text{-}\min}
 
 \newcommand{\prefix}{\preccurlyeq}
 
@@ -31,8 +33,9 @@
 
 \renewcommand{\epsilon}{\varepsilon}
 \newcommand{\pred}{p}
-\renewcommand{\succ}[1]{s_i}
+\renewcommand{\succ}[1]{s_{#1}}
 \newcommand{\cond}{C}
+\newcommand{\smsh}{\#}
 
 \newcommand{\safe}{{S}}
 \newcommand{\normal}{N}
Index: CSL17/further.tex
===================================================================
--- CSL17/further.tex	(revision 167)
+++ CSL17/further.tex	(revision 168)
@@ -1 +1,7 @@
-\section{Further results}
\ No newline at end of file
+\section{Further results}
+
+\subsection{Equational theories}
+\todo{Mention PVBC}
+
+\subsection{Modal and second order theories}
+\todo{Mention links with ramification/sortedness}
\ No newline at end of file
Index: CSL17/completeness.tex
===================================================================
--- CSL17/completeness.tex	(revision 167)
+++ CSL17/completeness.tex	(revision 168)
@@ -5,4 +5,140 @@
 \begin{theorem}
 	\label{thm:completeness}
 	For every $\mubci{i-1}$ program $f(\vec u ; \vec x)$ (which is in $\fphi i$), there is a $\Sigma_i$ formula $A_f(\vec u, \vec x)$ such that $\arith^i$ proves $\forall \vec u \in \normal . \forall \vec x \in \safe. \exists ! y \in \safe . A_f(\vec u , \vec x , y )$ and $\Nat \models \forall \vec u , \vec x. A(\vec u , \vec x , f(\vec u ; \vec x))$.
-\end{theorem}
\ No newline at end of file
+\end{theorem}
+
+The rest of this section is devoted to a proof of this theorem.
+We proceed by structural induction on a $\mubc{i-1} $ program, dealing with each case in the proceeding paragraphs.
+
+\paragraph*{Predicative minimisation}
+Suppose $f(\vec u ; \vec x)$ is defined as $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$. 
+By definition $g$ is in $\mubci{i-2}$, and so by the inductive hypothesis there is a $\Sigma_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$ computing the graph of $g$ such that,
+\[
+\arith^i \proves \forall \vec u^\normal . \forall \vec x^\safe , x^\safe . \exists ! y^\safe . A_g(\vec u , \vec x , x , y)
+\]
+Let us define $A_f(\vec u ; \vec x , z)$ as:
+\[
+\begin{array}{rl}
+&\left(
+z=0 \  \cand \ \forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)
+\right) \\
+\cor & \left(
+\begin{array}{ll}
+z\neq 0 
+& \cand\   \forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) \\
+& \cand\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) 
+\end{array}
+\right)
+\end{array}
+\]
+Notice that $A_f$ is $\Pi_{i-1}$, since $A_g$ is $\Sigma_{i-1}$ and occurs only in negative context above, with additional safe universal quantifiers occurring in positive context.
+In particular this means $A_f$ is $\Sigma_i$.
+
+Now, to prove totality of $A_f$, we rely on $\Sigma^\safe_{i-1}$-minimisation, which is a consequence of $\cpind{\Sigma^\safe_i}$:
+
+\begin{lemma}
+[Minimisation]
+$\arith^i \proves \cmin{\Sigma^\safe_{i-1}}$.	
+\end{lemma}
+\begin{proof}
+\todo{}
+\end{proof}
+
+Now, working in $\arith^i$, let $\vec u \in \normal , \vec x \in \safe$ and let us prove:
+\[
+\exists !z^\safe  . A_f(\vec u ; \vec x , z)
+\]
+Suppose that $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$.
+We can apply minimisation due to the lemma above to find the least $x\in \safe$ such that $\exists y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$, and we set $z = \succ 1 x$.
+\todo{verify $z\neq 0$ disjunct.} 
+
+Otherwise, we have that $\forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)$ and so we can set $z=0$.
+
+
+\paragraph*{Predicative recursion on notation}
+Now suppose that $f$ is defined by PRN:
+\[
+\begin{array}{rcl}
+f(0 , \vec u ; \vec x) & \dfn & g(\vec u ; \vec x) \\
+f(\succ i u, \vec u ; \vec x) & \dfn & h_i( u , \vec u ; \vec x , f(u , \vec u ; \vec x))
+\end{array}
+\]
+
+\anupam{using $\beta(i,x,y)$ predicate for sequences: ``$i$th element of $x$ is $y$''. Provably total in $\arith^1$.}
+
+Suppose we have $\Sigma^\safe_i$ formulae $A_g (\vec u ; \vec x,y)$ and $A_{h_i} (u , \vec u ; \vec x , y , z)$ computing the graphs of $g$ and $h_i$ respectively, provably total in $\arith^i$.
+We define $A_f (u ,\vec u ; \vec x , y)$ as,
+\[
+\exists w^\safe . \left(
+\begin{array}{ll}
+& 
+%Seq(z) \cand 
+\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\
+\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_i) \cand \beta (k+1 ,w, y_{k+1})  \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )
+\end{array}
+\right)
+\]
+which is $\Sigma^\safe_i$ by inspection, and indeed defines the graph of $f$.
+
+To show totality, let $\vec u \in \normal, \vec x \in \safe$ and proceed by induction on $u \in \normal$.
+The base case, when $u=0$, is immediate from the totality of $A_g$, so for the inductive case we need to show:
+\[
+\exists y^\safe . A_f (u , \vec u ; \vec x , y) 
+\quad \seqar \quad
+\exists z^\safe . A_f (s_i u, \vec u ; \vec x , y)
+\]
+
+\anupam{here need to `add' element to the computation sequence. Need to do this earlier in the paper.}
+
+\anupam{for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
+
+\paragraph*{Safe composition}
+Now suppose that $f$ is defined by safe composition:
+\[
+f(\vec u ; \vec x) \quad \dfn \quad g( \vec h(\vec u;) ; \vec h' (\vec u ; \vec x) )
+\]
+
+By the inductive hypothesis, let us suppose that we have $\Sigma^\safe_i $ definitions $A_g , A_{h_i} , A_{h_j'} $ of the graphs of $g , h_i , h_j'$ respectively, which are provably total etc.
+In particular, by Raising, we have that $\forall \vec u^\normal . \exists v^\normal . A_{h_i} (\vec u , v)$.
+
+We define $A_f (\vec u , \vec x , z)$ defining the graph of $f$ as follows:
+\[
+\exists \vec v^\normal . \exists \vec y^\safe .  
+\left(  
+\bigwedge\limits_i A_{h_i} (\vec u , v_i)
+\wedge
+\bigwedge\limits_j A_{h_j'} (\vec u ; \vec x , y_j)
+\wedge
+A_g ( \vec v , \vec y , z ) 
+\right)
+\]
+The provable totality of $A_f$ follows from simple first-order reasoning, mostly cuts and basic quantifier manipulations.
+
+\todo{elaborate}
+
+\paragraph*{Other cases}
+\todo{}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Index: CSL17/soundness.tex
===================================================================
--- CSL17/soundness.tex	(revision 167)
+++ CSL17/soundness.tex	(revision 168)
@@ -1 +1,9 @@
 \section{Soundness}
+\label{sect:soundness}
+
+The main result of this section is the following:
+
+\begin{theorem}
+	If $\arith^i$ proves $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that $\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x))$.
+\end{theorem}
+
Index: CSL17/preliminaries.tex
===================================================================
--- CSL17/preliminaries.tex	(revision 167)
+++ CSL17/preliminaries.tex	(revision 168)
@@ -46,7 +46,7 @@
 	\begin{enumerate}
 		\item The constant functions $\epsilon^k$ which takes $k$ arguments and outputs $\epsilon \in \Word$.
 		\item The projection functions $\pi^{m,n}_k ( x_1 , \dots , x_m ; x_{m+1} , \dots, x_{m+n} )  := x_k$ for $n,m \in \Word$ and $1 \leq k \leq m+n$.
-		\item The successor functions $\succ_i ( ; x) := xi$ for $i = 0,1$.
+		\item The successor functions $\succ i ( ; x) := xi$ for $i = 0,1$.
 		\item The predecessor function $\pred (; x) := \begin{cases}
 		\epsilon &  \mbox{ if }  x = \epsilon \\
 		x' &  \mbox{ if }  x = x'i
@@ -77,7 +77,7 @@
 		\[
 		\begin{array}{rcl}
 		f(0, \vec v ; \vec x) & := & g(\vec v ; \vec x) \\
-		f (\succ_i u , \vec v ; \vec x ) & := & h_i ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) )
+		f (\succ i u , \vec v ; \vec x ) & := & h_i ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) )
 		\end{array}
 		\]
 		for $i = 0,1$,  so long as the expressions are well-formed. % (i.e.\ in number/sort of arguments).
@@ -101,7 +101,7 @@
 \[
 \begin{array}{rcl}
 f^j(0, \vec v ; \vec x) & := & g^j(\vec v ; \vec x) \\
-f^j(\succ_i u , \vec v ; \vec x ) & := & h^j_i ( u , \vec v ; \vec x , \vec{f} (u , \vec v ; \vec x) )
+f^j(\succ i u , \vec v ; \vec x ) & := & h^j_i ( u , \vec v ; \vec x , \vec{f} (u , \vec v ; \vec x) )
 \end{array}
 \]
 for $i = 0,1$,  so long as the expressions are well-formed.
