结果族 244：The Partition Principle does not imply Choice · 学科：Mathematical logic · 验证状态：主结果已 Lean 形式化
把无穷多张牌全部发进若干非空的堆。”分割原理”说：只要发得完，就总能从牌里挑出一组互不相同的牌、与堆一一对应。乍看这就是”每堆各挑一张”的选择公理；本文证明它其实更弱——两者并不等价。这个 1902 年提出的问题悬置一百二十余年后，终于有了答案。
关键词卡片
@@M@@X\to Y@@，则存在单射 @@M@@Y\to X@@。@@M@@X@@“铺满”@@M@@Y@@，每个目标都被打到；单射不重复地嵌入。看个具体例子
微妙之处在于：PP 保证的单射不必”从每堆里挑自家的牌”——落点完全自由（见下图红线）。定理断言：若 ZF 一致，则”分割原理＋对良序指标族的选择＋否定选择公理”也一致；换句话说，仅凭 PP 永远推不出 AC。
为什么值得关心
这是无选择集合论中最著名的公开问题之一，答案出乎多数人预料；配套的传递对称模型还保持序数不变、不新增基模型元素的可数序列。更弱的两个推论——对偶 Cantor–Schröder–Bernstein 原理与弱分割原理——也随之与选择公理分离。
已 Lean 形式化
第一级台阶
导读的”发牌”类比换成半数学语言：对象是两个集合与一个把它们联系起来的映射；”发得完”即满射——每个堆都被打到；”挑出一组互不相同的牌”即单射——无重复地嵌回。分割原理说满射必伴随反向单射。与”每堆各挑一张”的差别在于：单射的落点完全自由，不必落在自己那一堆里。
第二级台阶
用本科术语精确化：分割原理 @@M@@\mathsf{PP}@@ 断言存在满射 @@M@@X\twoheadrightarrow Y@@ 就存在单射 @@M@@Y\hookrightarrow X@@；选择公理 @@M@@\mathsf{AC}@@ 断言任何非空集族都有选择函数；@@M@@\mathsf{AC}_{\mathrm{WO}}@@ 是指标可良序时的选择。相对一致性指若 @@M@@\ZF@@ 无矛盾则加新公理后仍无矛盾；证明载体是力迫扩张的对称子模型——只保留在某个群作用下”遗传对称”的名字。
第三级台阶
定理断言：@@M@@\Con(\ZF)@@ 蕴含 @@M@@\Con(\ZF+\PP+\AC_{\mathrm{WO}}+\neg\AC)@@（@@M@@\AC_{\mathrm{WO}}@@ 本就是 @@M@@\PP@@ 的推论，非额外强度）；更强形式在每个可数传递 @@M@@\ZFC@@ 模型上造出序数不变、不新增基模型可数序列的传递对称模型 @@M@@W@@。核心是 @@M@@W@@ 内三条事实——每个非空集都是标签集乘序数的满射像、序标选择成立、@@M@@A@@ 的每个不可良序满射像都与 @@M@@A@@ 双射——由纯 @@M@@\ZF@@ 的全集聚减引理合成 @@M@@\PP@@。而 @@M@@A@@ 不可良序由 Hartogs 论证给出 @@M@@\neg\AC@@。
本文证明分割原理不蕴含选择公理：若 ZF 一致，则 @@M@@\ZF+\PP+\ACwo+\neg\AC@@ 一致，否定了自 1902 年 Beppo Levi 提出后悬置百余年的公开问题。
分割原理（Partition Principle, PP）断言：只要存在满射（surjection）@@M@@f:X\twoheadrightarrow Y@@，就存在反向单射（injection）@@M@@j:Y\hookrightarrow X@@；等价地说，任何划分（partition）的块集可嵌入原集合。选择公理（Axiom of Choice, AC）显然蕴含 PP——在每个纤维（fiber）里选一个元素即可。反向问题由 Beppo Levi 于 1902 年提出，悬置一个多世纪，是无选择集合论中最著名的公开问题之一。症结在于：PP 给出的单射不必满足 @@M@@f\circ j=\id_Y@@，即不必取划分块自身的元素，这份自由度使人既证不出也驳不倒蕴含；此前数个分离模型的宣称已于 2026 年被撤回。
论文有两条主定理。定理一（相对一致性）：若 @@M@@\ZF@@ 一致，则 @@M@@\ZF+\PP+\ACwo+\neg\AC@@ 一致，其中 @@M@@\ACwo@@ 是对序标家族（ordinal-indexed families，良序指标族）的选择公理。经典已知 @@M@@\PP\Rightarrow\ACwo@@（归于 Pincus），故 @@M@@\ACwo@@ 并非额外强度。定理二（传递模型形式）：对 ZFC 的每个可数传递模型 @@M@@V@@，存在集合力迫 @@M@@\mathbb Q\in V@@ 与传递的对称子模型（symmetric submodel）@@M@@W@@，满足 @@M@@V\subseteq W\subseteq V[G]@@、序数相同、@@M@@W\models\ZF+\PP+\ACwo+\neg\AC@@，且 @@M@@W@@ 中每个由基模型元素组成的可数序列都已属于 @@M@@V@@。又因 @@M@@\ZF@@ 中 @@M@@\PP\Rightarrow\mathsf{CSB}^*\Rightarrow\mathsf{WPP}@@（对偶 Cantor–Schröder–Bernstein 原理与弱分割原理），两原理也随之与 AC 分离。
先搭骨架。取基模型 @@M@@V\models\ZFC@@，参数 @@M@@\kappa=\omega_1^V@@、@@M@@\mu=((2^{\aleph_0})^+)^V@@、@@M@@|I|^V=\mu^+@@。力迫为乘积 @@M@@\mathbb Q=\mathbb R\times\mathbb P@@：@@M@@\mathbb R=\operatorname{Add}(\kappa,I)@@ 添加 @@M@@|I|@@ 条 Cohen 子集；@@M@@\mathbb P@@ 的条件是”图”（diagram），即单射 @@M@@r:T\hookrightarrow I@@，@@M@@r@@ 强于 @@M@@s@@ 当且仅当 @@M@@s=r_n@@ 是它的平移子图。@@M@@T@@ 是特制的左可消幺半群（monoid），由 @@M@@\omega_1@@ 轮两类手术建成：有限合并实现指定的有限重叠模式，”探针”（probe）插入实现指定的精确交理想。对称群 @@M@@\Sym(I)^V@@ 同时搬动两坐标，由固定群生成正规滤子，得遗传对称（hereditarily symmetric）名字类与对称模型 @@M@@W@@。标签集 @@M@@A=\{A_j:j\in I\}@@ 是全体新 Cohen 子集；对称性使 @@M@@A@@ 不可良序，进而 @@M@@\mathcal P^W(A)\setminus\{\varnothing\}@@ 无选择函数（Hartogs 型论证），故 @@M@@\neg\AC@@。
再证 @@M@@W@@ 中三条性质：(i) 借名字的轨道映射得 @@M@@\mathrm{SVC}(A)@@，每个非空集都是某个 @@M@@A\times\eta@@ 的满射像；(ii) @@M@@\ACwo@@：@@M@@A@@ 有一个可良序部分能遇上任何序标非空子集族的每个成员，一般家族经 (i) 归约后取最元；(iii) 全文核心：@@M@@A@@ 的每个不可良序满射像都与 @@M@@A@@ 双射。
(iii) 分三步。先算精确可用性纤维：对固定的不可良序商 @@M@@A/E@@，记录每个符号等价类与每个标签在哪些子图上可命名，得理想（ideal）；精确纤维引理用 @@M@@\mu@@ 个独立探针副本加 Cohen 通有性证明每个理想对应的类与标签各有 @@M@@\mu@@ 个，支撑下降（support descent）引理排除非法重合。再把纤维沿典范限制等同粘成分量（component），各带可数共尾链；幺半群下降引理把剩余对称压缩为可数群。最后做等变选择：链上”最小码”良序给出初步双射，有界 Cohen 行片段区分可数陪集并协变选定，跨分量搬运输出被 @@M@@G_q@@ 整体固定的遗传对称图名字，赋值即 @@M@@A@@ 与 @@M@@A/E@@ 的双射。
最后是纯 @@M@@\ZF@@ 归约：任给满射 @@M@@f:X\to Y@@，用 (i) 把 @@M@@X@@ 切片并取互不相交的目标片；可良序片由 @@M@@\ACwo@@ 作截面，不可良序片由 (iii) 双射拼接，再由 @@M@@\ACwo@@ 逐片选出单射取并。元理论上先经可构成宇宙把 @@M@@\Con(\ZF)@@ 化为 @@M@@\Con(\ZFC+V=L)@@，再在可数可能非良基的模型上以内部名字商结构完成推导；传递情形按通常赋值实现。
论文主结果已配 Lean 形式化证明（族元信息链接 lean/docs/244.md），属对集合论构造目前最强的核验。本结果族仅此一篇手稿，相对一致性与传递模型两个定理共享同一构造、互为印证；文中与 Ryan-Smith 的 PP 局部化分析及 Holy–Schilhan 的对称积方法相衔接。按 OpenAI 官方声明，”未经形式化的结果可能有问题”，而本文主结果属已形式化之列；个别引理的范式重写细节技术性较强，此处从略。
问 1：证明中最关键、最脆弱的一步是什么？
答：商分类定理——@@M@@A@@ 的每个不可良序满射像都与 @@M@@A@@ 双射。它靠”精确可用性纤维”的理想计数：@@M@@\mu@@ 个独立探针副本加 Cohen 通有性算出每个理想对应的类与标签各 @@M@@\mu@@ 个，再用支撑下降引理排除非法重合。任何一处计数偏移，等变选择造不出双射，@@M@@\PP@@ 的第三条假设落空。
问 2：PP 的单射为什么不必是”截面”，这真是它与 AC 的全部空隙吗？
答：是全部空隙。全集聚减引理中可良序目标片的单射确是截面，但不可良序片只能借”两侧都与 @@M@@A@@ 双射”拼接，无任何纤维约束——结论一节的注记得明说：这正是 @@M@@\PP@@ 允许的自由度。若强行要求 @@M@@f\circ j=\mathrm{id}@@，就回到选择函数，@@M@@\neg\AC@@ 的模型里必然失败。
问 3：理论里为什么保留 @@M@@\mathsf{AC}_{\mathrm{WO}}@@，它不是多余的吗？
答：不多余但也不加分：Pincus 已证 @@M@@\PP\Rightarrow\mathsf{AC}_{\mathrm{WO}}@@，故加入它不改变强度；同时它在聚减引理里是必需工具——逐片证明候选集 @@M@@\mathcal J_i@@ 非空之后，须对已造好的序标序列一次性选取 @@M@@j_i\in\mathcal J_i@@。没有它，局部非空拼不成全局单射。
问 4：与此前工作相比真正的新意是什么？
答：问题自 Beppo Levi 1902 年悬置，2026 年前数个分离宣称已被撤回。新部件是特制左可消幺半群 @@M@@T@@（@@M@@\omega_1@@ 轮手术控制有限重叠模式与精确交理想）、”图”力迫 @@M@@\mathbb P@@ 与 Cohen 部分 @@M@@\mathbb R@@ 的乘积、以及沿可数共尾链的等变选择；聚减引理本身沿用 Ryan-Smith 的局部到全局方法但换成更强的商分类假设。
问 5：这种构造最可能出错的模式是什么？
答：对称模型的记账错误：遗传对称名字须在每层保持群作用相容，”搬运跨分量的图名字被 @@M@@G_q@@ 整体固定”这类断言层层嵌套，是 AI 生成证明最容易在细节处崩掉的地方。元理论一节还区分了内部力迫解释与外部传递模型两条路线，其间的名字商结构是第二个易错点。主结果已声明 Lean 形式化，是重要背书。
问 6：下游推论与使用者是谁？
答：由 @@M@@\ZF@@ 中 @@M@@\PP\Rightarrow\mathsf{CSB}^*\Rightarrow\mathsf{WPP}@@，对偶 Cantor–Schröder–Bernstein 原理与弱分割原理一并与 @@M@@\AC@@ 分离，无需新构造；模型还显式给出无选择函数的族 @@M@@\mathcal P(A)\setminus\{\varnothing\}@@（Hartogs 递归）。无选择集合论与基数比较理论的研究者直接受用。
总评
这是一百二十余年老问题的干净解决，Lean 形式化加传递模型双定理使其可信度在同类结果中居前；最大风险藏在商分类的理想计数与对称记账的深处，值得社区逐条复核。