[FOM] Origins of type theory
urquhart at cs.toronto.edu
Thu Oct 16 19:13:09 EDT 2003
Roger Jones asks:
> The idea of logical types itself is a descendant
> of Frege's hierarchy of functions.
Can you tell us on what evidence this conclusion
I think this is fairly clear from the Frege/Russell
correspondence of 1902. Read it yourself and see if
you don't agree that Russell's ideas on types grew
out of Frege's functional hierarchy. Of course, the
final form of the theory of types is not at all like
Frege's theory (nor, for that matter, is the theory of
types of Appendix B of the Principles of Mathematics
Fregean in form or content). But the point I was making
was that Russell was led to types in the first place
by reflecting on Frege's functional hierarchy.
If you grant me this point, and also grant the
centrality of the notion of types in modern logic,
then you also have to grant the importance of
Speaking of types, isn't Frege the grand-daddy of
the lambda calculus? Frege's smooth-breathing
abstraction operator is nothing other than
Church's functional abstraction.
Why am I the only one defending our great ancestor
Frege? Come on, logicians, stop lurking!
More information about the FOM