Révision 262

CSL17/tech-report/arithmetic.tex (revision 262)
464 464 

  		





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


  		





  466
  466
  
    

  		





  467
  
  
    
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:


  		





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


  		





  468
  468
  
    
\[


  		





  469
  469
  
    
\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)}


  		





  470
  470
  
    
\quad


  		












  

    
      CSL17/tech-report/soundness.tex	(revision 262)
    
  






  37
  37
  
    
\end{definition}


  		





  38
  38
  
    

  		





  39
  39
  
    
Notice that $\leqfn (l; x,y) = 1$ just if $x \mode l \leq y \mode l$.


  		





  40
  
  
    
We can also define $\eq( l; x,y)$ as $\andfn (;\leq(l;x,y),\leq(l;y,x))$.


  		





  
  40
  
    
We can also define $\eq( l; x,y)$ as $\andfn (;\leqfn(l;x,y),\leqfn(l;y,x))$.


  		





  41
  41
  
    

  		





  42
  42
  
    
%\anupam{Do we need the general form of length-boundedness? E.g. the $*$ functions from Bellantoni's paper? Put above if necessary. Otherwise just add sequence manipulation functions as necessary.}


  		





  43
  43
  
    
%


  		












Formats disponibles :
  Unified diff