Révision 166 CSL17/conclusions.tex

conclusions.tex (revision 166)
11 11 

  		





  12
  12
  
    
\anupam{By the way, Cantini asks for the provably total function of arbitrary safe induction. We kind of answer that with `PH'.}


  		





  13
  13
  
    

  		





  
  14
  
    
\anupam{Also, need some weird dual of Barcan's formula, perhaps: $\Box \exists x . A \cimp \exists x . \Box A$. This is validated by the existence of skolem functions, but syntactically requires a further axiom in the absence of comprehension.}


  		





  
  15
  
    

  		





  14
  16
  
    
\subsection{Comparison to PVi and Si2}


  		





  15
  17
  
    
We believe our theories can be embedded into their analogues, again generalising results of Bellantoni.


  		












Formats disponibles :
  Unified diff