42 found
Sort by:
Disambiguations:
Fernando Ferreira [41]Fernando J. Ferreira [1]
  1. Fernando Ferreira (forthcoming). On the Notion of Object. A Logical Genealogy. On the Notion of Object. A Logical Genealogy 4 (34):609-624.
    Ferreira-Fernando_On-the-notion-of-object.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  2. Fernando Ferreira (forthcoming). 6th Conference on Computability in Europe" Programs, Proofs, Processes". Bulletin of Symbolic Logic 17 (3):478-479.
     
    My bibliography  
     
    Export citation  
  3. 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  
  4. 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  
  5. Fernando Ferreira (2012). A Short Note on Spector's Proof of Consistency of Analysis. In. In S. Barry Cooper (ed.), How the World Computes. 222--227.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  6. Fernando Ferreira, Martin Hyland, Benedikt Löwe & Elvira Mayordomo (2012). Computability in Europe 2010. Annals of Pure and Applied Logic 163 (6):621-622.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  7. Patrícia Engrácia & Fernando Ferreira (2010). The Bounded Functional Interpretation of the Double Negation Shift. 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 (5 more)  
     
    My bibliography  
     
    Export citation  
  8. Fernando Ferreira (ed.) (2010). Programs, Proofs, Processes: 6th Conference on Computability in Europe, Cie, 2010, Ponta Delgada, Azores, Portugal, June 30-July 4, 2010 ; Proceedings. [REVIEW] Springer.
    The LNCS series reports state-of-the-art results in computer science research, development, and education, at a high level and in both printed and electronic form.
    Direct download  
     
    My bibliography  
     
    Export citation  
  9. Fernando J. Ferreira, John Harrison, François Loeser, Chris Miller, Joseph S. Miller, Slawomir J. Solecki, Stevo Todorcevic & John Steel (2010). Moscone Center West, San Francisco, CA January 15–16, 2010. Bulletin of Symbolic Logic 16 (3).
    Direct download  
     
    My bibliography  
     
    Export citation  
  10. Fernando Ferreira (2009). Injecting Uniformities Into Peano Arithmetic. Annals of Pure and Applied Logic 157 (2):122-129.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  11. 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  
  12. Fernando Ferreira (2008). The Co-Ordination Principles: A Problem for Bilateralism. Mind 117 (468):1051-1057.
    In "'Yes" and "No'" (2000), Ian Rumfitt proposed bilateralism--a use-based account of the logical words, according to which the sense of a sentence is determined by the conditions under which it is asserted and denied. One of Rumfitt's key claims is that bilateralism can provide a justification of classical logic. This paper raises a techical problem for Rumfitt's proposal, one that seems to undermine the bilateralist programme.
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  13. Fernando Ferreira (2008). A Most Artistic Package of a Jumble of Ideas. Dialectica 62 (2: Table of Contents"/> Select):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 (7 more)  
     
    My bibliography  
     
    Export citation  
  14. 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  
  15. Fernando Ferreira & Paulo Oliva (2007). Bounded Functional Interpretation and Feasible Analysis. Annals of Pure and Applied Logic 145 (2):115-129.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  16. Fernando Ferreira (2006). Comments on Predicative Logic. Journal of Philosophical Logic 35 (1):1 - 8.
    We show how to interpret intuitionistic propositional logic into a predicative second-order intuitionistic propositional system having only the conditional and the universal second-order quantifier. We comment on this fact. We argue that it supports the legitimacy of using classical logic in a predicative setting, even though the philosophical cast of predicativism is nonrealistic. We also note that the absence of disjunction and existential quantifications allows one to have a process of normalization of proofs that avoids the use of "commuting conversions.".
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  17. 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  
  18. Fernando Ferreira & Ana Nunes (2006). Bounded Modified Realizability. Journal of Symbolic Logic 71 (1):329 - 346.
    We define a notion of realizability, based on a new assignment of formulas, which does not care for precise witnesses of existential statements, but only for bounds for them. The novel form of realizability supports a very general form of the FAN theorem, refutes Markov's principle but meshes well with some classical principles, including the lesser limited principle of omniscience and weak König's lemma. We discuss some applications, as well as some previous results in the literature.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  19. Fernando Ferreira (2005). Amending Frege's Grundgesetze der Arithmetik. Synthese 147 (1):3-19.
    Frege’s Grundgesetze der Arithmetik is formally inconsistent. This system is, except for minor differences, second-order logic together with an abstraction operator governed by Frege’s Axiom V. A few years ago, Richard Heck showed that the ramified predicative second-order fragment of the Grundgesetze is consistent. In this paper, we show that the above fragment augmented with the axiom of reducibility for concepts true of only finitely many individuals is still consistent, and that elementary Peano arithmetic (and more) is interpretable in this (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  20. Fernando Ferreira (2005). Amending Frege's "Grundgesetze der Arithmetik" to the Memory of Nhê (1925-2001). Synthese 147 (1):3 - 19.
    Frege's "Grundgesetze der Arithmetik" is formally inconsistent. This system is, except for minor differences, second-order logic together with an abstraction operator governed by Frege's Axiom V. A few years ago, Richard Heck showed that the ramified predicative second-order fragment of the "Grundgesetze" is consistent. In this paper, we show that the above fragment augmented with the axiom of reducibility for concepts true of only finitely many individuals is still consistent, and that elementary Peano arithmetic (and more) is interpretable in this (...)
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  21. Fernando Ferreira (2005). A Simple Proof of Parsons' Theorem. Notre Dame Journal of Formal Logic 46 (1):83-91.
    Let be the fragment of elementary Peano arithmetic in which induction is restricted to -formulas. More than three decades ago, Parsons showed that the provably total functions of are exactly the primitive recursive functions. In this paper, we observe that Parsons' result is a consequence of Herbrand's theorem concerning the -consequences of universal theories. We give a self-contained proof requiring only basic knowledge of mathematical logic.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  22. Fernando Ferreira & Paulo Oliva (2005). Bounded Functional Interpretation. Annals of Pure and Applied Logic 135 (1):73-112.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  23. António M. Fernandes & Fernando Ferreira (2002). Groundwork for Weak Analysis. Journal of Symbolic Logic 67 (2):557-578.
    This paper develops the very basic notions of analysis in a weak second-order theory of arithmetic BTFA whose provably total functions are the polynomial time computable functions. We formalize within BTFA the real number system and the notion of a continuous real function of a real variable. The theory BTFA is able to prove the intermediate value theorem, wherefore it follows that the system of real numbers is a real closed ordered field. In the last section of the paper, we (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  24. Fernando Ferreira (2002). Review: Thomas Strahm, Polynomial Time Operations in Explicit Mathematics ; Andrea Cantini, Feasible Operations and Applicative Theories Based on $\Lambda \Eta $. [REVIEW] Bulletin of Symbolic Logic 8 (4):534-535.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  25. Fernando Ferreira (2002). Strahm Thomas. Polynomial Time Operations in Explicit Mathematics. The Journal of Symbolic Logic, Vol. 62 (1997), Pp. 575–594. Cantini Andrea. Feasible Operations and Applicative Theories Based on Λη. Mathematical Logic Quarterly, Vol. 46 (2000), Pp. 291–312. [REVIEW] Bulletin of Symbolic Logic 8 (4):534-535.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  26. Fernando Ferreira & Kai F. Wehmeier (2002). On the Consistency of the Δ11-CA Fragment of Frege's Grundgesetze. Journal of Philosophical Logic 31 (4):301-311.
    It is well known that Frege's system in the Grundgesetze der Arithmetik is formally inconsistent. Frege's instantiation rule for the second-order universal quantifier makes his system, except for minor differences, full (i.e., with unrestricted comprehension) second-order logic, augmented by an abstraction operator that abides to Frege's basic law V. A few years ago, Richard Heck proved the consistency of the fragment of Frege's theory obtained by restricting the comprehension schema to predicative formulae. He further conjectured that the more encompassing Δ₁¹-comprehension (...)
    Direct download (9 more)  
     
    My bibliography  
     
    Export citation  
  27. T. Strahm, A. Cantini & Fernando Ferreira (2002). REVIEWS-Two Papers-Explicit Mathematics. Bulletin of Symbolic Logic 8 (4):534-534.
     
    My bibliography  
     
    Export citation  
  28. Fernando Ferreira (2001). Review: Mitsuru Tada, Makoto Tatsuta, The Function $Lfloor a/M Rfloor$ in Sharply Bounded Arithmetic. [REVIEW] Bulletin of Symbolic Logic 7 (3):391-391.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  29. M. Tada, M. Tatsuta & Fernando Ferreira (2001). REVIEWS-The Function (a/M) in Sharply Bounded Arithmetic. Bulletin of Symbolic Logic 7 (3):391.
     
    My bibliography  
     
    Export citation  
  30. Nicholas Denyer, Theodor Ebert, Fernando Ferreira, Richard Gaskin, Rolf George, Burkhard Hafemann, Verity Harte, Fernando Inciarte, Christoph Kann & Melissa Lane (1999). Liste der Autoren List of Contributors. Logical Analysis and History of Philosophy 2:273.
    No categories
     
    My bibliography  
     
    Export citation  
  31. Fernando Ferreira (1999). A Note on Finiteness in the Predicative Foundations of Arithmetic. Journal of Philosophical Logic 28 (2):165-174.
    Recently, Feferman and Hellman (and Aczel) showed how to establish the existence and categoricity of a natural number system by predicative means given the primitive notion of a finite set of individuals and given also a suitable pairing function operating on individuals. This short paper shows that this existence and categoricity result does not rely (even indirectly) on finite-set induction, thereby sustaining Feferman and Hellman's point in favor of the view that natural number induction can be derived from a very (...)
    Direct download (9 more)  
     
    My bibliography  
     
    Export citation  
  32. Fernando Ferreira (1999). Two General Results on Intuitionistic Bounded Theories. Mathematical Logic Quarterly 45 (3):399-407.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  33. Fernando Ferreira (1998). A Substitutional Framework for Arithmetical Validity. Grazer Philosophische Studien 56:133-149.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  34. Fernando Ferreira & António Marques (1998). Extracting Algorithms From Intuitionistic Proofs. Mathematical Logic Quarterly 44 (2):143-160.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  35. Fernando Ferreira (1997). * Exercícios Eleáticos. Disputatio.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  36. Fernando Ferreira (1996). On End‐Extensions of Models of ¬Exp. Mathematical Logic Quarterly 42 (1):1-18.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  37. Fernando Ferreira (1995). Arithmetic, Proof Theory, and Computational Complexity, Edited by Clote Peter and Jan Krajíček, Oxford Logic Guides, No. 23, Clarendon Press, Oxford University Press, Oxford and New York 1993, Xiii+ 428 Pp. [REVIEW] Journal of Symbolic Logic 60 (3):1014-1017.
    Direct download  
     
    My bibliography  
     
    Export citation  
  38. Fernando Ferreira (1995). Review: Peter Clote, Jan Krajicek, Arithmetic, Proof Theory, and Computational Complexity. [REVIEW] Journal of Symbolic Logic 60 (3):1014-1017.
    Direct download  
     
    My bibliography  
     
    Export citation  
  39. Fernando Ferreira (1995). What Are the ∀∑1b-Consequences of T21 and T22? Annals of Pure and Applied Logic 75 (1-2):79-88.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  40. Fernando Ferreira (1995). What Are the∀∑< Sub> 1< Sup> B-Consequences of< I> T< Sub> 2< Sup> 1< I> And_< I> T< Sub> 2< Sup> 2? [REVIEW] Annals of Pure and Applied Logic 75 (1):79-88.
    Direct download  
     
    My bibliography  
     
    Export citation  
  41. Fernando Ferreira (1994). A Feasible Theory for Analysis. Journal of Symbolic Logic 59 (3):1001-1011.
    We construct a weak second-order theory of arithmetic which includes Weak König's Lemma (WKL) for trees defined by bounded formulae. The provably total functions (with Σ b 1 -graphs) of this theory are the polynomial time computable functions. It is shown that the first-order strength of this version of WKL is exactly that of the scheme of collection for bounded formulae.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  42. Fernando Ferreira (1994). Binary Models Generated by Their Tally Part. Archive for Mathematical Logic 33 (4):283-289.
    We introduce a class of models of the bounded arithmetic theoryPV n . These models, which are generated by their tally part, have a curious feature: they have end-extensions or satisfyB∑ n b only in case they are closed under exponentiation. As an application, we show that if then the polynomial hierarchy does not collapse.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation