Switch to: References

Add citations

You must login to add citations.
  1. A functional interpretation for nonstandard arithmetic.Benno van den Berg, Eyvind Briseid & Pavol Safarik - 2012 - Annals of Pure and Applied Logic 163 (12):1962-1994.
    We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Gödel and Shoenfield can be used to rewrite proofs performed in these systems into standard ones. These functional interpretations show in particular that our nonstandard systems are conservative extensions of E-HAω and E-PAω, strengthening earlier results by Moerdijk and Palmgren, and Avigad and Helzner. We will also indicate how our rewriting algorithm can be used for term extraction purposes. To conclude the (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   20 citations  
  • A note on non-classical nonstandard arithmetic.Sam Sanders - 2019 - Annals of Pure and Applied Logic 170 (4):427-445.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Factorization of the Shoenfield-like Bounded Functional Interpretation.Jaime Gaspar - 2009 - Notre Dame Journal of Formal Logic 50 (1):53-60.
    We adapt Streicher and Kohlenbach's proof of the factorization S = KD of the Shoenfield translation S in terms of Krivine's negative translation K and the Gödel functional interpretation D, obtaining a proof of the factorization U = KB of Ferreira's Shoenfield-like bounded functional interpretation U in terms of K and Ferreira and Oliva's bounded functional interpretation B.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • The abstract type of the real numbers.Fernando Ferreira - 2021 - Archive for Mathematical Logic 60 (7):1005-1017.
    In finite type arithmetic, the real numbers are represented by rapidly converging Cauchy sequences of rational numbers. Ulrich Kohlenbach introduced abstract types for certain structures such as metric spaces, normed spaces, Hilbert spaces, etc. With these types, the elements of the spaces are given directly, not through the mediation of a representation. However, these abstract spaces presuppose the real numbers. In this paper, we show how to set up an abstract type for the real numbers. The appropriateness of our construction (...)
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Nonstandardness and the bounded functional interpretation.Fernando Ferreira & Jaime Gaspar - 2015 - Annals of Pure and Applied Logic 166 (6):701-712.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  • Bounds for indexes of nilpotency in commutative ring theory: A proof mining approach.Fernando Ferreira - 2020 - Bulletin of Symbolic Logic 26 (3-4):257-267.
    It is well-known that an element of a commutative ring with identity is nilpotent if, and only if, it lies in every prime ideal of the ring. A modification of this fact is amenable to a very simple proof mining analysis. We formulate a quantitative version of this modification and obtain an explicit bound. We present an application. This proof mining analysis is the leitmotif for some comments and observations on the methodology of computational extraction. In particular, we emphasize that (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • A most artistic package of a jumble of ideas.Fernando Ferreira - 2008 - Dialectica 62 (2):205–222.
    In the course of ten short sections, we comment on Gödel's seminal dialectica paper of fifty years ago and its aftermath. We start by suggesting that Gödel's use of functionals of finite type is yet another instance of the realistic attitude of Gödel towards mathematics, in tune with his defense of the postulation of ever increasing higher types in foundational studies. We also make some observations concerning Gödel's recasting of intuitionistic arithmetic via the dialectica interpretation, discuss the extra principles that (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • The bounded functional interpretation of the double negation shift.Patrícia Engrácia & Fernando Ferreira - 2010 - Journal of Symbolic Logic 75 (2):759-773.
    We prove that the (non-intuitionistic) law of the double negation shift has a bounded functional interpretation with bar recursive functionals of finite type. As an application. we show that full numerical comprehension is compatible with the uniformities introduced by the characteristic principles of the bounded functional interpretation for the classical case.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic.Bruno Dinis & Fernando Ferreira - 2017 - Mathematical Logic Quarterly 63 (1-2):114-123.
    We show how to interpret weak Kőnig's lemma in some recently defined theories of nonstandard arithmetic in all finite types. Two types of interpretations are described, with very different verifications. The celebrated conservation result of Friedman's about weak Kőnig's lemma can be proved using these interpretations. We also address some issues concerning the collecting of witnesses in herbrandized functional interpretations.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations