Colin McLarty系列讲座:Type Theories From Frege To Homotopy Type Theory

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.

发布时间:2018-08-01 16:47:56
联系我们      关于本站      版权所有© 2009-2019  北京大学哲学系逻辑、语言与认知研究中心      地址:北京大学人文学苑二号楼