47 found
Order:
Disambiguations
Fernando Ferreira [56]Fernando J. Ferreira [1]
  1.  45
    Bounded functional interpretation.Fernando Ferreira & Paulo Oliva - 2005 - Annals of Pure and Applied Logic 135 (1):73-112.
    We present a new functional interpretation, based on a novel assignment of formulas. In contrast with Gödel’s functional “Dialectica” interpretation, the new interpretation does not care for precise witnesses of existential statements, but only for bounds for them. New principles are supported by our interpretation, including the FAN theorem, weak König’s lemma and the lesser limited principle of omniscience. Conspicuous among these principles are also refutations of some laws of classical logic. Notwithstanding, we end up discussing some applications of the (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   35 citations  
  2. On the consistency of the Δ11-CA fragment of Frege's grundgesetze.Fernando Ferreira & Kai F. Wehmeier - 2002 - 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 (6 more)  
     
    Export citation  
     
    Bookmark   33 citations  
  3. A feasible theory for analysis.Fernando Ferreira - 1994 - 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 (8 more)  
     
    Export citation  
     
    Bookmark   20 citations  
  4.  67
    The co-ordination principles: A problem for bilateralism.Fernando Ferreira - 2008 - 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.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   18 citations  
  5.  43
    Comments on Predicative Logic.Fernando Ferreira - 2006 - 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 (4 more)  
     
    Export citation  
     
    Bookmark   16 citations  
  6.  53
    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   9 citations  
  7.  35
    Nonstandardness and the bounded functional interpretation.Fernando Ferreira & Jaime Gaspar - 2015 - Annals of Pure and Applied Logic 166 (6):701-712.
  8.  29
    The FAN principle and weak König's lemma in herbrandized second-order arithmetic.Fernando Ferreira - 2020 - Annals of Pure and Applied Logic 171 (9):102843.
    We introduce a herbrandized functional interpretation of a first-order semi-intuitionistic extension of Heyting Arithmetic and study its main properties. We then extend the interpretation to a certain system of second-order arithmetic which includes a (classically false) formulation of the FAN principle and weak König's lemma. It is shown that any first-order formula provable in this system is classically true. It is perhaps worthy of note that, in our interpretation, second-order variables are interpreted by finite sets of natural numbers.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  9.  21
    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 (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  10.  47
    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   10 citations  
  11.  34
    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   6 citations  
  12.  17
    Zigzag and Fregean Arithmetic.Fernando Ferreira - 2018 - In Hassan Tahiri (ed.), The Philosophers and Mathematics: Festschrift for Roshdi Rashed. Cham: Springer Verlag. pp. 81-100.
    In Frege’s logicism, numbers are logical objects in the sense that they are extensions of certain concepts. Frege’s logical system is inconsistent, but Richard Heck showed that its restriction to predicative quantification is consistent. This predicative fragment is, nevertheless, too weak to develop arithmetic. In this paper, I will consider an extension of Heck’s system with impredicative quantifiers. In this extended system, both predicative and impredicative quantifiers co-exist but it is only permissible to take extensions of concepts formulated in the (...)
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  13.  27
    Injecting uniformities into Peano arithmetic.Fernando Ferreira - 2009 - Annals of Pure and Applied Logic 157 (2-3):122-129.
    We present a functional interpretation of Peano arithmetic that uses Gödel’s computable functionals and which systematically injects uniformities into the statements of finite-type arithmetic. As a consequence, some uniform boundedness principles are interpreted while maintaining unmoved the -sentences of arithmetic. We explain why this interpretation is tailored to yield conservation results.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  14. Groundwork for weak analysis.António M. Fernandes & Fernando Ferreira - 2002 - 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 (8 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  15.  57
    Bounded Modified Realizability.Fernando Ferreira & Ana Nunes - 2006 - 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 (5 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  16.  59
    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   5 citations  
  17.  36
    Bounded functional interpretation and feasible analysis.Fernando Ferreira & Paulo Oliva - 2007 - Annals of Pure and Applied Logic 145 (2):115-129.
    In this article we study applications of the bounded functional interpretation to theories of feasible arithmetic and analysis. The main results show that the novel interpretation is sound for considerable generalizations of weak König’s Lemma, even in the presence of very weak induction. Moreover, when this is combined with Cook and Urquhart’s variant of the functional interpretation, one obtains effective versions of conservation results regarding weak König’s Lemma which have been so far only obtained non-constructively.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  18.  27
    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  
  19.  18
    (1 other version)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   3 citations  
  20.  22
    Elementary Proof of Strong Normalization for Atomic F.Fernando Ferreira & Gilda Ferreira - 2016 - Bulletin of the Section of Logic 45 (1):1-15.
    We give an elementary proof of the strong normalization of the atomic polymorphic calculus Fat.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  21. Amending Frege’s Grundgesetze der Arithmetik.Fernando Ferreira - 2005 - 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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  22. On End‐Extensions of Models of ¬exp.Fernando Ferreira - 1996 - Mathematical Logic Quarterly 42 (1):1-18.
    Every model of IΔ0 is the tally part of a model of the stringlanguage theory Th-FO . We show how to “smoothly” introduce in Th-FO the binary length function, whereby it is possible to make exponential assumptions in models of Th-FO. These considerations entail that every model of IΔ0 + ¬exp is a proper initial segment of a model of Th-FO and that a modicum of bounded collection is true in these models.
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  23.  39
    A Simple Proof of Parsons' Theorem.Fernando Ferreira - 2005 - 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)  
     
    Export citation  
     
    Bookmark   3 citations  
  24.  22
    (1 other version)What are the ∀∑1 b-consequences of T 2 1 and T 2 2?Fernando Ferreira - 1995 - Annals of Pure and Applied Logic 75 (1):79-88.
    We formulate schemes and of the “typical” ∀∑ 1 b -sentences that are provable in T 2 1, respectively T 2 2. As an application, we reprove a recent result of Buss and Krajíček which describes witnesses for the ∀∑ 1 b -sentences provable in T 2 1 in terms of solutions to PLS-problems.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  25.  57
    Binary models generated by their tally part.Fernando Ferreira - 1994 - 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.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  26.  38
    The Finitistic Consistency of Heck’s Predicative Fregean System.Luís Cruz-Filipe & Fernando Ferreira - 2015 - Notre Dame Journal of Formal Logic 56 (1):61-79.
    Frege’s theory is inconsistent. However, the predicative version of Frege’s system is consistent. This was proved by Richard Heck in 1996 using a model-theoretic argument. In this paper, we give a finitistic proof of this consistency result. As a consequence, Heck’s predicative theory is rather weak. We also prove the finitistic consistency of the extension of Heck’s theory to $\Delta^{1}_{1}$-comprehension and of Heck’s ramified predicative second-order system.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  27.  61
    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  
  28.  17
    A new computation of the σ-ordinal of KPω.Fernando Ferreira - 2014 - Journal of Symbolic Logic 79 (1):306-324.
  29.  86
    A note on finiteness in the predicative foundations of arithmetic.Fernando Ferreira - 1999 - 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 (6 more)  
     
    Export citation  
     
    Bookmark  
  30.  7
    A Substitutional Framework for Arithmetical Validity.Fernando Ferreira - 1998 - Grazer Philosophische Studien 56 (1):133-149.
  31.  20
    A short note on Spector's proof of consistency of analysis.Fernando Ferreira - 2012 - In S. Barry Cooper (ed.), How the World Computes. pp. 222--227.
    Direct download  
     
    Export citation  
     
    Bookmark  
  32.  19
    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 theleitmotiffor some comments and observations on the methodology of computational extraction. In particular, we emphasize that the formulation (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  33.  19
    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  
     
    Export citation  
     
    Bookmark  
  34.  19
    Categoricity and Mathematical Knowledge.Fernando Ferreira - 2017 - Revista Portuguesa de Filosofia 73 (3-4):1423-1436.
    We argue that the basic notions of mathematics can only be properly formulated in an informal way. Mathematical notions transcend formalizations and their study involves the consideration of other mathematical notions. We explain the fundamental role of categoricity theorems in making these studies possible. We arrive at the conclusion that the enterprise of mathematics is not infallible and that it ultimately relies on degrees of evidence.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  35.  31
    Computability in Europe 2010.Fernando Ferreira, Martin Hyland, Benedikt Löwe & Elvira Mayordomo - 2012 - Annals of Pure and Applied Logic 163 (6):621-622.
  36.  40
    Extracting Algorithms from Intuitionistic Proofs.Fernando Ferreira & António Marques - 1998 - Mathematical Logic Quarterly 44 (2):143-160.
    This paper presents a new method - which does not rely on the cut-elimination theorem - for characterizing the provably total functions of certain intuitionistic subsystems of arithmetic. The new method hinges on a realizability argument within an infinitary language. We illustrate the method for the intuitionistic counterpart of Buss's theory Smath image, and we briefly sketch it for the other levels of bounded arithmetic and for the theory IΣ1.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  37.  9
    Exercícios Eleáticos.Fernando Ferreira - 1997 - Disputatio 1 (2):2-21.
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  38.  35
    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 (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  39.  39
    On the Notion of Object. A Logical Genealogy.Fernando Ferreira - 2012 - Disputatio 4 (34):609-624.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  40. (1 other version)On the Parmenidean misconception.Fernando Ferreira - 1999 - History of Philosophy & Logical Analysis 2.
    This paper makes two main claims. Firstly, it imputes to Parmenides a misconception rooted in an erroneous theory of the meaning of sentences. In Parmenides' hands, this theory took the extreme form not only of being unable to make sense of falsehoods, but also of being unable to make sense of true negative predications. Secondly, it claims that Plato's double theory of "limited mixing" plus "negation as otherness" - as expounded in the Sophist - is a theory still within the (...)
     
    Export citation  
     
    Bookmark   1 citation  
  41.  32
    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  
  42.  20
    Two General Results on Intuitionistic Bounded Theories.Fernando Ferreira - 1999 - Mathematical Logic Quarterly 45 (3):399-407.
    We study, within the framework of intuitionistic logic, two well-known general results of bounded arithmetic. Firstly, Parikh's theorem on the existence of bounding terms for the provably total functions. Secondly, the result which states that adding the scheme of bounded collection to bounded theories does not yield new II2 consequences.
    Direct download  
     
    Export citation  
     
    Bookmark  
  43.  21
    (1 other version)Arithmetic, proof theory, and computational complexity, edited by Peter Clote and Krajíček Jan, Oxford logic guides, no. 23, Clarendon Press, Oxford University Press, Oxford and New York1993, xiii + 428 pp. [REVIEW]Fernando Ferreira - 1995 - Journal of Symbolic Logic 60 (3):1014-1017.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  44.  28
    (1 other version)Mitsuru Tada and Makoto Tatsuta. The function ⌊a/m⌋ in sharply bounded arithmetic. Archive for mathematical logic, vol. 37 no. 1 , pp. 51–57. [REVIEW]Fernando Ferreira - 2001 - Bulletin of Symbolic Logic 7 (3):391-391.
  45.  14
    Programs, proofs, processes: 6th Conference on Computability in Europe, CiE, 2010, Ponta Delgada, Azores, Portugal, June 30-July 4, 2010 ; proceedings.Fernando Ferreira (ed.) - 2010 - New York: 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  
     
    Export citation  
     
    Bookmark  
  46.  16
    (1 other version)Review: Thomas Strahm, Polynomial Time Operations in Explicit Mathematics ; Andrea Cantini, Feasible Operations and Applicative Theories Based on $\lambda \eta $. [REVIEW]Fernando Ferreira - 2002 - Bulletin of Symbolic Logic 8 (4):534-535.
  47.  6
    (1 other version)Two papers by T. Strahm and by A. Cantini on explicit mathematics. [REVIEW]Fernando Ferreira - 2002 - Bulletin of Symbolic Logic 8 (4):534-534.