•  1
    Constructive Reasoning
    In B. van Rootselaar & Frits Staal (eds.), Logic, methodology and philosophy of science III, North-holland Pub. Co.. pp. 185-99. 1968.
  •  50
    “Finitism” (Tait 1981) presents an argument that finitist number theory is primitive recursive arithmetic (PRA). The argument is based on taking seriously the “finite” in “finitism”. But the question remained: what did Hilbert (and Bernays) mean in the early 1920’s through the early 1930’s by “finitism” and in particular, did they restrict finitist number theory to PRA. In his dissertation (Zach 2003), Richard Zach pointed out that Hilbert endorsed results as finitist that require more than PRA …Read more
  •  136
    Meeting of the Association for Symbolic Logic, Chicago, 1977
    with Carl G. Jockusch, Robert I. Soare, and Gaisi Takeuti
    Journal of Symbolic Logic 43 (3): 614-619. 1978.
  •  80
    Plato's Second Best Method
    Review of Metaphysics 39 (3). 1986.
    AT PHAEDO 96A-C Plato portrays Socrates as describing his past study of "the kind of wisdom known as περὶ φυσέως ἱστορία." At 96c-97b, Socrates says that this study led him to realize that he had an inadequate understanding of certain basic concepts which it involved. In consequence, he says at 97b, he abandoned this method and turned to a method of his own. But at this point in the dialogue, instead of proceeding immediately to describe his method, Plato has him interjecting a complaint concern…Read more
  •  155
    Kant and Finitism
    Journal of Philosophy 113 (5/6): 261-273. 2016.
    An observation and a thesis: The observation is that, whatever the connection between Kant’s philosophy and Hilbert’s conception of finitism, Kant’s account of geometric reasoning shares an essential idea with the account of finitist number theory in “Finitism”, namely the idea of constructions f from ‘arbitrary’ or ‘generic’ objects of various types. The thesis is that, contrary to a substantial part of contemporary literature on the subject, when Kant referred to number and arithmetic, he was …Read more
  •  197
    There can be no doubt about the value of Frege's contributions to the philosophy of mathematics. First, he invented quantification theory and this was the first step toward making precise the notion of a purely logical deduction. Secondly, he was the first to publish a logical analysis of the ancestral R* of a relation R, which yields a definition of R* in second-order logic.1 Only a narrow and arid conception of philosophy would exclude these two achievements. Thirdly and very importantly, the …Read more
  •  84
    The five questions
    In V. F. Hendricks & Hannes Leitgeb (eds.), Philosophy of Mathematics: Five Questions, Automatic Press/vip. 2007.
    1. A Road to Philosophy of Mathematics l became interested in philosophy and mathematics at more or less the same time, rather late in high school; and my interest in the former certainly influenced my attitude towards the latter, leading me to ask what mathematics is really about at a fairly early stage. I don ’t really remember how it was that I got interested in either subject. A very good math teacher came to my school when I was in 9th grade and I got caught up in his course on solid geomet…Read more
  •  93
    These essays present new analyses of the central figures of analytic philosophy -- Frege, Russell, Moore, Wittgenstein, and Carnap -- from the beginnings of the analytic movement into the 1930s. The papers do not reflect a single perspective, but rather express divergent interpretations of this controversial intellectual milieu.
  •  54
    Nested Recursion
    Journal of Symbolic Logic 28 (1): 103-104. 1963.
  •  339
    The last section of “Lecture at Zilsel’s” [9, §4] contains an interesting but quite condensed discussion of Gentzen’s first version of his consistency proof for P A [8], reformulating it as what has come to be called the no-counterexample interpretation. I will describe Gentzen’s result (in game-theoretic terms), fill in the details (with some corrections) of Godel's reformulation, and discuss the relation between the two proofs.
  •  74
    William Tait is one of the most distinguished philosophers of mathematics of the last fifty years. This volume collects his most important published philosophical papers from the 1980's to the present. The articles cover a wide range of issues in the foundations and philosophy of mathematics, including some on historical figures ranging from Plato to Gödel.
  •  45
    Extensional Equality in the Classical Theory of Types
    Vienna Circle Institute Yearbook 3 219-234. 1995.
    The classical theory of types in question is essentially the theory of Martin-Löf [1] but with the law of double negation elimination. I am ultimately interested in the theory of types as a framework for the foundations of mathematics and, for this purpose, we need to consider extensions of the theory obtained by adding ‘well-ordered types,’ for example the type N of the finite ordinals; but the unextended theory will suffice to illustrate the treatment of extensional equality
  •  308
    The completeness of Heyting first-order logic
    Journal of Symbolic Logic 68 (3): 751-763. 2003.
    Restricted to first-order formulas, the rules of inference in the Curry-Howard type theory are equivalent to those of first-order predicate logic as formalized by Heyting, with one exception: ∃-elimination in the Curry-Howard theory, where ∃x : A.F (x) is understood as disjoint union, are the projections, and these do not preserve firstorderedness. This note shows, however, that the Curry-Howard theory is conservative over Heyting’s system.
  •  91
    Set Existence
    with R. O. Gandy and G. Kreisel
    Journal of Symbolic Logic 27 (2): 232-233. 1962.
  •  235
    Proof-theoretic Semantics for Classical Mathematics
    Synthese 148 (3): 603-622. 2006.
    We discuss the semantical categories of base and object implicit in the Curry-Howard theory of types and we derive derive logic and, in particular, the comprehension principle in the classical version of the theory. Two results that apply to both the classical and the constructive theory are discussed. First, compositional semantics for the theory does not demand ‘incomplete objects’ in the sense of Frege: bound variables are in principle eliminable. Secondly, the relation of extensional equalit…Read more
  •  68
    The Logic of Provability (review)
    Journal of Philosophy 96 (1): 50-53. 1999.
  •  160
    History and Philosophy of Logic, Volume 32, Issue 2, Page 177-183, May 2011
  •  145
    The background of these remarks is that in 1967, in ‘’Constructive reasoning” [27], I sketched an argument that finitist arithmetic coincides with primitive recursive arithmetic, P RA; and in 1981, in “Finitism” [28], I expanded on the argument. But some recent discussions and some of the more recent literature on the subject lead me to think that a few further remarks would be useful.
  •  76
    The Palmer House Hilton Hotel, Chicago, Illinois April 19–21, 2007
    with Yiannis Moschovakis, Richmond H. Thomason, Steffen Lempp, Steve Awodey, and Jean-Pierre Marquis
    Bulletin of Symbolic Logic 13 (4). 2007.