【锚点】只钉一个判断：经典命题逻辑是单调的（monotonic）——加前提永远不会推翻已得结论；而真实推理几乎从不单调。凡是把真实推理硬塞进单调逻辑的模型，都会在「新信息到来」这一刻系统性失效。

【显式】单调性的定义：若 Γ ⊢ φ，则对任意 Δ，Γ ∪ Δ ⊢ φ。加前提只会增加、不会减少定理集。这是经典逻辑的一条元定理，不是可选项。

【显式】反例是常识级的：Tweety 是鸟 → Tweety 会飞。加上「Tweety 是企鹅」→ 结论被撤销。这不是逻辑错误，这是推理的正确行为。

【隐式】这里暴露的不是「逻辑不够用」，而是「推理有两种：蕴含（entailment）与默认（default）」。蕴含不可撤销，默认可撤销。

【细微】Reiter 1980 的默认逻辑（default logic）把默认写成规则 α : β / γ，读作「若相信 α，且 β 与当前信念集一致，则可默认 γ」。注意 β 是「一致性检验」——它让推理对「当前还相信什么」敏感，这正是非单调性的来源。

【极难发现】代价藏在定理里：默认逻辑不保证唯一解。Nixon diamond——尼克松既是贵格会教徒（默认和平主义），又是共和党人（默认鹰派），两个默认冲突，系统给出两个「扩展」（extension），而不是一个答案。非单调逻辑的「结论」不是单个命题，而是一族自洽的信念闭包。你以为在算一个答案，其实在算一个不动点集合。

【隐式】语用学早就独立发现了同一件事：Grice 的会话含义（conversational implicature）是可取消的（cancellable）。「有些学生通过了」含义是「并非全部」，但可以当场取消：「有些学生通过了——事实上全部通过了。」可取消性正是「含义」区别于「蕴含」的判据。含义是默认推理，蕴含是单调推理。

【流程节点链路】把「有些学生通过了」的推理拆开：起点=说出「有些」（量词）→ 中间节点1=听者假设说话人遵守量的准则（信息量最大化）→ 中间节点2=若「全部」为真则「有些」信息量不足，说话人本可说「全部」→ 中间节点3=推断说话人不知道或并非全部 → 终点=含义「并非全部」。任一中间节点被新信息打断（如后续补「事实上全部」），终点即被撤销。这条链路本身就是证据：含义不是从字面逻辑推出的，是从「说话人为何这样说」的默认推出的。

【极难发现】所以「除非」在自然语言里比「如果」更诚实：unless 天生携带一个可撤销的默认，而 if 假装自己不可撤销。形式化里我们常把 unless 翻译成 if not，但那个翻译丢掉了「可撤销」这个语义核心。

【结论】可撤销推理不是「不严谨的逻辑」，它是唯一能对「新信息」保持敏感的推理。代价是：你不能再问「这个结论对不对」，只能问「在哪个信念集下它成立、被什么打断」。

【值得辩论的问题】如果推理本质上是可撤销的，那么「证明」到底是什么？一个结论在什么条件下才算被「钉住」，而不只是「暂时成立」？我的初步立场：证明不是「不可撤销的推导」，而是「对撤销条件的显式登记」——一个结论的价值，取决于它写清楚了自己会在什么前提下失效。