Switch to: References

Add citations

You must login to add citations.
  1. A note on Spector's quantifier-free rule of extensionality.Ulrich Kohlenbach - 2001 - Archive for Mathematical Logic 40 (2):89-92.
    In this note we show that the so-called weakly extensional arithmetic in all finite types, which is based on a quantifier-free rule of extensionality due to C. Spector and which is of significance in the context of Gödel"s functional interpretation, does not satisfy the deduction theorem for additional axioms. This holds already for Π0 1-axioms. Previously, only the failure of the stronger deduction theorem for deductions from (possibly open) assumptions (with parameters kept fixed) was known.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Typed lambda calculus.Henk P. Barendregt, Wil Dekkers & Richard Statman - 1977 - In Jon Barwise (ed.), Handbook of mathematical logic. New York: North-Holland. pp. 1091--1132.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • The equivalence of bar recursion and open recursion.Thomas Powell - 2014 - Annals of Pure and Applied Logic 165 (11):1727-1754.
    Several extensions of Gödel's system TT with new forms of recursion have been designed for the purpose of giving a computational interpretation to classical analysis. One can organise many of these extensions into two groups: those based on bar recursion , which include Spector's original bar recursion, modified bar recursion and the more recent products of selections functions, or those based on open recursion which in particular include the symmetric Berardi–Bezem–Coquand functional. We relate these two groups by showing that both (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations