[FOM] Origins of type theory

[Alasdair Urquhart]

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
	is based?

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
Frege's contribution.  

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!