Fairouz Kamareddine

Heriot-Watt University, School of Mathematical and Computer Sciences

Abstract

In 1922, a young 21-year-old Curry started reading Principia Mathematica and was intrigued by the complications of its substitution rule. As a result of trying to analyse substitution, Curry conceived of the combinators in 1926 and started a lifelong search for powerful systems that combine computations and deductions (functions and logic) and that are able to formalise mathematics. His formalisms as well as existing complementary and competing formalisms demonstrate the struggle to internalise as much as possible while keeping the system consistent. There is also a struggle for elegant theories that minimise the number of basic concepts while remaining as close as possible to the language’s structure, and also the struggle for generalising concepts, connecting areas that may seem far apart and applying useful techniques from one area to the other.

This talk discusses two aspects of this development:

• First, we go back as far as the ancient mathematicians (and especially the Pythagorean school) and discuss how the problems/paradoxes associated with of the infinite led them to miss the opportunity of defining the real numbers and how the developments from middle ages to the 17th and 19th century led to the development of real numbers and mathematical analysis, and also to even more paradoxes that led to the birth of computability and mathematical foundations.
• Second, we discuss the problem of defining and internalising substitution in the lamba calculus and how to avoid the hurdle of how/when to introduce the substitution rule and alpha congruence. We cannot define alpha congruence without a form of substitution but for substitution and reduction to work, we need to assume a form of alpha congruence. The Curry school of thought has laid the foundations for this.

There is also a third aspect which discusses the struggle of going fully formal (especially with the variety and approaches to mechanise and formalise mathematics, e.g., in proof checkers) and keeping the informal as well as the historical tradition and lessons.

Short bio

Fairouz Kamareddine is Professor of Theoretical Computer Science in Heriot-Watt University in Scotland. Fairouz Kamareddine has been involved in a number of worldwide consultancy assignments, especially on education and research issues working for United Nations and the EU. Her research interests include Interface of Mathematics, Logic and Computer Science. She has held numerous invited positions at universities worldwide. She has well over 200 published articles and a number of books. She has played leading roles in the development, administration, and implementation of interdisciplinary, international, and academic collaborations and networks.