Lecture Series by Prof. Colin McLarty
Title: Type Theories From Frege To Homotopy Type Theory Type Theories From Frege To Homotopy Type Theory
Speaker Colin S. McLarty Truman (P. Handy Professor of Intellectual Philosophy Professor of Mathematics Case Western Reserve University)
Date and Time: Aug. 7, 9, 10, 2：30pm-5：30pm
Room: B114, Building 2 Department of Philosophy
Abstract: Type theory in logic began in Gottlob Frege's and Bertrand Russell's philosophical projects to express all of mathematics as pure logic. Russell created the explicit idea of type theory as a solution to the famous "Russell's Paradox," which showed Frege's logic was inconsistent. But this was just one of several paradoxes in the foundations of logic. The philosophical issues took decades to clarify and are not fully settled to this day. At the same time, new ideas for logic and computer science are still arising in the mathematical heritage of Russell's type theory. These lectures will look briefly Frege's and Russell's idea at the origins of type theory. We will look in more detail at versions of Simple Type Theory, category theory and Zermelo-Fraenkel set theory as type theories, and Martin-Lof's constructive Dependent Type Theory. And we will look at research uses of these in proof theory and Homotopy Type Theory.