Révision 234 CSL17/conclusions.tex

conclusions.tex (revision 234)
1 1 
\section{Conclusions}
2 2 
\label{sect:conclusion}
3 3 

  		





  4
  
  
    
 We have presented a ramified arithmetic parameterized by the formulas on which induction is allowed. The hierarchy of induction formulas 


  		





  5
  
  
    
$\Sigma_i^{\safe}$ is defined by the number of alternances of safe (unbounded) quantifiers. We have proved that the system $\arith^i$ with 


  		





  6
  
  
    
$\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.


  		





  
  4
  
    
 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 


  		





  
  5
  
    
$\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.


  		





  7
  6
  
    
 


  		





  8
  
  
    
 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.


  		





  9
  
  
    
 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.


  		





  
  7
  
    
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.


  		





  
  8
  
    
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.


  		





  
  9
  
    
 


  		





  
  10
  
    
 


  		





  
  11
  
    
 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.


  		





  10
  12
  
    

  		





  11
  13
  
    
%\subsection{Why not modal?}


  		





  12
  14
  
    
%We have used a two-sorted approach, although we believe that this can be implemented as a modal approach.


  		












Formats disponibles :
  Unified diff