区分作为根基

为什么我们认为 e0/e1 比集合、类型、范畴更原始 — Wheeler、Bishop、同伦类型论怎么看

BEDC 从「施行区分」这个动作本身, 递归地展开. 这是别的形式系统都没占据的位置. 这一页讲清楚这个位置是什么, 以及它不是什么.
作者

The Omega Institute

发布于

2026年5月2日

English

没被命名的构造子

再看一遍这个 Lean 类型:

inductive BHist where
  | Empty
  | e0 (h : BHist)
  | e1 (h : BHist)

大多数读者看到的是”二叉树”、“二进制字符串”、“两符号编码的自然数”. 所有这些读法都把这个类型 投影 到一个已经被理解的对象上去. 它们偷偷塞进了一个先验承诺: 存在一个叫”0”的东西和一个叫”1”的东西被记录下来.

Lean 代码字面上没说这件事. e0 和 e1 是构造子的名字, 但它们也完全可以叫 α 和 β, 或者 left 和 right. 这段代码实际说的是:

存在一个起始态, 在这里没有任何构造发生过 (Empty). 存在两种递归延展任何已有历史的方式. 这两种方式不同 (否则类型就冗余了). 仅此而已.

这是 Lean 允许你写出的最小有实质内容的 inductive 类型. 这两个递归构造子不编码任何已存在的实体. 它们是 “这个相对于那个”这件事本身的可能性 — 递归地.

它们的”不同”不是它们具有的属性. 它们的”不同”就是它们是什么.

主流根基预设了什么

要看清这有多原始, 把每个主流根基系统的起点摆出来:

系统 起始对象 已经预设了
ZFC 集合 “集合”作为元层概念; 外延性; 配对、并集、幂集公理
类型论 (MLTT) 类型 类型宇宙; 同一性类型; 某种相等判断
范畴论 对象 + morphism 两层结构; 复合; 单位; 结合律由公理给出
同伦类型论 类型 + path MLTT 的类型; path/同一性这一层
Bishop 构造分析 自然数 Peano 公理; 序列函数; 子集理解原理
Peano 算术 0 + 后继 后继函数作为与任何东西都不同的原语; 自然数的结构
BEDC 施行区分这个动作 CIC 的 inductive 机制, 仅此而已

每个其他系统都拿 某个已经被区分出来的东西 作输入 — 集合、类型、对象、自然数 — 然后向上建. BEDC 拿”施行区分”本身, 递归地, 让其余的自然涌现.

✗ 「但你仍然依赖 Lean / CIC / inductive 类型」

对, 必须承认. BEDC 是 相对的 原始, 不是 绝对的 原始. 我们坐在 Calculus of Inductive Constructions 之上, 用 Lean 的 inductive 机制. BEDC 做的是 把 CIC 内部的残余承诺降到最低: 不用 Classical.choice, 不用 Quot.sound, 不用 propext. 一切都被 axiom-purity --strict 审计验证, 它对每条定理跑 #print axioms, 拒绝 Lean 标准库的任何公理.

$ python3 lean4/scripts/bedc_ci.py axiom-purity
[bedc-ci] axiom-purity: theorems=1837 pure=1837 impure=0
forbidden=['Classical.choice', 'Quot.sound', 'propext']

所以位置是: 在 CIC 之上, BEDC 处于其最小处. 如果你接受 CIC 的 inductive 机制作为表达工具 — 而我们必须接受 某个东西 — 那么 BHist 的两构造子递归就是你能取的最小有意义的起点.

Wheeler 的 “It from bit”, 经过机械验证

1990 年, John Wheeler 提出物理实在或许在根上是信息性的: 每一个”它” — 每个粒子, 每个场 — 都源自对是/否问题的回答. It from bit. 这是哲学. Wheeler 自己很清楚这是猜想, 是问题, 不是定理.

这个猜想有两个自然的延伸:

  1. bit 是物理信息的最小单位. (Susskind, Bekenstein, 全息原理.)
  2. bit 是 任何 信息的最小单位, 包括数学信息. (这一步 Wheeler 没明确承诺, 但他论证的结构暗示了它.)

第 2 步是一个强得多的主张. 它说: 即使我们不在谈物理, 即使我们在做纯数学, 底层原语仍然是二进制区分.

BEDC 是对第 2 步的工作测试. 不是证明, 是构造性测试: 你能从 inductive BHist | Empty | e0 | e1 出发, 不加任何公理, 把 Bishop 风格的实分析、入门范畴论、基础代数搭起来吗?

经过 72 小时的 AI 驱动形式化: 暂时是可以的, 38 章覆盖到数、序列、实数流分类器、连续函数、度量空间、紧致子集、S¹、范畴、函子、自然变换. 1837 条机械验证的定理, mathlib-free, 公理纯净.

这不是 Wheeler 正确的证明. 这是他主张的 结构版本 — 区分作为根基 — 是可建的, 以及当你建起来时它的样子.

三个直觉支持区分作为根基

如果”区分是信息根基”这个主张听起来像门外汉的胡扯, 三个直觉从不同方向给它分量.

信息论直觉. Shannon 的 bit 按定义是信息的最小单位. 任何信息源都可以通过重新标记和拼接归约为二进制流. bit 作为最小是不容讨价的; 唯一的问题是非信息对数学有没有话可说.

认知直觉. 婴儿的认知发展从自我/他者区分开始. 音位区分是语言的最小单位. 概念形成是范畴边界检测. 没有哪一层人类可读的认知不是从”区分”上落下来的.

数学直觉. 每个形式根基最终都落在相等与有别上. 即使最抽象的类型论也需要某种方式说”这一项不是那一项”, 这种能力的证明论内容就是区分.

这些不证明区分是唯一的根基. 它们暗示这是 一个 根基, 如果它工作, 就能解释为什么数学跟物理、跟认知、跟信息论能整合在一起 — 因为它们在根上是同一种活动.

“Hom = Cont” 这个惊喜作为证据

如果区分是根基, 你会期望数学的范畴性结构 自然落出来 — 不需要作为新公理加上去. 它们应该作为内核关系的模式可见, 而不是作为另一层结构.

这就是 BEDC 观察到的 (在 主故事 和 发现回路 详述):

def CategoryHomCarrier (a b f : BHist) : Prop :=
  UnaryHistory a ∧ UnaryHistory b ∧ UnaryHistory f ∧ Cont a f b

范畴的 morphism 是 unary 延续. 复合是 cont_assoc. 单位是 Empty. 范畴公理是内核定理.

如果你从集合开始, 你不得不把范畴作为 新的 代数结构加在集合之上, 配自己的公理. 从类型开始, 同样. 从范畴论开始, 你就有它作原语, 但你已经从一开始就承诺了对象-morphism 的分层结构.

如果你从区分开始, 范畴 已经在那 — 藏在历史与延续的递归结构里. 你不引入它; 你发现内核从一开始就是个范畴.

这是部分但真实的证据. 不是证明. 是证据.

这个位置 不是

不是新物理. 我们没声称 Wheeler 关于量子力学是对的. 我们声称的是, 他结构性直觉的 数学 形式是可建的.

不是说其他根基是错的. ZFC 工作. MLTT 工作. 范畴论工作. 它们成功地建起了数学. BEDC 不是对它们的反驳. BEDC 是一个演示: 存在一个 更原始的起点 也工作, 在它现在已经产出 1837 条机械验证定理这个有限意义上.

不是哲学上的原创. Wheeler 在 1990 年说过类似的话. Spencer-Brown 的 Laws of Form (1969) 探索过区分的代数. 自 Brouwer 以降的构造主义数学认为数学的有意义内容是构造的, 这跟我们密切相关. BEDC 的贡献不是哲学主张本身 — 是这个主张的 机械验证, 在工作的 Lean 代码里, 没有公理.

72 小时之后我们实际知道什么

我们知道, 从 inductive BHist | Empty | e0 | e1 出发, 只加可表达为 BHist 上的 inductive 或 def 的关系, 我们能建:

  • Bishop 风格的实数等价类 (16 条定理在涨)
  • 构造性度量距离见证, 带对称与 transport 闭合 (20 条)
  • 通过 located ε-net 的构造性紧致 (26 条)
  • 连续函数 modulus 链与其复合 (20 条)
  • 范畴、函子、自然变换作为受限延续 (合计 59 条)
  • 完整基础数据类型: 布尔、option、和、积、列表、自然数、整数、有理 (饱和)

我们知道项目是 axiom-purity --strict — 这 1837 条定理每一条都传递性地追溯到 CIC 的 inductive 与 def, 别的什么都没有.

我们知道 schema-only 的章节 (群、幺半群、环、域、模) — 它们的 paper 定义用参数化的 mul : BHist → BHist → BHist — 无法 在不给具体 carrier 的情况下被建出, 因为 AI 的尝试产 parameter echo 而机械 lint 拒绝它们. 这本身是证据: 根基性主张说你不能在 BEDC 里抽象地定义代数结构, 必须 展示 具体实例. 卡住的章节是个信号, 说明根基在做它该做的事.

我们还不知道的:

  • 哲学主张是不是不仅是结构性观察. (问: 区分 真的 是信息的底吗, 还是只是个方便的最小值?)
  • 外部数学家会把 Hom = Cont 这个 unification 读成真洞察还是定义性平凡. (我们还没让构造性分析家或范畴论家审过代码.)
  • 这个根基能走多远才撞墙. (层、流形、测度论、模形式 — 这些 BEDC paper schema 都还是空 stub.)

一个工作假说, 经过机械测试

所以我们愿意以书面形式承诺的位置是:

区分是信息 (包括数学信息) 的候选根基. BEDC 是第一个用构造方式测试这一主张的 Lean 级项目, 不加公理. 测试在 38 章数学 (覆盖计数、实分析、拓扑、入门范畴论) 上暂时为正. 它在层、模形式、同伦群上是否仍为正 — 我们还不知道.

这不是一个宣言. 这是一个被机械测试了 72 小时、产出了 1837 条工作定理的假说. 这也是一个迟早会撞上一个它编码不了的结构的假说 — 而那堵墙, 当我们找到它时, 会告诉我们一些关于”区分作为根基”的边界.

到那之前, 我们继续建.

← 回到主故事
BEDC 是什么, 72 小时里发生了什么, AI 驱动形式化里浮现的五个惊喜. Schema-only 作为证据 →
经验上的搭档: 当我们试图形式化没有具体载体的抽象代数, 它编译不通过. 这种失败是基础主义在工作. 一个 closed loop →
同一个根基如何把 Gödel、Tarski、Hofstadter 变成同一个约束 — 并把它定位在单一 inductive 声明里. 发现回路 →
工程: AI 驱动 harness 怎么自驱, 在哪儿失败, 这套方法论可以推广到什么.

— The Omega Institute