Type Theories From Frege To Homotopy Type Theory
演讲者：Colin S. McLarty
Truman P. Handy Professor of Intellectual Philosophy
Professor of Mathematics
Case Western Reserve University, USA
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.