William W. Tait

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 discussion in §§58-60 of the G r u n d l a g e n defends a conception of mathematical existence, to be found in Cantor (1883) and later in the writings of Dedekind and Hilbert, by basing it upon considerations about meaning which have general application, outside mathematics.2..

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 geometry; but he soon left and math then lost its luster again in the hands of teachers who neither liked nor understood it. Calculus wasn’t taught in high school in those days, or at least not in mine: besides geometry we learned some algebra and trigonometry. I doubt that even the word “ philosophy ” passed the lips of any of my teachers. My mother, who worked for a publishing house, brought home for me copies of, among other works, the Jowett translations of Plato’s Dialogues, Will Durant’s Story of Philosophy and Courant and Robbins’ What Is Mathematics?; but I can’t remember why she did that: She wasn’t at all intellectual and, as far as I recall, my interests at the time were mostly confined to sports and girls—in some order. Maybe she just thought it was time for me to develop new interests. After high school, I went in 1948 to Lehigh University, then at least primarily an engineering school, on an athletic scholarship. There I had the good fortune in my first year to have an introduction to philosophy course with Lewis White Beck. He had just moved there from the University of Delaware and shortly thereafter moved on to the University of Rochester, where he became one of the leading lights of American Kant studies. My good luck was compounded when, in my second year, Adolph Gr¨ unbaum arrived at Lehigh, fresh from graduate school at Yale, and stayed at least long enough for me to graduate, before moving to the University of Pittsburgh as Andrew Mellon Professor of Philosophy of Science..

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 equality for each type is definable in the Curry-Howard theory.