Index: CSL17/tech-report/main.tex
===================================================================
--- CSL17/tech-report/main.tex	(revision 260)
+++ CSL17/tech-report/main.tex	(revision 261)
@@ -6,6 +6,7 @@
 \usepackage{microtype}
 \usepackage[dvipsnames]{xcolor}
 \usepackage{hyperref}
+\usepackage{enumerate}
 
 
 
Index: CSL17/tech-report/arithmetic.tex
===================================================================
--- CSL17/tech-report/arithmetic.tex	(revision 260)
+++ CSL17/tech-report/arithmetic.tex	(revision 261)
@@ -22,89 +22,119 @@
 
 The $\basic$ axioms of bounded arithmetic give the inductive definitions and interrelationships of the various function and predicate symbols.
 It also states fundamental algebraic properties, e.g.\ $(0,\succ{ } )$ is a free algebra, and, for us, it will also give us certain `typing' information for our function symbols based on their $\bc$ specification, with safe inputs ranging over $\safe$ and normal ones over $\normal$.
-For instance, we include the following axioms:\footnote{Later some of these will be redundant, for instance $\safe (u \times x) $ and $\safe (u \smsh v)$ are consequences of $\Sigma^\safe_i$-$\pind$, but $\safe (x + y)$ is not since both inputs are safe and so we cannot induct.}
-\[
-\begin{array}{l}
-\forall u^\normal. \safe(u) \\
-\safe (0) \\
-\forall x^\safe . \safe (\succ{} x) \\
-\end{array}
-\qquad
-\begin{array}{l}
-\forall x^\safe, y^\safe . \safe(x+y)\\
-\forall u^\normal, x^\safe . \safe(u\times x) \\
-\forall u^\normal , v^\normal . \safe (u \smsh v)\\
-\forall u^\safe .\safe(\hlf{u})\\
-\forall u^\normal .\safe(|x|)
-\end{array}
-\]
-Notice that we have $\normal \subseteq \safe$.
 
+
+Namely, in addition to usual axioms, our $\basic$ includes the following:\footnote{Later some of these will be redundant, for instance $\safe (u \times x) $ and $\safe (u \smsh v)$ are consequences of $\Sigma^\safe_i$-$\pind$, but $\safe (x + y)$ is not since both inputs are safe and so we cannot induct.}
+\begin{enumerate}[(a)]
+	\item $\forall u^\normal. \safe(u) $
+	\item $\safe (0) $
+	\item $\forall x^\safe . \safe (\succ{} x) $
+	\item $\forall u^\safe .\safe(\hlf{u})$
+	\item $\forall x^\safe, y^\safe . \safe(x+y)$
+	\item $\forall u^\normal, x^\safe . \safe(u\times x) $
+	\item $\forall u^\normal , v^\normal . \safe (u \smsh v)$
+	\item $\forall u^\normal .\safe(|x|)$
+\end{enumerate}
+%\[
+%\begin{array}{l}
+%\forall u^\normal. \safe(u) \\
+%\safe (0) \\
+%\forall x^\safe . \safe (\succ{} x) \\
+%\forall u^\safe .\safe(\hlf{u})
+%\end{array}
+%\qquad
+%\begin{array}{l}
+%\forall x^\safe, y^\safe . \safe(x+y)\\
+%\forall u^\normal, x^\safe . \safe(u\times x) \\
+%\forall u^\normal , v^\normal . \safe (u \smsh v)\\
+%\forall u^\normal .\safe(|x|)
+%\end{array}
+%\]
+Notice in particular that we have $\normal \subseteq \safe$.
+%
 Apart from these, the remaining $\basic$ axioms mimic those of Buss in \cite{Buss86book}:
+\begin{enumerate}[(1)]
+	\item $\forall x^{\safe}, y^{\safe}.  (y\leq x\cimp  y \leq \succ{} x) $
+	\item $\forall x^{\safe}. x \neq \succ{} x$
+	\item $\forall x^{\safe}.0 \leq x$
+	\item $\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) $
+	\item $\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)$
+	\item $\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)$
+	\item $\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)$
+	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)$
+	\item $|0|=0$
+	\item $\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp  (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) $
+	\item $|\succ{}0|=\succ{} 0$
+	\item $\forall x^{\safe}, y^{\safe}.   (x\leq y \cimp   |x|\leq  |y|)$
+	\item $\forall x^{\normal}, y^{\normal}.    |x\smsh y|=\succ{}( |x|\cdot  |y|)$
+	\item $\forall y^{\normal}.    0 \smsh y=\succ{} 0$
+	\item $\forall x^{\normal}.    (x\neq 0 \cimp (1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)))$
+	\item $\forall x^{\normal}, y^{\normal}.    x \smsh y = y \smsh x$
+	\item $\forall x^{\normal}, y^{\normal}, z^{\normal}. (   |x|= |y| \cimp x\smsh z = y\smsh z)$
+	\item $\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}.      (|x|= |u|+  |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))$
+	\item $\forall x^{\safe}, y^{\safe}.      x\leq x+y$
+	\item $\forall x^{\safe}, y^{\safe}.    (  ( x\leq y \cand x\neq y) \cimp( \succ{}(\succ{0}x) \leq \succ{0}y \cand  \succ{}(\succ{0}x) \neq \succ{0}y))$
+	\item $\forall x^{\safe}, y^{\safe}.     x+y=y+x$
+	\item $\forall x^{\safe}.       x+0=x$
+	\item $\forall x^{\safe}, y^{\safe}.       x+\succ{}y=\succ{}(x+y)$
+	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}.      (x+y)+z=x+(y+z)$
+	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. (    x+y \leq x+z \ciff y\leq z)$
+	\item $\forall x^{\safe}       0\cdot x =0$
+	\item $\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x$
+	\item $\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x$
+	\item $\forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)$
+	\item $\forall x^{\normal}, y^{\safe}, z^{\safe}.      (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))$
+	\item $\forall x^{\normal}  .     (x\neq 0 \cimp  |x|=\succ{}(\hlf{x}))$
+	\item $\forall x^{\safe}, y^{\safe}.   (  x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))$
+\end{enumerate}
 
-$$
-%\begin{equation}
-\begin{array}{l}
-\forall x^{\safe}, y^{\safe}.  (y\leq x\cimp  y \leq \succ{} x) \\
-\forall x^{\safe}. x \neq \succ{} x\\
-\forall x^{\safe}.0 \leq x\\
-\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) \\
-\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)\\
-\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)\\
-\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)\\
-\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)\\
-|0|=0\\
-\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp  (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) \\
-|\succ{}0|=\succ{} 0\\
-\forall x^{\safe}, y^{\safe}.   (x\leq y \cimp   |x|\leq  |y|)\\
-\forall x^{\normal}, y^{\normal}.    |x\smsh y|=\succ{}( |x|\cdot  |y|)\\
-\forall y^{\normal}.    0 \smsh y=\succ{} 0\\
-\forall x^{\normal}.    (x\neq 0 \cimp (1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)))\\
-\forall x^{\normal}, y^{\normal}.    x \smsh y = y \smsh x\\
-\forall x^{\normal}, y^{\normal}, z^{\normal}. (   |x|= |y| \cimp x\smsh z = y\smsh z)\\
-\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}.      (|x|= |u|+  |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))\\
-\forall x^{\safe}, y^{\safe}.      x\leq x+y\\
-\forall x^{\safe}, y^{\safe}.    (  ( x\leq y \cand x\neq y) \cimp( \succ{}(\succ{0}x) \leq \succ{0}y \cand  \succ{}(\succ{0}x) \neq \succ{0}y))\\
-\forall x^{\safe}, y^{\safe}.     x+y=y+x\\
-\forall x^{\safe}.       x+0=x\\
-\forall x^{\safe}, y^{\safe}.       x+\succ{}y=\succ{}(x+y)\\
-\forall x^{\safe}, y^{\safe}, z^{\safe}.      (x+y)+z=x+(y+z)\\
-\forall x^{\safe}, y^{\safe}, z^{\safe}. (    x+y \leq x+z \ciff y\leq z)\\
-\forall x^{\safe}       0\cdot x =0\\
-\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x\\
-%\text{\anupam{check above normal/safe! Pretty sure should be other way around.}}\\
-\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x\\
-\forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)\\
-\forall x^{\normal}, y^{\safe}, z^{\safe}.      (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))\\
-\forall x^{\normal}  .     (x\neq 0 \cimp  |x|=\succ{}(\hlf{x}))\\
-\forall x^{\safe}, y^{\safe}.   (  x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))
-\end{array}
-%\end{equation}
-$$
 
+%$$
+%%\begin{equation}
+%\begin{array}{l}
+%\forall x^{\safe}, y^{\safe}.  (y\leq x\cimp  y \leq \succ{} x) \\
+%\forall x^{\safe}. x \neq \succ{} x\\
+%\forall x^{\safe}.0 \leq x\\
+%\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) \\
+%\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)\\
+%\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)\\
+%\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)\\
+%\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)\\
+%|0|=0\\
+%\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp  (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) \\
+%|\succ{}0|=\succ{} 0\\
+%\forall x^{\safe}, y^{\safe}.   (x\leq y \cimp   |x|\leq  |y|)\\
+%\forall x^{\normal}, y^{\normal}.    |x\smsh y|=\succ{}( |x|\cdot  |y|)\\
+%\forall y^{\normal}.    0 \smsh y=\succ{} 0\\
+%\forall x^{\normal}.    (x\neq 0 \cimp (1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)))\\
+%\forall x^{\normal}, y^{\normal}.    x \smsh y = y \smsh x\\
+%\forall x^{\normal}, y^{\normal}, z^{\normal}. (   |x|= |y| \cimp x\smsh z = y\smsh z)\\
+%\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}.      (|x|= |u|+  |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))\\
+%\forall x^{\safe}, y^{\safe}.      x\leq x+y\\
+%\forall x^{\safe}, y^{\safe}.    (  ( x\leq y \cand x\neq y) \cimp( \succ{}(\succ{0}x) \leq \succ{0}y \cand  \succ{}(\succ{0}x) \neq \succ{0}y))\\
+%\forall x^{\safe}, y^{\safe}.     x+y=y+x\\
+%\forall x^{\safe}.       x+0=x\\
+%\forall x^{\safe}, y^{\safe}.       x+\succ{}y=\succ{}(x+y)\\
+%\forall x^{\safe}, y^{\safe}, z^{\safe}.      (x+y)+z=x+(y+z)\\
+%\forall x^{\safe}, y^{\safe}, z^{\safe}. (    x+y \leq x+z \ciff y\leq z)\\
+%\forall x^{\safe}       0\cdot x =0\\
+%\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x\\
+%%\text{\anupam{check above normal/safe! Pretty sure should be other way around.}}\\
+%\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x\\
+%\forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)\\
+%\forall x^{\normal}, y^{\safe}, z^{\safe}.      (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))\\
+%\forall x^{\normal}  .     (x\neq 0 \cimp  |x|=\succ{}(\hlf{x}))\\
+%\forall x^{\safe}, y^{\safe}.   (  x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))
+%\end{array}
+%%\end{equation}
+%$$
+%
 
 
 
 
 
-It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:
-\begin{proposition}
-	[Length induction]
-	The axiom schema of formulae,
-	\begin{equation}
-	\label{eqn:lind}
-	( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)
-	\end{equation}
-	for formulae $A \in \Sigma^\safe_i$
-	is equivalent to $\cpind{\Sigma^\safe_i}$.
-\end{proposition}
-\begin{proof}
-	Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.
-	Then, by $\basic$, we have that $A(|a|) \cimp A(|2a|)$ and $A(|a|) \cimp A(|2a+1|)$ for each $a \in \normal$, whence we may conclude $\forall x. A(|x|)$ by polynomial induction on $A(|x|)$.
-\end{proof}
 
-Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\Xi}$, when $A \in \mathcal \Xi$.
-We will freely use this in place of polynomial induction whenever it is convenient.
 
 %\begin{definition}
 %	[Basic theory]
@@ -126,18 +156,8 @@
 %
 %Use base theory + sharply bounded quantifiers.
 
+In addition to these axioms, our theories will contain forms of induction, defined below.
 
-\begin{definition}
-[Quantifier hierarchy]
-$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded and where $\safe , \normal$ do not occur free.
-We define $\Sigma^\safe_{i+1}$ as the closure of $\Pi^\safe_i $ under $\cor, \cand $, safe existentials and sharply bounded quantifiers.
-We define $\Pi^\safe_{i+1}$ as the closure of $\Sigma^\safe_i $ under $\cor, \cand $, safe universals and sharply bounded quantifiers.
-\end{definition}
-
-
-Notice that the criterion that $\safe$ does not occur free is not a real restriction, since we can write $\safe (x)$ as $\exists y^\safe . y=x$.
-The criterion is purely to give an appropriate definition of the hierarchy above.
-
 %\anupam{Collection principles for prenexing? Otherwise need to add closure under sharply bounded quantifiers.}
 
 
@@ -158,7 +178,20 @@
 %We write $I\Xi$ to denote the theory consisting of $\basic$ and $\cax{\Xi}{\ind}$.
 \end{definition}
 
+We will introduce in fact a hierarchy of theories calibrated by the complexity of induction formulae, so we now introduce the appropriate quantifier hierarchy.
 
+\begin{definition}
+	[Quantifier hierarchy]
+	$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded and where $\safe , \normal$ do not occur free.
+	We define $\Sigma^\safe_{i+1}$ as the closure of $\Pi^\safe_i $ under $\cor, \cand $, safe existentials and sharply bounded quantifiers.
+	We define $\Pi^\safe_{i+1}$ as the closure of $\Sigma^\safe_i $ under $\cor, \cand $, safe universals and sharply bounded quantifiers.
+\end{definition}
+
+
+Notice that the criterion that $\safe$ does not occur free is not a real restriction, since we can write $\safe (x)$ as $\exists y^\safe . y=x$.
+The criterion is purely to give an appropriate definition of the hierarchy above.
+
+
 \begin{definition}\label{def:ariththeory}
 Define the theory $\arith^i$ consisting of the $\basic$ axioms, $\cpind{\Sigma^\safe_i } $,
 %\begin{itemize}
@@ -195,10 +228,30 @@
 	\todo{Proof: Patrick? The final two should require PIND.}
 \end{example}
 
+It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:
+\begin{proposition}
+	[Length induction]
+	The axiom schema of formulae,
+	\begin{equation}
+	\label{eqn:lind}
+	( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)
+	\end{equation}
+	for formulae $A \in \Sigma^\safe_i$
+	is equivalent to $\cpind{\Sigma^\safe_i}$.
+\end{proposition}
+\begin{proof}
+	Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.
+	Then, by $\basic$, we have that $A(|a|) \cimp A(|2a|)$ and $A(|a|) \cimp A(|2a+1|)$ for each $a \in \normal$, whence we may conclude $\forall x. A(|x|)$ by polynomial induction on $A(|x|)$.
+\end{proof}
 
+Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\Xi}$, when $A \in \Xi$.
+We will freely use this in place of polynomial induction whenever it is convenient.
+
+
 \subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
 
-We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall \vec u^{\normal} , \forall  \vec x^{\safe}, \exists! y^{\safe}. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
+We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall \vec u^{\normal} , \forall  \vec x^{\safe}, \exists! y^{\safe}. A_f (\vec u , \vec x , y)$, such that $\Nat \models A_f (\vec u , \vec x , f(\vec u , \vec x))$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
+We sometimes explicitly delimit variables as such when it is helpful, writing $A_f (\vec u ; \vec x , y)$.
  
 Let us give a few examples for basic functions representable in $\arith^1$, wherein proofs of totality are routine:
 \begin{itemize}
@@ -206,12 +259,21 @@
 %\item Successor $\succ{}$: $\forall x^{\safe} , \exists^{\safe} y. y=x+1.$. The formulas for the binary successors $\succ{0}$, $\succ{1}$ and the constant functions $\epsilon^k$ are defined in a similar way.
 %\item Predecessor $p$:   $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$
 \item Conditional $C$: 
-$$\begin{array}{ll}
-\forall x^{\safe} ,  y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=0)\cand (y=y_0)\\
-                                                                                                   & \cor( \exists z^{\safe}.(x=\succ{0}z) \cand (y=y_0))\\
-                                                                                                   & \cor( \exists z^{\safe}.(x=\succ{1}z) \cand (y=y_1)))\
+$$
+\forall x^{\safe} ,  y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. 
+\left( 
+\begin{array}{rl}
+&\exists z^{\safe}.x=\succ{0}z \cand y=y_0 \\
+\cor&  \exists z^{\safe}.x=\succ{1}z \cand y=y_1
 \end{array}
+\right)
 $$
+%$$\begin{array}{ll}
+%\forall x^{\safe} ,  y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=0)\cand (y=y_0)\\
+%                                                                                                   & \cor( \exists z^{\safe}.(x=\succ{0}z) \cand (y=y_0))\\
+%                                                                                                   & \cor( \exists z^{\safe}.(x=\succ{1}z) \cand (y=y_1)))\
+%\end{array}
+%$$
 %\item Addition:
 %$\forall^{\safe} x, y,  \exists^{\safe} z. z=x+y$. 
 \item Prefix:
