Switch to: References

Add citations

You must login to add citations.
  1. Elementary arithmetic.Geoffrey E. Ostrin & Stanley S. Wainer - 2005 - Annals of Pure and Applied Logic 133 (1):275-292.
    There is a very simple way in which the safe/normal variable discipline of Bellantoni–Cook recursion [S. Bellantoni, S. Cook, A new recursion theoretic characterization of the polytime functions, Computational Complexity 2 97–110] can be imposed on arithmetical theories like PA: quantify over safes and induct on normals. This weakens the theory severely, so that the provably recursive functions become more realistically computable . Earlier results of D. Leivant [Intrinsic theories and computational complexity, in: D. Leivant , Logic and Computational Complexity, (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Provably recursive functions of constructive and relatively constructive theories.Morteza Moniri - 2010 - Archive for Mathematical Logic 49 (3):291-300.
    In this paper we prove conservation theorems for theories of classical first-order arithmetic over their intuitionistic version. We also prove generalized conservation results for intuitionistic theories when certain weak forms of the principle of excluded middle are added to them. Members of two families of subsystems of Heyting arithmetic and Buss-Harnik’s theories of intuitionistic bounded arithmetic are the intuitionistic theories we consider. For the first group, we use a method described by Leivant based on the negative translation combined with a (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Homomorphisms and chains of Kripke models.Morteza Moniri & Mostafa Zaare - 2011 - Archive for Mathematical Logic 50 (3-4):431-443.
    In this paper we define a suitable version of the notion of homomorphism for Kripke models of intuitionistic first-order logic and characterize theories that are preserved under images and also those that are preserved under inverse images of homomorphisms. Moreover, we define a notion of union of chain for Kripke models and define a class of formulas that is preserved in unions of chains. We also define similar classes of formulas and investigate their behavior in Kripke models. An application to (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Extracting Algorithms from Intuitionistic Proofs.Fernando Ferreira & António Marques - 1998 - Mathematical Logic Quarterly 44 (2):143-160.
    This paper presents a new method - which does not rely on the cut-elimination theorem - for characterizing the provably total functions of certain intuitionistic subsystems of arithmetic. The new method hinges on a realizability argument within an infinitary language. We illustrate the method for the intuitionistic counterpart of Buss's theory Smath image, and we briefly sketch it for the other levels of bounded arithmetic and for the theory IΣ1.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Quick cut-elimination for strictly positive cuts.Toshiyasu Arai - 2011 - Annals of Pure and Applied Logic 162 (10):807-815.
    In this paper we show that the intuitionistic theory for finitely many iterations of strictly positive operators is a conservative extension of Heyting arithmetic. The proof is inspired by the quick cut-elimination due to G. Mints. This technique is also applied to fragments of Heyting arithmetic.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations