Révision 229 CSL17/arithmetic.tex

arithmetic.tex (revision 229)
125 125 
\subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
126 126 
%Todo: $+1$,
127 127 

  		





  128
  
  
    
We say that a function $f$ is \emph{represented} by a formula $A_f$ if we can prove a formula of the form $\forall ^{\normal} \vec u, \forall ^{\safe} x, \exists^{\safe}! y. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.


  		





  
  128
  
    
We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall ^{\normal} \vec u, \forall ^{\safe} x, \exists^{\safe}! y. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.


  		





  129
  129
  
    
 


  		





  130
  130
  
    
Let us give a few examples for basic functions representable in $\arith^1$:


  		





  131
  131
  
    
\begin{itemize}


  		





  ......




  335
  335
  
    

  		





  336
  336
  
    
As we mentioned, the fact that only $\Sigma^\safe_i$ formulae occur is due to the free-cut elimination result for first-order calculi \cite{Takeuti87,Cook:2010:LFP:1734064}, which gives a form of proof where every $\cut$ step has one of its cut formulae immediately below a non-logical step. Again, we have to adapt the $\rais$ rule a little to achieve our result, due to the fact that it has a $\exists x^\normal$ in its lower sequent. For this we consider a merge of $\rais$ and $\cut$, which allows us to directly cut the upper sequent of $\rais$ against a sequent of the form $\normal(u), A(u), \Gamma \seqar \Delta$.


  		





  337
  337
  
    

  		





  338
  
  
    
Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers, e.g.\


  		





  339
  
  
    
\todo{}


  		





  
  338
  
    
Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers, although we use ones that satisfy the aforementioned constraints. For instance, we include the following rules, from which the remaining ones are similar:


  		





  
  339
  
    
\[


  		





  
  340
  
    
\vlinf{\rigrul{\forall}}{}{ \normal(\vec u) , \safe (\vec x), \Gamma \seqar \Delta , \forall x^\safe . A(x)}{\normal(\vec u ) , \safe (\vec x), \safe (x) , \Gamma \seqar \Delta, A(x)}


  		





  
  341
  
    
\quad


  		





  
  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
  
    
\]


  		





  
  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  }


  		





  
  346
  
    
\]


  		





  
  347
  
    
where, in $\rigrul{\exists}$, $(\vec u ; \vec x)$ is compatible with $t$.


  		












Formats disponibles :
  Unified diff