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 公理。
正文 · 原文
Abstract:Mathematical proof assistants such as Coq, Agda, and Lean 4 build proof irrelevance into definitional conversion ($p \equiv q$ for $p, q : P$ with $P : Prop$), erasing which derivation established a theorem. While natural for mathematics over fixed axioms, judgmental proof irrelevance is incompatible with verified scientific stores, which must inspect and compare independent derivations of the same claim to assess consilience and compute counterfactual retractions when an assay, reagent, or model is invalidated. Moreover, combining definitional proof irrelevance with subsingleton elimination breaks strong normalization and renders algorithmic conversion non-transitive.
We present the type-theoretic and institutional foundations of Eigenius, a verified knowledge substrate for science. First, we formulate a dependent kernel with cumulative universes ($Prop, Set, Type_k$), impredicative $Prop$, inductive families with index-forced subsingleton elimination, and intensional identity types, where definitional equality $\equiv$ is untyped joinability under an orthogonal CRS and proof irrelevance is a witnessed propositional axiom ($irrel : \Pi P{:}Prop.\,\Pi p,q{:}P.\,Id\,P\,p\,q$). Second, we unify universe cumulativity, codomain-covariant $\Pi$-subtyping, and ontology class inclusions in a coercion-free subsumption judgment whose bidirectional fragments ($\mathcal{K}_0, \mathcal{K}_1$) satisfy subject reduction and are sound and complete for declarative typing. Third, we organize external verifiers into a three-level institutional hierarchy with explicit axiom policies (Adopt, Discharge, Relativize), internalize a justification logic with Why-provenance semiring support $supp(j,P)$, and embed Cooper's Type Theory with Records (TTR) to type open-world knowledge graphs. Finally, we prove consistency in Grothendieck universes and mechanize the metatheory in Lean 4 with zero sorry axioms.
| Subjects: | Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Computation and Language (cs.CL) |
| ACM classes: | F.4.1; I.2.3; I.2.4 |
| Cite as: | arXiv:2611.15108 [cs.LO] |
| (or arXiv:2611.15108v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2611.15108 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Hans-Martin Will [view email]
[v1]
Wed, 11 Nov 2026 06:35:29 UTC (36 KB)
来源：arXiv cs.AI · arxiv.org