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.