Abstract: The evolution of types and logic in the 20th century: A journey through Frege, Russell and other founders of modern logic and computation

Fairouz Kamareddine

Wednesday 5 May 2004.

The introduction of a general definition of function was key to Frege's formalisation of logic. Self-application of functions was at the heart of Russell's paradox. Russell introduced type theory in order to control the application of functions and hence to avoid the paradox. Since, different type systems have been introduced, each allowing different functional power. These type systems are used in many disciplines (e.g., the formal semantics of natural language, the design and implementation of programming languages and of theorem provers). The first clear and influential use of types in the semantics of natural language is due to Montague, however, Montague's system fails to capture important aspects of language (e.g., self-reference). In this talk, I will briefly review the evolution of types from the time of Euclid (325 B.C.) to the mid of the 20th century. Then, I will explain how different aspects of natural language need different power of type systems and I will establish parallels with programming languages. This talk is of interest for anyone interested in the foundation and implementation of logic, mathematics, computer science and natural or programming language.