-
290A feasible theory for analysisJournal of Symbolic Logic 59 (3): 1001-1011. 1994.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
-
265Comments on Predicative LogicJournal of Philosophical Logic 35 (1): 1-8. 2006.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 normal…Read more
-
237On End‐Extensions of Models of ¬expMathematical Logic Quarterly 42 (1): 1-18. 1996.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
-
141Amending Frege’s Grundgesetze der ArithmetikSynthese 147 (1): 3-19. 2005.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 P…Read more
-
130On 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
-
94Groundwork for weak analysisJournal of Symbolic Logic 67 (2): 557-578. 2002.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 show how to interpr…Read more
-
78A Substitutional Framework for Arithmetical ValidityGrazer Philosophische Studien 56 (1): 133-149. 1998.
-
77A note on finiteness in the predicative foundations of arithmeticJournal of Philosophical Logic 28 (2): 165-174. 1999.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 …Read more
-
67Commuting Conversions vs. the Standard Conversions of the “Good” ConnectivesStudia Logica 92 (1): 63-84. 2009.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 conversio…Read more
-
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
-
50Bounded 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
-
48Binary models generated by their tally partArchive for Mathematical Logic 33 (4): 283-289. 1994.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
-
48The bounded functional interpretation of the double negation shiftJournal of Symbolic Logic 75 (2): 759-773. 2010.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
-
47Atomic polymorphismJournal of Symbolic Logic 78 (1): 260-274. 2013.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 $…Read more
-
40Thomas 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.
-
38Extracting 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.
-
38Bounded functional interpretationAnnals of Pure and Applied Logic 135 (1): 73-112. 2005.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…Read more
-
32The Finitistic Consistency of Heck’s Predicative Fregean SystemNotre Dame Journal of Formal Logic 56 (1): 61-79. 2015.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
-
31Nonstandardness and the bounded functional interpretationAnnals of Pure and Applied Logic 166 (6): 701-712. 2015.
-
31Bounded functional interpretation and feasible analysisAnnals of Pure and Applied Logic 145 (2): 115-129. 2007.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…Read more
-
31Mitsuru 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.
-
31A 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
-
30Moscone Center West, San Francisco, CA January 15–16, 2010Bulletin of Symbolic Logic 16 (3). 2010.
-
29The Faithfulness of Fat: A Proof-Theoretic ProofStudia Logica 103 (6): 1303-1311. 2015.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-th…Read more
-
27Harrington’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.
-
26Benton, RA, 527 Blackburn, P., 281 Braüner, T., 359 Brink, C., 543Journal of Philosophical Logic 31 (615). 2002.
-
25What are the∀∑1 b-consequences of T21 and T22?Annals of Pure and Applied Logic 75 (1): 79-88. 1995.