Switch to: Citations

Add references

You must login to add references.
  1. Epistemic and intuitionistic formal systems.R. C. Flagg & H. Friedman - 1986 - Annals of Pure and Applied Logic 32:53-60.
    Download  
     
    Export citation  
     
    Bookmark   17 citations  
  • Shoenfield is Gödel after Krivine.Thomas Streicher & Ulrich Kohlenbach - 2007 - Mathematical Logic Quarterly 53 (2):176-179.
    We show that Shoenfield's functional interpretation of Peano arithmetic can be factorized as a negative translation due to J. L. Krivine followed by Gödel's Dialectica interpretation. (© 2007 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim).
    Download  
     
    Export citation  
     
    Bookmark   16 citations  
  • A Note on the Godel-Gentzen Translation.Hajime Ishihara - 2000 - Mathematical Logic Quarterly 46 (1):135-138.
    We give a variant of the Gödel-Gentzen-negative translation, and a syntactic characterization which entails conservativity result for formulas.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • The collected papers of Gerhard Gentzen.Gerhard Gentzen - 1969 - Amsterdam,: North-Holland Pub. Co.. Edited by M. E. Szabo.
    Download  
     
    Export citation  
     
    Bookmark   114 citations  
  • Opérateurs de mise en mémoire et traduction de Gödel.Jean-Louis Krivine - 1990 - Archive for Mathematical Logic 30 (4):241-267.
    Inλ-calculus, the strategy of leftmost reduction (“call-by-name”) is known to have good mathematical properties; in particular, it always terminates when applied to a normalizable term. On the other hand, with this strategy, the argument of a function is re-evaluated at each time it is used.To avoid this drawback, we define the notion of “storage operator”, for each data type. IfT is a storage operator for integers, for example, let us replace the evaluation, by leftmost reduction, ofϕτ (whereτ is an integer, (...)
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  • Refined program extraction from classical proofs.Ulrich Berger, Wilfried Buchholz & Helmut Schwichtenberg - 2002 - Annals of Pure and Applied Logic 114 (1-3):3-25.
    The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form ∀x∃yB . We also generalize previously known results, since B no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “goal formulas”. Furthermore we allow unproven lemmas D in the proof of ∀x∃yB , where D is a so-called “definite” formula.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik.Gerhard Gentzen - 1974 - Archive for Mathematical Logic 16 (3-4):119-132.
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • ASH, CJ, Stability of recursive structures in arithmetical degrees BLASS, A. and GUREVICH, Y., Henkin quantifiers and complete problems BUCHHOLZ, W., A new system of proof-theoretic ordinal functions. [REVIEW]H. Friedman & Rc Flagg - 1986 - Annals of Pure and Applied Logic 32 (C):299.
    Download  
     
    Export citation  
     
    Bookmark   9 citations