[FOM] Re: Origins of type theory

[A.P. Hazen]

     There's an irony here.  Types are an important idea in f.o.m. 
(even now), Russell introduced type theory, maybe (or better: 
probably) he was influenced by Frege.  But the types most often 
considered in modern contexts are those of SIMPLE type theory: the 
type of a function depends on the type of its arguments, not on 
complexity of its definition.  THIS notion is certainly closely 
analogous to Frege's hierarchy of objects, concepts, "second-level" 
concepts, and so on.

   (It was also to some degree anticipated by Schroeder: Church 
presented a paper on "S.'s anticipation of the simple theory of 
types" that was supposed to appear in the tenth volume of 
"Erkenntnis," but didn't because the Nazi's suppressed the journal. 
C's paper finally appeared in "Erkenntnis" 10 in 1976: pp. 407-411.)

    The sort of Type Theory considered (and rejected) by Russell in 
the appendix to "Principles of Mathematics" is similar to this. 
(Note that "the doctrine of types" is discussed in one of two 
appendices o "Principle of Mathematics," the other being a 
consideration of "the logical doctrines of Frege."  I assume that 
these are appendices because Russell became acquainted with F's work, 
and the idea of types, too late to work them into the main text, but 
Russell scholars may know better.)  The "Theory of Types" that 
Russell presented in his 1908 "Mathematical Logic as based on the 
theory of types" (repr. in Van Heijenoort), and which was used in 
"Principia Mathematica," was the RAMIFIED theory of types, in which 
the type of a function depends, not only on the types of its 
arguments, but on the types of entities referred to and quantified 
over in defining the function.  This is a theory I think is still of 
some philosophical interest (cf. Church's paper in "JSL" 1976), but 
which doesn't have a high profile in current f.o.m. literature.

     So: Frege's hierarchy stimulated Russell to discover something 
different, and something more like Frege's original version was then 
re-introduced in the 1920s by Ramsey and the Poles!

--

Allen Hazen
Philosophy Department
University of Melbourne