四、【极难发现】非单调性的精确来源：不是「前提变多」，是「极小元被挤走了」

很多人以为非单调就是「新证据推翻了旧结论」。错了。新证据完全可以和旧结论【相容】，结论照样被撤回。为什么？因为 |~ 的判定发生在 Min_≺(Mod(φ)) 上，而 Min 这个算子对集合包含【不单调】。

给一个三行反例： Ω = {w1, w2}，w1 ≺ w2。 取 B = Ω，则 Min(B) = {w1}。 取 A = {w2}，则 Min(A) = {w2}。 A ⊆ B，但 Min(A) ⊄ Min(B)。

翻译成人话：w2 本来被 w1 压着，轮不到它说话；一旦 w1 被前提排除，w2 立刻变成「最合理的世界」，而它可能满足完全相反的命题。于是 φ |~ ψ 成立，φ ∧ χ |~ ψ 不成立——哪怕 χ 与 φ 毫无矛盾。撤回不是因为冲突，是因为【排序的极小元换了人】。

【流程节点链路】：新前提 χ → Mod(φ∧χ) = Mod(φ) ∩ Mod(χ) → 重新取 Min_≺ → 极小元集合可能整体换血 → 结论重算 → 旧结论被撤回。链条的第四节点是全部反直觉的来源：集合只是变小，argmin 却可以跳变。

这就是为什么「非单调」这个词有误导性。它听起来像「逻辑变得不严格了」。恰恰相反：它比古典逻辑多了一个参数，因此更严格——只是那个参数（≺）平时被古典逻辑默认成了「所有世界一样合理」，也就是空序。

五、【细微】语用学早就知道这件事：可撤销性 = 非单调性

Grice 的会话含义有一条判据叫【可撤销性】（cancellability）：「Some students passed」蕴含「不是全部」，但你补一句「in fact all of them passed」，含义就消失了，且不产生矛盾。这不是语用学的花边，这是 |~ 的定义在自然语言里的实例。

再看预设投射：「The king of France is bald」预设法国有国王；放进「法国没有国王，所以……」里，预设被局部消解。这也是 Min 在子集上重算。语用学的「accommodation」本质上就是【选一个 ≺】：听者为了让话语成立，临时调整世界的合理性排序。

所以形式逻辑和语用学在这里是同一件事的两面：古典逻辑管 Mod(φ)，语用学管 ≺。谁只谈前者，谁就解释不了「默认」和「撤回」。

六、我的靶子：大家都把 ≺ 当成固定的

KLM 的表示定理很美，但它有一个没人爱提的前提：一个知识库配【一个】全局序。真实推理不是这样。你问「这只鸟会飞吗」和问「这只鸟是企鹅吗」，调用的合理性序不一样——前者按物种典型性排，后者按分类学排。序随【查询】变。

Pearl 的 ε-semantics 和 system Z 想用「最小化异常」造出唯一序，但造出来的仍然是一个序。这就留下一个真问题：如果 ≺ 是语境依赖的，表示定理还剩下什么？我的猜测是：非单调逻辑真正该建模的不是「序」，而是【序的更新算子】——一个把 (Ω, ≺) 和查询一起映射到新序的东西。那才是「默认」的语法。

【待验证点】：是否存在一个表示定理，把「语境依赖的偏好序族 {≺_q}」刻画成一组公理？如果有，它大概会像动态认知逻辑对公开宣告的处理：不是改模型，是改模型上的序。

留一个值得吵的问题：如果 ≺ 随语境变，那「一个知识库有一个逻辑后承集」这个假设本身是不是错的？换句话说——非单调逻辑可能根本不该有「定理」，只该有「策略」。