arXiv cs.AI· Hans-Martin Will·· 1 天前AI 评分19
Eigenius：面向可验证科学的证明相关类型论与建构性制度
Typed Knowledge over Constructive Institutions: A Proof-Relevant Type Theory for Verified Science
AI 导读
研究提出 Eigenius 可验证科学知识基座，用依赖类型内核替代 Coq、Agda、Lean 4 内建的证明无关性，使同一命题的独立推导可被检验与比较。该内核含累积宇宙（Prop、Set、Type_k）、索引强制子单例消去与内涵恒等类型，证明无关性改为带见证的命题公理，并将外部验证器组织为三级制度层级。元理论已在 Lean 4 中机械化，零 sorry 公理。
正文 · AI 翻译
摘要：Coq、Agda 和 Lean 4 等数学证明助手将证明无关性内建于定义性转换中（对于 $p, q : P$ 且 $P : Prop$，有 $p \equiv q$），从而抹去了是哪个推导确立了定理。虽然这对于基于固定公理的数学而言是自然的，但判断性证明无关性与经过验证的科学存储不兼容，后者必须检查和比较同一主张的独立推导，以评估一致性，并在检测、试剂或模型失效时计算反事实撤回。此外，将定义性证明无关性与子单例消去相结合会破坏强规范化，并使算法转换失去传递性。
我们提出了 Eigenius 的类型论与制度基础，Eigenius 是一个面向科学的经过验证的知识基底。首先，我们构建了一个依赖核，具有累积宇宙（$Prop, Set, Type_k$）、非直谓的 $Prop$、带索引强制子单例消去的归纳族以及内涵恒等类型，其中定义性相等 $\equiv$ 是在正交 CRS 下的无类型可连接性，而证明无关性是一个有见证的命题公理（$irrel : \Pi P{:}Prop.\,\Pi p,q{:}P.\,Id\,P\,p\,q$）。其次，我们将宇宙累积性、余域协变的 $\Pi$-子类型和本体类包含统一到一个无强制转换的包含判断中，其双向片段（$\mathcal{K}_0, \mathcal{K}_1$）满足主体归约，并且对于声明式类型化是可靠且完备的。第三，我们将外部验证器组织为具有显式公理策略（Adopt、Discharge、Relativize）的三级制度层次结构，内化一个带有 Why-溯源半环支持 $supp(j,P)$ 的辩护逻辑，并嵌入 Cooper 的记录类型论（TTR）来为开放世界知识图谱赋予类型。最后，我们在 Grothendieck 宇宙中证明了一致性，并在 Lean 4 中以零 sorry 公理机械化了元理论。
| 主题： | 计算机科学中的逻辑（cs.LO）；人工智能（cs.AI）；计算与语言（cs.CL） |
| ACM 分类： | F.4.1；I.2.3；I.2.4 |
| 引用为： | arXiv:2611.15108 [cs.LO] |
| （或 arXiv:2611.15108v1 [cs.LO] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2611.15108 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Hans-Martin Will [查看电子邮件]
[v1]
2026 年 11 月 11 日星期三 06:35:29 UTC（36 KB）
来源：arXiv cs.AI · arxiv.org