Switch to: Citations

Add references

You must login to add references.
  1. Fragments of Heyting arithmetic.Wolfgang Burr - 2000 - Journal of Symbolic Logic 65 (3):1223-1240.
    We define classes Φnof formulae of first-order arithmetic with the following properties:(i) Everyφϵ Φnis classically equivalent to a Πn-formula (n≠ 1, Φ1:= Σ1).(ii)(iii)IΠnandiΦn(i.e., Heyting arithmetic with induction schema restricted to Φn-formulae) prove the same Π2-formulae.We further generalize a result by Visser and Wehmeier. namely that prenex induction within intuitionistic arithmetic is rather weak: After closing Φnboth under existential and universal quantification (we call these classes Θn) the corresponding theoriesiΘnstill prove the same Π2-formulae. In a second part we consideriΔ0plus collection-principles. We (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   17 citations  
  • Fragments of $HA$ based on $\Sigma_1$ -induction.Kai F. Wehmeier - 1997 - Archive for Mathematical Logic 37 (1):37-49.
    In the first part of this paper we investigate the intuitionistic version $iI\!\Sigma_1$ of $I\!\Sigma_1$ (in the language of $PRA$ ), using Kleene's recursive realizability techniques. Our treatment closely parallels the usual one for $HA$ and establishes a number of nice properties for $iI\!\Sigma_1$ , e.g. existence of primitive recursive choice functions (this is established by different means also in [D94]). We then sharpen an unpublished theorem of Visser's to the effect that quantifier alternation alone is much less powerful intuitionistically (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   21 citations  
  • Basic proof theory.A. S. Troelstra - 1996 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
    This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   159 citations  
  • Stephen Bellantoni and Stephen Cook. A new recursion-theoretic characterization of the polytime functions. Computational complexity, vol. 2 , pp. 97–110. - Arnold Beckmann and Andreas Weiermann. A term rewriting characterization of the polytime functions and related complexity classes. Archive for mathematical logic, vol. 36 , pp. 11–30. [REVIEW]Karl-Heinz Niggl - 2000 - Bulletin of Symbolic Logic 6 (3):351-353.
  • Review: D. Rodding, Klassen Rekursiver Funktionen. [REVIEW]Gunter Asser - 1972 - Journal of Symbolic Logic 37 (1):196-196.
  • Fragments of HA Based on Σ 1 -Induction.Kai F. Wehmeier - 2001 - Bulletin of Symbolic Logic 7 (4):532-532.
     
    Export citation  
     
    Bookmark   5 citations