
253The myth of the mindTopoi 21 (12): 6574. 2002.Of course, I do not mean by the title of this paper to deny the existence of something called

140The completeness of Heyting firstorder logicJournal of Symbolic Logic 68 (3): 751763. 2003.Restricted to ﬁrstorder formulas, the rules of inference in the CurryHoward type theory are equivalent to those of ﬁrstorder predicate logic as formalized by Heyting, with one exception: ∃elimination in the CurryHoward theory, where ∃x : A.F (x) is understood as disjoint union, are the projections, and these do not preserve ﬁrstorderedness. This note shows, however, that the CurryHoward theory is conservative over Heyting’s system.

118There 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 secondorder logic.1 Only a narrow and arid conception of philosophy would exclude these two achievements. Thirdly and very importantly, the …Read more

117Gödel's reformulation of Gentzen's first consistency proof for arithmetic: The nocounterexample interpretationBulletin of Symbolic Logic 11 (2): 225238. 2005.The last section of “Lecture at Zilsel’s” [9, §4] contains an interesting but quite condensed discussion of Gentzen’s ﬁrst version of his consistency proof for P A [8], reformulating it as what has come to be called the nocounterexample interpretation. I will describe Gentzen’s result (in gametheoretic terms), ﬁll in the details (with some corrections) of Godel's reformulation, and discuss the relation between the two proofs.

106Against intuitionism: Constructive mathematics is part of classical mathematics (review)Journal of Philosophical Logic 12 (2). 1983.

94Gödel on intuition and on Hilbert's finitismIn Kurt Gödel, Solomon Feferman, Charles Parsons & Stephen G. Simpson (eds.), Kurt Gödel: Essays for His Centennial, Association For Symbolic Logic. 2010.There are some puzzles about G¨ odel’s published and unpublished remarks concerning finitism that have led some commentators to believe that his conception of it was unstable, that he oscillated back and forth between different accounts of it. I want to discuss these puzzles and argue that, on the contrary, G¨ odel’s writings represent a smooth evolution, with just one rather small doublereversal, of his view of finitism. He used the term “finit” (in German) or “finitary” or “finitistic” primar…Read more

86Prooftheoretic Semantics for Classical MathematicsSynthese 148 (3): 603622. 2006.We discuss the semantical categories of base and object implicit in the CurryHoward 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

73Intensional interpretations of functionals of finite type IJournal of Symbolic Logic 32 (2): 198212. 1967.

73Beyond the axioms: The question of objectivity in mathematicsPhilosophia Mathematica 9 (1): 2136. 2001.This paper contains a defense against antirealism in mathematics in the light both of incompleteness and of the fact that mathematics is a ‘cultural artifact.’. Antirealism (here) is the view that theorems, say, of aritltmetic cannot be taken at face value to express true propositions about the system of numbers but must be reconstrued to be about somctliiiig else or about nothing at all. A ‘bitethebullet’ aspect of the defease is that, adopting new axioms, liitherto independent, is not. a m…Read more

69Some recent essays in the history of the philosophy of mathematics: A critical review (review)Synthese 96 (2). 1993.

60Foundations of a General Theory of Manifolds [Cantor, 1883], which I will refer to as the Grundlagen, is Cantor’s first work on the general theory of sets. It was a separate printing, with a preface and some footnotes added, of the fifth in a series of six papers under the title of “On infinite linear point manifolds”. I want to briefly describe some of the achievements of this great work. But at the same time, I want to discuss its connection with the socalled paradoxes in set theory. There se…Read more

59The 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.

55Curtis Franks The Autonomy of Mathematical Knowledge: Hilbert's Program RevisitedHistory and Philosophy of Logic 32 (2). 2011.History and Philosophy of Logic, Volume 32, Issue 2, Page 177183, May 2011

50Noesis: Plato on exact scienceIn David B. Malament (ed.), Reading Natural Philosophy: Essays in the History and Philosophy of Science and Mathematics, Open Court. pp. 1131. 2002.

46Godel's interpretation of intuitionismPhilosophia Mathematica 14 (2): 208228. 2006.Gödel regarded the Dialectica interpretation as giving constructive content to intuitionism, which otherwise failed to meet reasonable conditions of constructivity. He founded his theory of primitive recursive functions, in which the interpretation is given, on the concept of computable function of finite type. I will (1) criticize this foundation, (2) propose a quite different one, and (3) note that essentially the latter foundation also underlies the CurryHoward type theory, and hence Heyting…Read more

39Kant and FinitismJournal of Philosophy 113 (5/6): 261273. 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

37The law of excluded middle and the axiom of choiceIn Alexander George (ed.), Mathematics and Mind, Oxford University Press. pp. 4570. 1994.

36The five questionsIn 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

35Meeting of the association for symbolic logic: Biloxi, 1979Journal of Symbolic Logic 46 (1): 191198. 1981.

30Finite Definability of NumberTheoretic Functions and Parametric Completeness of Equational CalculiZeitschrift fur mathematische Logik und Grundlagen der Mathematik 7 (15): 2838. 1961.

27A counterexample to a conjecture of Scott and SuppesJournal of Symbolic Logic 24 (1): 1516. 1959.

26The reduction of the lambda calculus to the theory of combinators in [Sch¨ onfinkel, 1924] applies to positive implicational logic, i.e. to the typed lambda calculus, where the types are built up from atomic types by means of the operation A −→ B, to show that the lambda operator can be eliminated in favor of combinators K and S of each type A −→ (B −→ A) and (A −→ (B −→ C)) −→ ((A −→ B) −→ (A −→ C)), respectively.1 I will extend that result to the case in which the types are built up by means o…Read more

26Review: J. P. Mayberry, The Foundations of Mathematics in the Theory of Sets (review)Bulletin of Symbolic Logic 8 (3): 424426. 2002.
Chicago, Illinois, United States of America