[FOM] Re: Origins of type theory
a.hazen at philosophy.unimelb.edu.au
Sat Oct 18 03:13:05 EDT 2003
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!
University of Melbourne
More information about the FOM