数学里的构造主义与直觉主义（一） (3-3)

等等，0∈2 是什么鬼？！计算机辩解道，根据定义，万物都是集合，首先有空集∅，然后通过 0＝∅，1＝{0}，2＝{0，1}，. . . 来定义自然数ℕ嘛。人类数学家急了，这只是自然数的集合论模型之一啊！0∈2 这种依赖于模型的东西，怎么能用来证明这么重要的定理呢？这时候，另一台计算机，用另一个自然数的集合论模型，也找到了一个黎曼猜想的证明，但是这台计算机里，自然数的模型ℕ₁是通过0＝{∅}，1＝{0}，2＝{1}，. . .来定义的。而在证明的关键一步，它用到了 0∈1，1∈2... 我们甚至没法比较两台计算机给出的证明是否相同。

在人类看来，两个自然数的模型的选取，本来是无关紧要的东西，不管怎么说，任意两个模型都是同构的嘛。对重要命题的证明不应该依赖于模型的选取，这就好像对一个关于整数的结论的证明不应该依赖于整数的十进制表示一样显然。同构的话，对一个成立的命题，可以通过同构 “搬” 到另一个上，但显然，“可以搬动的性质” 并不包括0∈2这种奇怪的东西——这又是一个没法跟计算机解释的怪现象。

§3. 从集合论到类型论 (type theory)

花开两朵，各表一枝。七十年代末，瑞典人 Martin-Löf 做出了一个重要的发现，即 algorithmic mathematics, 也就是计算机科学, 等价于只用直觉主义逻辑的数学。在 Martin-Löf 发展的构造性类型理论 (constructive type theory) 中，有以下的对应关系

第一个公式：

Programming

Program，procedure，algorithm input

output，result

⋮

α：·A

⋮

record s1：T1；s2：T2 end .

⋮

第二个公式：

Mathematics function argument value

⋮

α∈A

⋮

T1 × T2

⋮

熟悉集合论的读者应该能注意到上述表格的第一行的不寻常之处——在 Martin-Löf type theory 中，一个 “函数” 就是一个 “公式”！（只不过这个公式可以稍微复杂一点，写成一段代码或者算法而已。）这套观点完全丢弃了原来对函数的定义，X → Y的函数不再是Ⅹ × Y的一个特殊子集，而是从一个类型X的输入到一个类型Y的输出的一个计算的步骤(procedure) !

实际上，尽管离学术界广泛接受还有一定距离，type theory 其实很有适用于数学基础的潜力，并且是一个从诞生之初就适合计算机理解的数学基础。

在类型论中，“集合” 的概念被 “类型” (type) 取代，自然数、整数、有理数，都有对应的类型。乍一看这和集合论 “万物都是集合” 没啥不同，只是把 “放在一起的一堆东西” 的名字从集合 (set) 改成了类型 (type), 并且把记号α ∈ A 改成了α：A. 实际上，两者差了十万八千里——在集合论中，我们可以构造一个集合α， 和另一个集合A（两者都是从空集∅出发，用 ZFC 集合论允许的运算进行构造得到的结果，比如{∅，0，1，3} × {1，2}），再讨论

α ∈ A是否成立？

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。