Philosophy of Mathematics as a Design Science

In the history of philosophy, much has been made of the disagreements between W. V. O. Quine and Rudolf Carnap on the nature of mathematical and scientific knowledge. But when the dust settles, the points of agreement are more substantial: mathematical and scientific reasoning are shaped by the rules of our language, and these rules are, in turn, adopted for pragmatic scientific reasons.

In this talk, I will take this perspective seriously, and regard mathematics as a system of conventions and norms that is designed to help us make sense of the world and reason efficiently. Like any designed system, it can perform well or poorly, and the philosophy of mathematics has a role to play in helping us understand the general principles by which it serves its purposes well.

To that end, I will consider models of mathematical language currently implemented in interactive theorem provers, which support the formalization and verification of mathematical theorems. Using these models, as well as reflection on ordinary mathematical practice, I will try to extract some insights as to how mathematical language works, and what makes it so effective.

Jeremy Avigad is Professor of Philosophy and Mathematical Sciences at Carnegie Mellon University. He has done work in mathematical logic, interactive theorem proving, philosophy of mathematics, history of mathematics, and automated reasoning. He is currently leading the library development for the Lean interactive theorem prover.

The Mathematics & Philosophy Lectures aim to introduce topics at the intersection of mathematics and philosophy to a general academic audience. They are sponsored by the  Departments of Philosophy and Mathematics, PIMS, the Pacific Institute for the Mathematical Sciences, and the Faculty of Science. The events are free & open to the public; a reception follows.