Switch to: Citations

Add references

You must login to add references.
  1. On the no-counterexample interpretation.Ulrich Kohlenbach - 1999 - Journal of Symbolic Logic 64 (4):1491-1511.
    In [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated ε-substitution method (due to W. Ackermann), that for every theorem A (A prenex) of first-order Peano arithmetic PA one can find ordinal recursive functionals Φ A of order type 0 which realize the Herbrand normal form A H of A. Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and cut-elimination were found. These proofs however do (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Godel's unpublished papers on foundations of mathematics.W. W. Tatt - 2001 - Philosophia Mathematica 9 (1):87-126.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • The substitution method.W. W. Tait - 1965 - Journal of Symbolic Logic 30 (2):175-192.
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • (1 other version)Functionals defined by transfinite recursion.W. W. Tait - 1965 - Journal of Symbolic Logic 30 (2):155-174.
    Download  
     
    Export citation  
     
    Bookmark   13 citations  
  • A semantics of evidence for classical arithmetic.Thierry Coquand - 1995 - Journal of Symbolic Logic 60 (1):325-337.
    Download  
     
    Export citation  
     
    Bookmark   23 citations  
  • On the interpretation of non-finitist proofs—Part I.G. Kreisel - 1951 - Journal of Symbolic Logic 16 (4):241-267.
    Download  
     
    Export citation  
     
    Bookmark   27 citations  
  • Explaining the Gentzen–Takeuti reduction steps: a second-order system.Wilfried Buchholz - 2001 - Archive for Mathematical Logic 40 (4):255-272.
    Using the concept of notations for infinitary derivations we give an explanation of Takeuti's reduction steps on finite derivations (used in his consistency proof for Π1 1-CA) in terms of the more perspicious infinitary approach from [BS88].
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • (1 other version)Update Procedures and the 1-Consistency of Arithmetic.Jeremy Avigad - 2002 - Mathematical Logic Quarterly 48 (1):3-13.
    The 1-consistency of arithmetic is shown to be equivalent to the existence of fixed points of a certain type of update procedure, which is implicit in the epsilon-substitution method.
    Download  
     
    Export citation  
     
    Bookmark   9 citations