Index: CSL17/completeness.tex
===================================================================
--- CSL17/completeness.tex	(revision 233)
+++ CSL17/completeness.tex	(revision 234)
@@ -32,7 +32,7 @@
 \right)
 \end{array}
 \]
-As for the analogous bounded arithmetic theory $S^i_2$ (\cite{Buss86book}, Thm 20, p. 58),  $\arith^i$ can prove a minimisation principle for $\cmin{\Sigma^\safe_{i-1}}$ formulas, allowing us to extract the \emph{least} witness of a safe existential, which we apply to $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$. From here we are able to readily prove the totality of $A_f(\vec u ; \vec x , z)$, notably relying crucially on classical reasoning.
+As for the analogous bounded arithmetic theory $S^i_2$ (\cite{Buss86book}, Thm 20, p. 58),  $\arith^i$ can prove a \emph{minimisation} principle for $\Sigma^\safe_{i-1}$ formulas, allowing us to extract the \emph{least} witness of a safe existential, which we apply to $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$. From here we are able to readily prove the totality of $A_f(\vec u ; \vec x , z)$, notably relying crucially on classical reasoning.
 
 \end{proof}
 
Index: CSL17/arithmetic.tex
===================================================================
--- CSL17/arithmetic.tex	(revision 233)
+++ CSL17/arithmetic.tex	(revision 234)
@@ -342,6 +342,6 @@
 \vlinf{\rigrul{\exists}}{}{\normal(\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x^\safe . A(x)}{ \normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A(t) }
 \]
 \[
-\vlinf{\lefrul{|\forall|}}{}{\normal (\vec u ) , \safe (\vec x) , s(\vec u) \leq |t(\vec u)| , \forall u^\normal \leq |t(\vec u)| . A(u) , \Gamma \seqar \Delta }{\normal (\vec u ) , \safe (\vec x) , A(t(\vec u)  ) , \Gamma \seqar \Delta  }
+\vlinf{\lefrul{|\forall|}}{}{\normal (\vec u ) , \safe (\vec x) , s(\vec u) \leq |t(\vec u)| , \forall u^\normal \leq |t(\vec u)| . A(u) , \Gamma \seqar \Delta }{\normal (\vec u ) , \safe (\vec x) , A(s(\vec u)  ) , \Gamma \seqar \Delta  }
 \]
 where, in $\rigrul{\exists}$, $(\vec u ; \vec x)$ is compatible with $t$.
Index: CSL17/conclusions.tex
===================================================================
--- CSL17/conclusions.tex	(revision 233)
+++ CSL17/conclusions.tex	(revision 234)
@@ -1,12 +1,14 @@
 \section{Conclusions}
 \label{sect:conclusion}
 
- We have presented a ramified arithmetic parameterized by the formulas on which induction is allowed. The hierarchy of induction formulas 
-$\Sigma_i^{\safe}$ is defined by the number of alternances of safe (unbounded) quantifiers. We have proved that the system $\arith^i$ with 
-$\Sigma_i^{\safe}$-induction corresponds to the $i$th level $\fphi{i}$ of the polynomial hierarchy. This result brings an implicit complexity analog of Buss' bounded arithmetic in which $S_2^i$ captures  $\fphi{i}$, and suggests that implicit arithmetics can provide fine-grained characterizations of hierarchies of complexity classes.
+ We have presented a ramified arithmetic parameterized by the number of alternations of safe (unbounded) quantifiers allowed in induction formulae. We have proved that the system $\arith^i$ with 
+$\Sigma_i^{\safe}$-induction corresponds to the $i$th level $\fphi{i}$ of the polynomial hierarchy. This result brings an implicit complexity analogue of Buss' bounded arithmetic in which $S_2^i$ captures  $\fphi{i}$, and suggests that implicit arithmetics can provide fine-grained characterizations of hierarchies of complexity classes.
  
- Several natural and interesting questions remain open. First we have   used a two-sorted logic, but we believe that this approach could be implemented with a modal logic, as in \cite{BelHof:02}. The exposition would be more complicated, but arguably more elegant.
- Second this work has provided an indirect comparison between $\arith^i$ and the bounded arithmetic $S_2^i$. We think a direct relationship could also be established, by defining an embedding of  $\arith^i$  into  $S_2^i$. This is left for future work.
+We have used a two-level ramified logic, but we believe that this approach could be implemented with a modal logic, setting $\normal = \Box \safe$, as in \cite{BelHof:02}. The exposition would be more complicated due to the lack of a developed proof theory for first-order modal logic, but arguably more elegant.
+At the same time, we could consider \emph{second-order} theories that characterise $\fph$, analogous to the bounded arithmetic theories $V^i$ from \cite{Cook:2010:LFP:1734064}, since the treatment of sequence (de)coding might be more natural, using function symbols. However it seems that delineating the levels of $\fph$ might be more difficult in such a setting.
+ 
+ 
+ This work has provided an indirect comparison between $\arith^i$ and the bounded arithmetic $S_2^i$. However, we think that a direct relationship could also be established, in particular in the form of an embedding of  $\arith^i$  into  $S_2^i$. This is left to future work.
 
 %\subsection{Why not modal?}
 %We have used a two-sorted approach, although we believe that this can be implemented as a modal approach.
