Révision 234

CSL17/arithmetic.tex (revision 234)
342 342 
\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) }
343 343 
\]
344 344 
\[
345 
\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  }
345 
\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  }
346 346 
\]
347 347 
where, in $\rigrul{\exists}$, $(\vec u ; \vec x)$ is compatible with $t$.
CSL17/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.


  		












  

    
      CSL17/completeness.tex	(revision 234)
    
  






  32
  32
  
    
\right)


  		





  33
  33
  
    
\end{array}


  		





  34
  34
  
    
\]


  		





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


  		





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


  		





  36
  36
  
    

  		





  37
  37
  
    
\end{proof}


  		





  38
  38
  
    

  		












Formats disponibles :
  Unified diff