Index: arithmetic.tex
===================================================================
--- arithmetic.tex	(revision 219)
+++ arithmetic.tex	(revision 220)
@@ -1,36 +1,28 @@
 \section{An arithmetic for the polynomial hierarchy}\label{sect:arithmetic}
 %Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$. 
-Our base language is defined by the set of functions (and constants) symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|, \hlf{}.\}$ and the set of predicate symbols 
- $\{\leq, \safe, \normal \}$. The intended meaning of $|x|$ is the length of $x$ seen as a binary string, and that of $\smash(x,y)$ is $2^{|x||y|}$, so a string of length $|x||y|+1$.
+Our base language consists of constant and function symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|, \hlf{}.\}$ and predicate symbols 
+ $\{\leq, \safe, \normal \}$. The function symbols are interpreted in the intuitive way, with $|x|$ denoting the length of $x$ seen as a binary string, and $\smash(x,y)$ denoting $2^{|x||y|}$, so a string of length $|x||y|+1$.
+ We may write $\succ{0}(x)$ for $2\cdot x$, $\succ{1}(x)$ for $\succ{}(2\cdot x)$, and $\pred (x)$ for $\hlf{x}$, to better relate to the $\bc$ setting.
  
-We use classical logic connectives $\neg$, $\cand$, $\cor$, $\forall$, $\exists$. The formula $A \cimp B$ will be a notation for $\neg A \cor B$.
-We will also use as shorthand notations:
-$$ (s=t) = (s\leq t) \cand (t\leq s), \quad (s\neq t) = \neg(s=t).$$ 
-We call \textit{atomic formulas} formulas of the form $(s\leq t)$ or $(s=t)$.
- As we are in classical logic, we will assume, without loss of generality, that formulas are in \textit{De Morgan normal form}, that is to say that in formulas negation can only occur on atomic formulas, and that there is not any occurrence of subformula of the form $\neg \neg A$.
+We consider formulas of classical first-order logic, over $\neg$, $\cand$, $\cor$, $\forall$, $\exists$, along with usual shorthands and abbreviations. 
+%The formula $A \cimp B$ will be a notation for $\neg A \cor B$.
+%We will also use as shorthand notations:
+%$$ (s=t) = (s\leq t) \cand (t\leq s), \quad (s\neq t) = \neg(s=t).$$ 
+\textit{Atomic formulas} formulas are of the form $(s\leq t)$, for terms $s,t$.
+ We will assume, without loss of generality, that formulas are in \textit{De Morgan normal form}, that is to say that in formulas negation can only occur on atomic formulas, and that there is not any occurrence of a subformula of the form $\neg \neg A$.
+ We write $\exists x^{N_i} . A$ or $\forall x^{N_i} . A$ for $\exists x . (N_i (x) \cand A)$ and $\forall x . (N_i (x) \cimp A)$ respectively.
 
-In the sequel $\succ{0}(x)$ stand for $2\cdot x$ and $\succ{1}(x)$ stand for $\succ{}(2\cdot x)$,
-Now, let us describe the axioms we are considering.The $\basic$ axioms are as follows:
-\[
-\begin{array}{l}
-\safe (0) \\
-\forall x^\safe . \safe (\succ{} x) \\
-\forall x^\safe . 0 \neq \succ{} (x) \\
-\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
-\forall x^\safe . (x = 0 \cor \exists y^\safe.\  x = \succ{} y   )\\
-\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(u) \\
-\forall u^\safe \safe(\hlf{u})\\
-\forall x^\safe \safe(|x|)  
-\end{array}
-\]
-%\patrick{did I type writly the 2 last axioms?}
 
-and the list of axioms of Appendix \ref{appendix:arithmetic}, coming from \cite{Buss86book}.
+The theories we introduce are directly inspired from bounded arithmetic, namely the theories $S^i_2$.
+We include a similar set of axioms for direct comparison, although in our setting these are not minimal.
+Indeed, $\#$ can be defined using induction in our setting.
 
-\anupam{in fact, we use essentially the same language, so just take Buss' Basic axioms after proper typing. Should also add the symbol $\hlf{\cdot}$ for binary predecessor then we have the full language of bounded arithmetic.}
+The $\basic$ axioms of bounded arithmetic give the inductive definitions and interrelationships of the various function symbols.
+It also states the fundamental algebraic properties, i.e.\ $(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$.
+\begin{definition}
+	[Basic theory]
+	The theory $\basic$ consists of the axioms from Appendix \ref{appendix:arithmetic}.
+	\end{definition}
 
 
 Notation: if $\vec t=t_0,\dots, t_k$, we will denote as $\safe(\vec t)$ the sequence of formulas $\safe(t_0),\dots, \safe(t_k)$. Similarly for $\normal(\vec t)$.
@@ -108,25 +100,7 @@
 Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\mathcal C}$, when $A \in \mathcal C$.
 We will freely use this in place of polynomial induction whenever it is convenient.
 
-\begin{lemma}
-[Sharply bounded lemma]
-\label{lem:sharply-bounded-recursion}
-Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$.
-Then the characteristic functions of $\forall u \prefix v . A(u,\vec u ; \vec x)$ and $\exists u \prefix v . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$.
-\end{lemma}
-\begin{proof}
-	We give the $\forall$ case, the $\exists$ case being dual.
-	The characteristic function $f(v , \vec u ; \vec x)$ is defined by predicative recursion on $v$ as:
-	\[
-	\begin{array}{rcl}
-	f(0, \vec u ; \vec x) & \dfn & f_A (0 , \vec u ; \vec x) \\
-	f(\succ i v , \vec u ; \vec x) & \dfn & \cond ( ; f_A (\succ i v, \vec u ; \vec x) , 0 , f(v , \vec u ; \vec x) )
-	\end{array}
-	\]
-\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)$.
 
 
 \subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
