Workshop on History of Logics, Types and Rewriting

Heriot-Watt University, Edinburgh

Tuesday 5 December 2000

A History of Types in Logic and Mathematics

Fairouz Kamareddine

In this talk, we outline the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica (1910-1912) and Church's simply typed lambda-calculus of 1940. We first argue that types have always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's Grundgesetze der Arithmetik for which Russell derived his famous paradox that led him to introduce the first theory of types, the Ramified Type Theory rtt. We discuss how Ramsey, Hilbert and Ackermann removed the orders from rtt leading to the simple theory of types stt upon which Church's simply typed lambda calculus is based. This is joint work with Twan Laan and Rob Nederpelt.