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

4. 让计算机理解集合论并没有文中说的那么困难，参见 Mizar system —— A proof assistant based on first-order logic, in a natural deduction style, and Tarski–Grothendieck set theory. (Tarski-Grothendieck set theory 是 ZFC 的一个 non-conservertive extension, 添加了 Tarski 公理：对任意一个集合x存在一个 Grothendieck universeU使得x∈U.)

5. 可能有读者会问 type theory 里这套 Programming 和 Mathematics 的对应和所谓的 Curry-Howard Isomorphism 有什么区别和联系, 实际上上述对应相当于把 Curry-Howard isomorphism 扩展到了 dependent type theory. 相当于 Curry–Howard isomorphism 加上了谓词逻辑的的强化版。

6. 集合论的 extensionality 公理的推论之一是，对于两个集合之间的函数f，g：X → Y，f＝g ⇔ ∀x ∈ X，f(x)＝g(x)：因为作为X × Y的子集，f，g的图像Γf，Γg在函数值完全相当的时候完全重合，所以作为集合相等。

7. 用不严谨的话讲，加入了 univalence axiom 的 type theory, 叫 homotopy type theory. 我故意在正文里避开了这个词。

8. Jacob Lurie 以集合论为基础来定义(∞，1)-groupoid，做了很重要的工作，但他的工作与 homotopy type theory 无关。窃认为 Jacob Lurie 工作的困难程度可以反过来说明 homotopy type theory 的重要性。

§6. 参考

1. 关于构造主义的一个比较耐读的参考 (40 pp.): Constructive Mathematics in Theory and Programming Practice, Douglas BRIDGES and Steve REEVES

2. Constructive Mathematics (Stanford Encyclopedia of Philosophy)

3. 有一定数学背景，且对 Homotopy type theory 有兴趣的读者很有必要看看这三个 slides：

• /~coquan...

• /~coquan...

• /~coquan...

（题图：Wikipedia File：Logic.svg）

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