Eigenius：面向可验证科学的证明相关类型理论基础
Typed Knowledge over Constructive Institutions: A Proof-Relevant Type Theory for Verified Science
AI 导读
arXiv 论文提出 Eigenius 可验证科学知识底座的类型论与制度基础，指出 Coq、Agda、Lean 4 等证明助手的判断性证明无关性 incompatible with 可验证科学存储。
正文 · 原文
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