- Lean4将会终止对HoTT的支持,目前来看Lean4将会更专注于传统数学形式化验证的生态位,如果你对学习类型论和HoTT有关的知识感兴趣的话建议别入坑Lean4
- Lean3有三大特性破坏了canonicity(正规性,但我更愿意称之为可求值性)使得其不再是构造主义的,即propositional extensionality(命题宇宙等词,对应集合论的外延公理), quotient soundness(商类型可靠,对应集合论的商集存在性), choice(选择公理)。
- Lean验证关于非构造命题的证明代码的具体做法是你只能在一个叫做noncomputable的子集里面间接引用破坏了canonicity的公理,在之后VM会将这些反构造主义的项用erase推理规则给擦除掉。更人话的说就是:你可以写非构造的证明代码,但你不准用这些代码来求值。
- Lean对于非构造主义命题的自动证明推理应该也是SMT求解器,没什么特别的
- 冷知识:HoTT也破坏canonicity,CuTT才满足canonicity
- HoTT为什么不比集合论弱,自己看HoTT book的Theorem 10.5.8,简单来说就是它们将CZF变成了HoTT的内定理,然后加上选择公理AC就复原成了ZFC
如果你问的是这个构造子是怎么想出来的或者怎么写出来的,真的不会,,,回答不了
7.Lean为什么不比集合论弱,因为pCIC(predicative Calculus of Inductive Constructions)不比集合论弱,简单来说CIC的n+2层宇宙级别可以编码ZFC + n个不可达基数。但考虑到类型论需要保持canonicity,因此类似的推广似乎无法超过Con( 个不可达基数 ),无论如何都无法越过ZFC + 无界个[1]不可达基数。目前类型论[2]没有支持更强的大基数或者反射原理的计划。
参考
- ^ 只不过这个无界可以不只是全体集合的势,而是某个超真类,但笔者认为企图通过这样那样的榨柠檬能榨到ZFC + Mahlo基数的水平是过于天真的
- ^ NF/NFU有一些特有的公理可以翻译成TST上的公理并达到可测基数的水平,某一些大数函数引用了无穷博弈或许可以达到I0的水平,某一些范畴论公理或许可以达到 Vopenka 基数的水平;但至少,通俗的说,负责编译器研发的那个主流构造主义类型论学界,没有更高的大基数需求