Special Event In Memory of Martin Davis

Computability and Unsolvability

Time and Location:

Jan. 26, 2024 at 2PM; Warren Weaver Hall, Room 109

Speaker:

Wilfried Sieg, Carnegie Mellon University

Abstract:

Computability and Unsolvability is the title of Martin Davis’ classic textbook that was published in 1958. I read parts of the book when I was a student of mathematical logic; I have used it as a central text in a course proving unsolvability theorems, for more than 20 years. The book’s very title points to a deep methodological problem: What are the computational means that can be shown not to solve particular problems? How can one characterize computations in a mathematically precise and most general way, thus determine what is computable?

Martin Davis decisively contributed to the clarification of this methodological problem. His insistence on joining Alan Turing’s and Emil Post’s approaches to the problem opened a path to addressing it in a novel, mathematically illuminating way. This is, it seems to me, a fundamental part of the modern history of ideas; it concerns computer science, artificial intelligence, and computational sciences – that are having such a dramatic impact on contemporary society.

Notes:

Speaker Bio: Wilfried Sieg is Patrick Suppes Professor of Logic & Philosophy at Carnegie Mellon University and a Fellow of the American Academy of Arts and Sciences as well as of the American Association for the Advancement of Science. He received his Ph.D. from Stanford University in 1977. From 1977 to 1985, he was Assistant and Associate Professor at Columbia University. He joined the Carnegie Mellon Faculty in 1985 as a founding member of the University’s Philosophy Department; he served as its Head from 1994 to 2005.

He is internationally known for mathematical work in proof theory, historical work on the emergence of modern mathematics and logic, analyses of the concept of computability, and philosophical essays on the nature of mathematics. Over the last three decades he has developed novel methods for human-centered automated proof search. These methods have been implemented in web-based courses to teach proof construction in logic and elementary set theory; indeed, they are used to support the active learning of individual students.