7 found
Sort by:
  1. Fernando Ferreira & Gilda Ferreira (forthcoming). Interpretability in Robinson's Q. Association for Symbolic Logic: The Bulletin of Symbolic Logic.
    Edward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is an impassable barrier in the totality of exponentiation. On the positive side, Nelson embarks on a program of investigating how much mathematics can be interpreted in Raphael Robinson's theory of arithmetic Q. In the shadow of this program, some very nice logical investigations and results were produced by a number of people, not only regarding what can be interpreted in Q but (...)
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  2. Fernando Ferreira & Gilda Ferreira (2013). Atomic Polymorphism. Journal of Symbolic Logic 78 (1):260-274.
    It has been known for six years that the restriction of Girard's polymorphic system $\text{\bfseries\upshape F}$ to atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait's method of “convertibility” applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each $\beta$-reduction step of the full intuitionistic propositional calculus translates into one or more $\beta\eta$-reduction steps in the restricted Girard system. As a consequence, we obtain (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  3. Gilda Ferreira & Paulo Oliva (2012). On Bounded Functional Interpretations. Annals of Pure and Applied Logic 163 (8):1030-1049.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  4. Gilda Ferreira & Paulo Oliva (2010). Confined Modified Realizability. Mathematical Logic Quarterly 56 (1):13-28.
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  5. Fernando Ferreira & Gilda Ferreira (2009). Commuting Conversions Vs. The Standard Conversions of the “Good” Connectives. Studia Logica 92 (1):63 - 84.
    Commuting conversions were introduced in the natural deduction calculus as ad hoc devices for the purpose of guaranteeing the subformula property in normal proofs. In a well known book, Jean-Yves Girard commented harshly on these conversions, saying that ‘one tends to think that natural deduction should be modified to correct such atrocities.’ We present an embedding of the intuitionistic predicate calculus into a second-order predicative system for which there is no need for commuting conversions. Furthermore, we show that the redex (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  6. Fernando Ferreira & Gilda Ferreira (2008). Harrington's Conservation Theorem Redone. Archive for Mathematical Logic 47 (2):91-100.
    Leo Harrington showed that the second-order theory of arithmetic WKL 0 is ${\Pi^1_1}$ -conservative over the theory RCA 0. Harrington’s proof is model-theoretic, making use of a forcing argument. A purely proof-theoretic proof, avoiding forcing, has been eluding the efforts of researchers. In this short paper, we present a proof of Harrington’s result using a cut-elimination argument.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  7. Fernando Ferreira & Gilda Ferreira (2006). Counting as Integration in Feasible Analysis. Mathematical Logic Quarterly 52 (3):315-320.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation