15 found
Order:
  1.  28
    Atomic Polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - 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 (5 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  2.  16
    The Faithfulness of Fat: A Proof-Theoretic Proof.Fernando Ferreira & Gilda Ferreira - 2015 - Studia Logica 103 (6):1303-1311.
    It is known that there is a sound and faithful translation of the full intuitionistic propositional calculus into the atomic polymorphic system F at, a predicative calculus with only two connectives: the conditional and the second-order universal quantifier. The faithfulness of the embedding was established quite recently via a model-theoretic argument based in Kripke structures. In this paper we present a purely proof-theoretic proof of faithfulness. As an application, we give a purely proof-theoretic proof of the disjunction property of the (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  3.  8
    Rasiowa–Harrop Disjunction Property.Gilda Ferreira - 2017 - Studia Logica 105 (3):649-664.
    We show that there is a purely proof-theoretic proof of the Rasiowa–Harrop disjunction property for the full intuitionistic propositional calculus ), via natural deduction, in which commuting conversions are not needed. Such proof is based on a sound and faithful embedding of \ into an atomic polymorphic system. This result strengthens a homologous result for the disjunction property of \ and answers a question then posed by Pierluigi Minari.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  50
    Commuting Conversions Vs. The Standard Conversions of the “Good” Connectives.Fernando Ferreira & Gilda Ferreira - 2009 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  5.  9
    Elementary Proof of Strong Normalization for Atomic F.Fernando Ferreira & Gilda Ferreira - 2016 - Bulletin of the Section of Logic 45 (1).
    We give an elementary proof of the strong normalization of the atomic polymorphic calculus Fat.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  6.  12
    Interpretability in Robinson's Q.Fernando Ferreira & Gilda Ferreira - 2013 - Bulletin of Symbolic Logic 19 (3):289-317.
    Edward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is animpassable barrierin 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. 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 inbut also what cannot be so (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  7.  8
    Interpretability in Robinson's Q.Fernando Ferreira & Gilda Ferreira - forthcoming - 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 (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  8.  29
    Confined Modified Realizability.Gilda Ferreira & Paulo Oliva - 2010 - Mathematical Logic Quarterly 56 (1):13-28.
    We present a refinement ofthe bounded modified realizability which provides both upper and lower bounds for witnesses. Our interpretation is based on a generalisation of Howard/Bezem's notion of strong majorizability. We show how the bounded modified realizability coincides with our interpretation in the case when least elements exist . The new interpretation, however, permits the extraction of more accurate bounds, and provides an ideal setting for dealing directly with data types whose natural ordering is not well-founded.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  9.  12
    A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism.José Espírito Santo & Gilda Ferreira - 2020 - Studia Logica 108 (3):477-507.
    We study an alternative embedding of IPC into atomic system F whose translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity. As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at the levels of provability and preservation of proof identity, but it produces shorter derivations and shorter simulations of reduction sequences. Lambda-terms are employed in the technical development so that the algorithmic (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  10.  4
    The Computational Content of Atomic Polymorphism.Gilda Ferreira & Vasco T. Vasconcelos - 2019 - Logic Journal of the IGPL 27 (5):625-638.
    We show that the number-theoretic functions definable in the atomic polymorphic system are exactly the extended polynomials. Two proofs of the above result are presented: one, reducing the functions’ definability problem in ${\mathbf{F}}_{\mathbf{at}}$ to definability in the simply typed lambda calculus and the other, directly adapting Helmut Schwichtenberg’s strategy for definability in $\lambda ^{\rightarrow }$ to the atomic polymorphic setting. The uniformity granted in the polymorphic system, when compared with the simply typed lambda calculus, is emphasized.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  11.  31
    On Bounded Functional Interpretations.Gilda Ferreira & Paulo Oliva - 2012 - Annals of Pure and Applied Logic 163 (8):1030-1049.
  12.  9
    Atomic Polymorphism and the Existence Property.Gilda Ferreira - 2018 - Annals of Pure and Applied Logic 169 (12):1303-1316.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  13.  16
    Harrington’s Conservation Theorem Redone.Fernando Ferreira & Gilda Ferreira - 2008 - 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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  14.  7
    A Herbrandized Functional Interpretation of Classical First-Order Logic.Fernando Ferreira & Gilda Ferreira - 2017 - Archive for Mathematical Logic 56 (5-6):523-539.
    We introduce a new typed combinatory calculus with a type constructor that, to each type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}, associates the star type σ∗\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma ^*$$\end{document} of the nonempty finite subsets of elements of type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}. We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this star combinatory (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  15.  8
    Counting as Integration in Feasible Analysis.Fernando Ferreira & Gilda Ferreira - 2006 - Mathematical Logic Quarterly 52 (3):315-320.
    Suppose that it is possible to integrate real functions over a weak base theory related to polynomial time computability. Does it follow that we can count? The answer seems to be: obviously yes! We try to convince the reader that the severe restrictions on induction in feasible theories preclude a straightforward answer. Nevertheless, a more sophisticated reflection does indeed show that the answer is affirmative.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark