Révision 235 CSL17/conclusions.tex

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

  		





  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.


  		





  
  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 $\fphi{i}$. 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.


  		





  6
  6
  
    
 


  		





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


  		












Formats disponibles :
  Unified diff