Eigenius：为数学证明构建带类型知识库的理论框架

当证明不再“匿名”：知识持久化对类型论的挑战

在数学形式化和程序验证领域，类型论的设计目标通常很纯粹：只关心命题是否成立。证明无关性（proof irrelevance）作为转换规则时，会在内核层面抹去“这个命题是如何被建立的”这一信息。换句话说，两个不同的证明项只要证明同一个命题，在转换时就被视为相等，推导过程、外部工具的参与、依赖的假设统统消失。

但一个持久化的知识存储不能这样。它需要记录：谁建立了这个断言、通过哪条推导或哪个外部工具、在何种假设下成立。这正是《Typed Knowledge over Constructive Institutions》一书要解决的问题。该书提出了 Eigenius 的理论——一个建立在构造性制度（constructive institutions）之上的带类型知识存储，并从这一需求出发发展其元理论。

内核设计：证明无关性作为公理而非转换规则

Eigenius 的内核是一个依赖类型论，包含累积宇宙（cumulative universes）、命题的非直谓宇宙（impredicative universe of propositions）、归纳族（inductive families）以及内涵身份类型（intensional identity type）。

关键设计在于：证明无关性被设定为一条带显式见证（explicit witness）的公理，而不是转换规则。这意味着，一个命题的两个证明虽然可证明相等，但仍然是不同的项——内核可以区分它们。这一改动看似细微，却为追踪证据来源保留了空间。

定义相等性（definitional equality）通过正交重写系统（orthogonal rewriting system）下的可连接性（joinability）来刻画。该系统是合流的（confluent）、在类型构造器上单射（injective on type formers），并且可通过一个无类型测试（type-free test）来判定。此外，一个独立的包含判断（subsumption judgment）处理宇宙累积性、余域协变的函数类型（codomain-covariant function types）以及声明的类包含（declared class inclusions）。

**证明无关性（proof irrelevance）**在类型论中有两种常见处理方式：作为转换规则（conversion rule）时，类型检查器在判断两个证明项是否相等时会直接忽略其内部结构，只要它们证明同一命题就视为可互换；作为公理时，则需显式声明“若 p 和 q 都证明命题 A，则 p = q”，且该等式证明本身是一个需要被构造和追踪的项。Eigenius 选择后者，意味着证明相等性不再是类型检查的隐式副作用，而是一个有见证的断言。这类似于在数据库中把“两条记录指向同一实体”从硬编码的去重逻辑改为一条可审计的合并记录。

**正交重写系统（orthogonal rewriting system）**是一类满足左线性（每个变量在左侧至多出现一次）且无临界对（critical pairs）的重写系统，其合流性可由正交性直接保证，无需额外验证。Eigenius 用可连接性（joinability）刻画定义相等性：两个项定义相等当且仅当它们能重写到同一个公共项。由于该系统正交且可判定，类型检查器可以通过一个无类型测试来判定相等性，而不必依赖复杂的归约策略。

元理论：一致性、证据追踪与制度组织

作者从多个层面构建了 Eigenius 的元理论。首先，通过集合论模型证明了系统的一致性（consistency）。其次，在内核命题之上发展了一种证成逻辑（justification logic），用来追踪证据和支持关系。

环境被组织为一个制度（institution），存储扩展（store extensions）成为签名态射（signature morphisms），外部裁决（external verdicts）通过余态射（comorphisms）进入。这一设计使得外部工具——定理证明器、计算引擎或其他验证服务——的判定结果可以以受控方式汇入知识库。

在此基础上，作者还形式化了一个带类型的知识图理论（typed knowledge-graph theory），包含记录（records）、类（classes）和精化（refinements）。转换、按值规范化（normalization by evaluation）以及双向类型检查（bidirectional type checking）相对于终止性的正确性也得到了证明。

值得指出的是，该工作附带了一个 Lean 4 形式化，意味着书中的核心结论经过了机器验证，而不仅是纸面推导。

**证成逻辑（justification logic）**是模态逻辑的一种细化，它将“□A”（A 是必然的）替换为“t : A”（项 t 是 A 的证成），其中 t 可以是证明、证据或支持关系的显式记录。与传统证明逻辑不同，证成逻辑允许追踪证据的结构：同一个命题可以由不同证成项支持，且证成项之间可以组合、合并。Eigenius 在内核命题之上发展证成逻辑，正是为了在不破坏证明无关性公理的前提下，记录“谁、通过什么方式”建立了断言。

**构造性制度（constructive institutions）**是制度理论在构造性类型论中的变体。经典制度理论（institution theory）用范畴论框架统一描述逻辑系统：签名（signature）对应语言，签名态射（signature morphism）对应语言翻译，模型函子与满足关系构成制度的核心。Eigenius 将知识存储的扩展建模为签名态射，将外部工具（定理证明器、计算引擎）的裁决通过余态射（comorphism）汇入——余态射是制度间保持满足关系的翻译，它保证外部结果进入知识库时语义不丢失。这一设计使异构验证工具的结果能以受控、可追溯的方式整合。

为什么这对知识库和 AI 系统有意义

Eigenius 的动机虽然来自数学与程序验证，但其问题意识对更广泛的知识管理场景同样成立。当前的知识图谱和数据库在存储断言时，往往只保留“结论”，而忽略“谁、如何、在什么前提下”得出该结论的完整证据链。当多个来源冲突时，或当外部工具升级导致结论失效时，缺乏证据记录的系统难以进行追溯和修正。

Eigenius 的思路是把证据追踪内建到类型系统里，让知识库从结构上就无法丢失推导历史。这种“证据优先”的设计，对于需要审计、溯源和持续更新的知识系统来说，提供了一条不同于传统数据库路线的理论路径。

当然，这套理论目前仍处于元理论构建阶段，距离工程化落地还有距离。但其将制度理论、证成逻辑与依赖类型论结合的方式，为构造性知识管理提供了一个值得关注的框架。

小结

Eigenius 通过把证明无关性降格为带见证的公理、引入证成逻辑追踪证据、以制度组织知识扩展，试图在内核层面解决知识持久化的证据保留问题。Lean 4 形式化增强了结论的可信度。对于关注类型论应用、形式化验证和知识表示的研究者与工程师，这本书提供了一个结构严谨的参考框架。