百科问答小站 logo
百科问答小站 font logo



HoTT为什么不比集合论弱? 第1页

  

user avatar   emberedison 网友的相关建议: 
      
  1. Lean4将会终止对HoTT的支持,目前来看Lean4将会更专注于传统数学形式化验证的生态位,如果你对学习类型论和HoTT有关的知识感兴趣的话建议别入坑Lean4
  2. Lean3有三大特性破坏了canonicity(正规性,但我更愿意称之为可求值性)使得其不再是构造主义的,即propositional extensionality(命题宇宙等词,对应集合论的外延公理), quotient soundness(商类型可靠,对应集合论的商集存在性), choice(选择公理)。
  3. Lean验证关于非构造命题的证明代码的具体做法是你只能在一个叫做noncomputable的子集里面间接引用破坏了canonicity的公理,在之后VM会将这些反构造主义的项用erase推理规则给擦除掉。更人话的说就是:你可以写非构造的证明代码,但你不准用这些代码来求值
  4. Lean对于非构造主义命题的自动证明推理应该也是SMT求解器,没什么特别的
  5. 冷知识:HoTT也破坏canonicity,CuTT才满足canonicity
  6. 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]没有支持更强的大基数或者反射原理的计划。

参考

  1. ^ 只不过这个无界可以不只是全体集合的势,而是某个超真类,但笔者认为企图通过这样那样的榨柠檬能榨到ZFC + Mahlo基数的水平是过于天真的
  2. ^ NF/NFU有一些特有的公理可以翻译成TST上的公理并达到可测基数的水平,某一些大数函数引用了无穷博弈或许可以达到I0的水平,某一些范畴论公理或许可以达到 Vopenka 基数的水平;但至少,通俗的说,负责编译器研发的那个主流构造主义类型论学界,没有更高的大基数需求



  

相关话题

  如何理解(证明)不存在与自己的真子集等势的自然数? 
  什么是实数? 
  如何证明一个实数的所有代表元(有理数Cauchy列)组成的集合不可数? 
  不可列个数的集合交集并集怎么定义? 
  为什么规定 0 的阶乘为 1? 
  如何证明所谓 是一个闭集? 
  如何证明下面的集合论问题? 
  为什么集合这个数学术语在麻将中没有被说明? 
  为什么规定空集是任何集合的子集,这样在数学上有什么意义? 
  若 A={x, x∉A},那么 A 是 ∅ 吗? 

前一个讨论
你觉得嘉然派蒙和原版派蒙哪个更可爱?
下一个讨论
如何评价 1 月 22 日尬魂发布的「尬魂 2S 系列」手机,有哪些值得关注的亮点和不足?





© 2024-11-09 - tinynew.org. All Rights Reserved.
© 2024-11-09 - tinynew.org. 保留所有权利