【锚点】这一篇只钉一个判断：【古典逻辑是单调的——加前提只会让结论集变大或不变，永不删除；但真实推理会「撤回」结论。可撤销推理（defeasible reasoning）不是逻辑的补丁，而是一套连「我错了」都能形式表达的推理系统。】

【显式】先摆定义。单调性：若 Γ ⊢ φ，则对任意 ψ，Γ∪{ψ} ⊢ φ。Modus ponens 就是样板：{P, P→Q} ⊢ Q；再加 R、再加 S，Q 永远在。古典逻辑里，「撤回」这个操作根本不存在——它连表达「我错了」的语法都没有。

【隐式】推理一步就看出问题：日常推理违反单调性。 - 前提1：Tweety 是鸟 → 默认 Tweety 会飞。 - 加前提2：Tweety 是企鹅 → 撤回「会飞」。 后一个前提是真的，前一个结论被合法撤销。这不是逻辑错误，这是「默认（default）」在起作用。

【细微】比对多处才发现的细节：Nixon 菱形。Nixon 既是贵格会教徒（默认和平主义者），又是共和党人（默认非和平主义者）。Reiter 的默认逻辑（1980）在这里给出两个互相冲突的「扩展」（extension）：一个世界里他是和平主义者，另一个世界里不是。关键不是「没有答案」，而是「有两个自洽答案，系统无法替你选」。这是多扩展问题（multiple extensions），不是矛盾。

【极难发现】深挖底层才暴露的盲点：撤回不是「删掉一行」，而是需要追踪每条信念的 justification。Doyle 的真值维护系统（TMS, 1979）就是干这个的：每个节点记录「我为什么被信」，当某个前提被撤销，系统顺着 justification 链传播，把依赖它的信念标成 OUT。单调逻辑里没有这套机制，因为它假设前提永不撤回。一旦你允许撤回，你就必须维护一张「依赖图」——这是从「证明」到「信念维护」的范式转移。

【流程节点链路】完整的可撤销推理链路： 起点（信念集 Γ + 默认规则集 D）→ 加入新前提 ψ → 触发默认规则（如「鸟→会飞」）→ 检测与已有结论的冲突（如「企鹅→不会飞」）→ 计算扩展（可能多个）→ 按优先级/特异性选出主扩展 → 终点（保留或撤回结论，并更新 justification 图）。少一环，系统就会在冲突面前要么死锁、要么静默出错。

结尾问题：一个无法表达「撤回」的推理系统，还能叫「推理」吗？还是只是「证明生成器」？古典逻辑给的是后者。真实智能要的是前者——这也是为什么「非单调」不是逻辑的边角料，而是它的心脏。