Philosophy of Mathematics Seminar (Monday - Week 6, HT23)

It is well known that the project of Principia Mathematica (PM), which was to deliver a single system of formal logic adequate for both (i) the reduction of mathematics to logic by definitions and (ii) the formalization of all scientific reasoning, remains incomplete. But perhaps surprisingly, PM itself remains the state of the art in this project. The PM system (or the usable part of it) is extensional, and it has become increasingly clear that an extensional system will not be adequate for the formalization of all scientific reasoning, and yet no non-extensional system has been proposed to date that is capable of replicating the success (on its own terms) of the PM system. For example, the non-extensional system of Church’s “A formulation of the simple theory of types” is in many respects an improvement over the PM system, but it is so weak that, if we adopt PM’s definitions of the natural numbers, we will find that it cannot prove that 1 + 1 = 2. We propose a new non-extensional system, LF, and we argue that it can replicate the success of the PM system. We also argue that the LF is superior to set theory when it comes to the formalization of mathematics.

Meeting will be online only. Those who wish to attend, please write to Daniel Isaacson.