上篇文章介绍了命题逻辑、一阶逻辑再到ZFC集合论，本文来看一种新的宣称想要取代集合论在数学中地位的新东西——类型论。事实上它已经广泛运用在机器证明当中，其中最著名的就是四色定理的证明了，同时它跟程序代码很类似。把类型论稍加改造成同伦类型论，它还能比集合论更加“直接”地处理拓扑学中的许多问题。
类型论的动机
“类型”这一概念广泛被用于编程语言中，具体来说用于编译前的类型检查，比如下面这段C语言代码
1 | int i = 0; // 定义整数变量i，并将其设为0 |
编译时会报错，因为这段程序声明i是整数类型的变量，而j是字符串类型的变量，它们无法相乘，或者说，乘法运算是一个接受两个数作为输入参数，输出返回一个数的函数，这里输入的i、j的类型显然与之不匹配。从上面的例子可以看出，类型检查其实就是编译器帮助我们检查代码有没有明显的低级错误导致执行一些像把数字与字符串相乘的这种无意义的命令。虽然检查一个表达式的类型也是机械化的（可定义成形式系统），但这似乎跟数学逻辑没有一点关系，它居然能用来构建公理化体系？yugu233做过一期视频《论码农与数学家的相似性【数学地图】》非常通俗形象地解释了类型跟证明之间的联系。
