Index: intro.tex
===================================================================
--- intro.tex	(revision 243)
+++ intro.tex	(revision 244)
@@ -7,15 +7,15 @@
 
 To some extent there is a distinction between various notions of `representability', namely between logics that \emph{type} terms computing functions of a given complexity class, and theories that prove the \emph{totality} or \emph{convergence} of programs computing functions in a given complexity class.
 But a perhaps more important distinction is whether the constraints on the logic or theory are
-\textit{explicit} or \textit{implicit}, that is to say whether they stipulate some bounds or resources, or whether the bounds are only \textit{consequence} of some logical properties. One important representative of the first category is \textit{bounded arithmetic}, based on theories of arithmetic where quantiiers are bounded by terms in induction or comprehension formulae \cite{Buss86book,Krajicek:1996:BAP:225488,Cook:2010:LFP:1734064}. Cobham's function algebra  \cite{Cobham}  for polynomial time is of a similar nature, and indeed is used as a tool for the study of bounded arithmetic. In the second category one can range the systems of \textit{implicit computational complexity}, like for instance function algebras based on restrictions of recursion, such as ramified or safe recursion \cite{BellantoniCook92,Leivant95}, arithmetics or logics based on analogous restrictions of induction \cite{Cantini02},  \cite{Leivant94:intrinsic-theories} \cite{BelHof:02},  \cite{Marion01}, \cite{Leivant94:found-delin-ptime} and subsystems of linear logic   \cite{Girard94:lll} \cite{Lafont04} .
+\textit{explicit} or \textit{implicit}, that is to say whether they stipulate some bounds or resources, or whether the bounds are only \textit{consequence} of some logical properties. One important representative of the first category is \textit{bounded arithmetic}, based on theories of arithmetic where quantifiers are bounded by terms in induction or comprehension formulae \cite{Buss86book,Krajicek:1996:BAP:225488,Cook:2010:LFP:1734064}. Cobham's function algebra  \cite{Cobham}  for polynomial time is of a similar nature, and indeed is used as a tool for the study of bounded arithmetic. In the second category one there are various systems of \textit{implicit computational complexity}, for instance function algebras based on \emph{ramification} or \emph{safe recursion} \cite{BellantoniCook92,Leivant95}, arithmetics or logics based on analogous restrictions of induction \cite{Cantini02},  \cite{Leivant94:intrinsic-theories} \cite{BelHof:02},  \cite{Marion01}, \cite{Leivant94:found-delin-ptime} and subsystems of \emph{linear logic} \cite{Girard94:lll} \cite{Lafont04} .
 
  Bounded arithmetic is a deep and well-established field, and one of its advantages is its great versatility, allowing a characterization of a wide range of complexity classes, such as $\ptime$, the polynomial hierarchy $\ph$, $\pspace$, $\mathbf{NC}^i$ etc. 
  %It is also closely related to \textit{proof complexity}, the research field investigating the size of propositional proofs in various proof systems. Finally it is also employed for the research direction of \textit{bounded reverse mathematics}. 
-  
-  Implicit computational complexity on the other hand is a slightly more recent and less unified line of research. It aims to relate certain computing disciplines with complexity theoretic features, and has helped shed some light on the foundational nature of `feasibility' (see e.g.~\cite{Leivant94:found-delin-ptime}). 
+  %
+  Implicit computational complexity on the other hand is a slightly more recent and less unified field of research. It aims to relate certain computing disciplines with complexity theoretic features, and has helped shed some light on the foundational nature of `feasibility' (see e.g.~\cite{Leivant94:found-delin-ptime}). 
   Another benefit is that implicit complexity systems can sometimes be extended into techniques for statically controlling the complexity of programs, e.g. in functional or imperative languages (e.g. \cite{Hofmann00,Hofmann03}, \cite{Marion11}).  However the variety of complexity classes that have been characterized in this implicit way is not as large as for bounded arithmetic. In particular implicit complexity has not managed to characterize non-deterministic classes, such as $\mathbf{NP}$ or $\ph$, in a purely logical way.\footnote{Actually some characterizations of such classes do exist, but they either take the form of a function algebra \cite{bellantoni1995fph} or of a type system extended with a non-logical feature \cite{GaboardiMarionRonchi12}.} 
   
- Systems in implicit complexity typically imposes constraints on the comprehension scheme, the primitive recursion scheme or the structural rules of proof systems (namely \emph{contraction}). 
+ Systems in implicit complexity typically imposes constraints on the comprehension scheme, the recursion/induction scheme or the structural rules of proof systems (namely \emph{contraction}). 
 % But it seems to us that first-order quantification has not yet been investigated as much as it deserves. We believe that this is one reason of the modest achievements of implicit complexity concerning non-deterministic classes.
 %  
   In the present work we aim to bridge the gap to bounded arithmetic by constructing `implicit' theories that characterise the functional polynomial hierarchy $\fph$ and its levels. We consider a base theory similar to that of bounded arithmetic, but we allow induction on \emph{unbounded} formulae, i.e.\ without any explicit bounds. 
@@ -24,11 +24,12 @@
 %  Our methodology will be the following one: 
 Naturally another constraint is in order, and for this we will use the concept of \textit{ramification} that is common in implicit complexity \cite{Leivant95,BellantoniCook92}.
 %, adapt it in the setting of first-order arithmetic, and then explore some properties relative to quantification. First 
-Also known as \emph{safe recursion}, ramification a discipline which aims at limiting the power of recursion by distinguishing two (or more) levels of integers: the \textit{safe} or level-0 integers (in this work $\safe$), and the \textit{normal} or level-1 ones (in this work $\normal$). 
+
+Similar to \emph{safe recursion}, ramification is a discipline which aims at limiting the power of recursion by distinguishing two (or more) levels of integers: the \textit{safe} or level-0 integers and the \textit{normal} or level-1 ones. 
 In a nutshell, recursion is permitted on normal arguments, but recursive calls can only appear in safe positions. Basic operations, such as conditionals and Boolean predicates, can be performed on safe arguments. 
 Functions defined in this way correspond to polynomial time functions \cite{BellantoniCook92}. 
   
-  This discipline can be transposed into first-order arithmetic by adding predicates for normal and safe integers and by limiting the induction scheme by allowing induction only on normal integers, but crucially on formulae with only \emph{safe} unbounded quantifiers. 
+  This discipline can be transposed into first-order arithmetic by adding predicates for normal and safe integers, in this work $\normal$ and $\safe$ respectively, and by limiting the induction scheme by allowing induction only on normal integers, but crucially with inductive invariants containing only \emph{safe} unbounded quantifiers. 
   %The key step we make is to focus our attention on \textit{safe quantifiers} that is to say quantifiers on safe variables.    
   These safe quantifiers play a r\^ole analogous to bounded quantifiers in bounded arithmetic. In particular we will consider a hierarchy $\Sigma_i^{\safe}$ of formulas, according to the number of alternations of safe quantifiers, to define a hierarchy of theories $\arith^i$ allowing induction on $\Sigma^\safe_i$ formulae. 
   We show that such a theory proves the totality of precisely the $\fph_i$ functions, relying on a recursion-theoretic characterisation of $\fph$ due to Bellantoni \cite{bellantoni1995fph} to both extract programs and prove completeness of the theory with respect to $\fph_i$.
@@ -43,18 +44,18 @@
 %   Our approach in this paper is to use the formula-specification point of view, because it is convenient for the polynomial hierarchy. 
    The arithmetic of \cite{KahOit:13:ph-levels} characterizes $\fph$, but it is not implicit, relying on axioms defining bounded schemes.
 %   Some other works are closer to our methodology in the sense that they are implicit arithmetics and rely on a notion of ramification, but they characterize other complexity classes. 
-   Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories}  induces characterizations of $\fptime$ and elementary functions, using equational specifications, and \cite{Cantini02} obtains an analogous result for $\fptime$ using combinatory terms. 
+   Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories}  induces characterizations of $\fptime$ and the Kalm\'ar elementary functions, using equational specifications, and \cite{Cantini02} obtains an analogous result for $\fptime$ using combinatory terms. 
    The paper \cite{BelHof:02} also provides a characterization of $\fptime$, with two differences: on the one hand induction is on arbitrarily quantified formulas, and on the other hand the underlying logic is not classical logic but a variant of linear logic, with a modality for normal arguments. Our paper \cite{BaillotDas16} proves a similar result, but with a different method.
    The lack of contraction is crucial here to stop the theory from exhausting higher complexity classes. 
-   Finally the paper \cite{OstrinWainer05} also presents an implicit ramified arithmetic, with quantification on safe variables. Here equational specifications are used instead of formulas and unary integers  instead of binary integers, which leads to a characterization of the elementary functions.
+   Finally the paper \cite{OstrinWainer05} also presents an implicit ramified arithmetic, with quantification on safe variables. Here equational specifications are used instead of formulas and unary integers  instead of binary integers, which leads to a characterization of the Kalm\'ar elementary functions.
   
   \medskip
   \noindent
   \textbf{Outline.} The rest of this paper proceeds as follows. We first give some background on function algebras for $\fptime$ and $\fph$ respectively in Sect.~\ref{sect:prelims}. 
   %Then we describe an encoding of sequences which will be instrumental in the proof of our result. 
-  We present our arithmetic theories $\arith^i$ in Sect.~\ref{sect:arithmetic} and prove our soundness result, that the provably total functions of $\arith^i$ are in $\fph_i$, in Sect.~\ref{sect:soundness}. Finally, we prove the completeness result, that all $\fph_i$ functions have a representation provably total in $\arith^i$, in Sect.~\ref{sect:completeness}, and present conclusions in Sect.~\ref{sect:conclusion}.
+  We present our arithmetic theories $\arith^i$ in Sect.~\ref{sect:arithmetic} and give our soundness result, that the provably total functions of $\arith^i$ are in $\fph_i$, in Sect.~\ref{sect:soundness}. Finally, we sketch the completeness result, that all $\fph_i$ functions have a representation provably total in $\arith^i$, in Sect.~\ref{sect:completeness}, and present conclusions in Sect.~\ref{sect:conclusion}.
   
-  We are able to include only brief outlines of our technical results in this paper, in particular for our soundness and completeness results, Thms.~\ref{sect:soundness} and \ref{thm:completeness} respectively. 
+  We are able to include only brief accounts of our technical results in this paper due to space constraints, in particular for our soundness and completeness results, Thms.~\ref{sect:soundness} and \ref{thm:completeness} respectively. 
   More detailed proofs can be found in the technical report \cite{BaiDas17:fph-techreport}.
   
   
