-
37Extracting Algorithms from Intuitionistic ProofsMathematical Logic Quarterly 44 (2): 143-160. 1998.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.
-
2Feasible Operations and Applicative Theories Based on ληBulletin of Symbolic Logic 8 (4): 534. 2002.
-
26Benton, RA, 527 Blackburn, P., 281 Braüner, T., 359 Brink, C., 543Journal of Philosophical Logic 31 (615). 2002.
-
Liu, Y., B21 Massey, C., B75 Mattingley, JB, 53 Melinger, A., B11 Meseguer, E., B1Cognition 98 309. 2006.
-
22The abstract type of the real numbersArchive for Mathematical Logic 60 (7): 1005-1017. 2021.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 ap…Read more
-
15Bounds for indexes of nilpotency in commutative ring theory: A proof mining approachBulletin of Symbolic Logic 26 (3-4): 257-267. 2020.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 the f…Read more
-
23The FAN principle and weak König's lemma in herbrandized second-order arithmeticAnnals of Pure and Applied Logic 171 (9): 102843. 2020.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 …Read more
-
14Elementary Proof of Strong Normalization for Atomic FBulletin of the Section of Logic 45 (1): 1-15. 2016.We give an elementary proof of the strong normalization of the atomic polymorphic calculus Fat.
-
19Arithmetic, 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)Journal of Symbolic Logic 60 (3): 1014-1017. 1995.
-
29Mitsuru Tada and Makoto Tatsuta. The function ⌊a/m⌋ in sharply bounded arithmetic. Archive for mathematical logic, vol. 37 no. 1 , pp. 51–57 (review)Bulletin of Symbolic Logic 7 (3): 391-391. 2001.
-
39Thomas Strahm. Polynomial time operations in explicit mathematics. The journal of symbolic logic, vol. 62 , pp. 575–594. - Andrea Cantini. Feasible operations and applicative theories based on λη. Mathematical logic quarterly, vol. 46 , pp. 291–312 (review)Bulletin of Symbolic Logic 8 (4): 534-535. 2002.
-
6th Conference on Computability in Europe "Programs, Proofs, Processes"Bulletin of Symbolic Logic 17 (3): 478-479. 2011.
-
10Zigzag and Fregean ArithmeticIn Hassan Tahiri (ed.), The Philosophers and Mathematics: Festschrift for Roshdi Rashed, Springer Verlag. pp. 81-100. 2018.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 on…Read more
-
13Categoricity and Mathematical KnowledgeRevista Portuguesa de Filosofia 73 (3-4): 1423-1436. 2017.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.
-
17A herbrandized functional interpretation of classical first-order logicArchive for Mathematical Logic 56 (5-6): 523-539. 2017.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{a…Read more
-
12A Most Artistic Package of a Jumble of IdeasDialectica 62 (2): 205-222. 2008.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, dis…Read more
-
12Programs, proofs, processes: 6th Conference on Computability in Europe, CiE, 2010, Ponta Delgada, Azores, Portugal, June 30-July 4, 2010 ; proceedings (edited book, review)Springer. 2010.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.
-
On the Parmenidean misconceptionHistory of Philosophy & Logical Analysis 2. 1999.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 bounds of Parmenides…Read more
-
17Interpreting weak Kőnig's lemma in theories of nonstandard arithmeticMathematical Logic Quarterly 63 (1-2): 114-123. 2017.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.
-
17Injecting uniformities into Peano arithmeticAnnals of Pure and Applied Logic 157 (2-3): 122-129. 2009.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
-
29A Simple Proof of Parsons' TheoremNotre Dame Journal of Formal Logic 46 (1): 83-91. 2005.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
-
59The co-ordination principles: A problem for bilateralismMind 117 (468): 1051-1057. 2008.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
-
50A most artistic package of a jumble of ideasDialectica 62 (2). 2008.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, dis…Read more
-
126On the consistency of the Δ11-CA fragment of Frege's grundgesetzeJournal of Philosophical Logic 31 (4): 301-311. 2002.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 predicat…Read more
-
24Harrington’s conservation theorem redoneArchive for Mathematical Logic 47 (2): 91-100. 2008.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.
-
49Bounded Modified RealizabilityJournal of Symbolic Logic 71 (1). 2006.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