William W. Tait

“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 for their proofs. Tait 2002 and tait2005 argue that it is not clear that Hilbertwas aware that these results go beyond PRA. But that view is challenged in more recent times in Sieg/Ravaglia 2005 and by the editors of (the invaluable!) David Hilbert’s Lectures on the Foundations of Arithmetic and Logic 1917-1933 (Hilbert 2013). I will survey the old ground and then discuss the new challenge, which claims that, from the early 1920’s on, Hilbert accepted as finitist an enumeration function of the primitive recursive functions (which of course is not primitive recursive). The grounds for this are a reading of a passage in §7 of Grundlagen der Mathematik I and an argument for the consistency of PRA which goes back to 1922-1923 and is elaborated again in §7 of Grundlagen der Mathematik I. I will argue that their reading of the passage in question is a misreading and that the argument for the consistency of PRA uses, not an enumeration function for the primitive recursive functions, but rather mathematical induction on a Π02 predicate (i.e. of the form ∀x∃yϕ(x, y)), which was explicitly rejected by Hilbert as finitist - e.g. notably in Hilbert 1926.

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.

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 Curry-Howard type theory, and hence Heyting's intuitionistic conception of logic. Thus the Dialectica interpretation (in so far as its aim was to give constructive content to intuitionism) is superfluous.

Foundations 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 so-called paradoxes in set theory. There seems to be some agreement now that Cantor’s own understanding of the theory of transfinite numbers in that monograph did not contain an implicit contradiction; but there is less agreement about exactly why this is so and about the content of the theory itself. For various reasons, both historical and internal, the Grundlagen seems not to have been widely read compared to later works of Cantor, and to have been even less well understood. But even some of the more recent discussions of the work, while recognizing to some degree its unique character, misunderstand it on crucial points and fail to convey its true worth.