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

时间：2018年8月7、9、10日，下午2：30-5：30

地点：北京大学哲学系（人文学苑2号楼）B114

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.