隔离，而非引爆——隔离作为次协调逻辑
经典逻辑对任何信念存储都埋着一颗地雷：ex falso quodlibet（"由假可推出一切"）——只要存在一个矛盾，就能推出任何命题。这对数学来说没问题（数学中一致性是神圣的，出现矛盾就意味着推倒重来），但对一个由不可靠求解器持续供给的存储来说是致命的。一个由 LLM 断言得到的约束集合，某处必然会出现矛盾（llm-as-fallible-theory-solver），而在经典逻辑下，一个矛盾就足以让整个存储坍缩为能证明任何东西——一场使推理失去意义的逻辑爆炸。
软化方案：次协调逻辑
次协调逻辑（paraconsistent logic）阻止了爆炸的发生：矛盾停留在局部；未受影响的区域推理照常继续。一致性要求从全局性的（一颗毒丸就能杀死整个存储）软化为限定范围的。一个领域内的矛盾不会扩散转移到整个信念格（belief lattice）。这不是把不一致当作一种特性来用（那样本身就不自洽），而是把不一致当作一个可被容纳的事件——就像一个沙箱化的进程可以崩溃，而不会拖垮内核。
harness 的落地方式——按来源限定范围
no-good / 信念存储必须按来源（provenance）限定范围：在区域 R 中发现的矛盾，只会使来源路径经过 R 的那些结论失效。coordinator 的来源图（provenance graph）机械地计算出这个锥形范围。来自不同来源或不同 world 的信念可以共存；一次冲突触发的是对该锥形范围的隔离，而不是全局性的恐慌。
具体来说：当一个 LLM 断言事实 f，随后又断言 ¬f 时，这两次断言都会连同各自的来源一起被记录下来（是哪一步推理、哪个输入集合、哪个 world）。一个矛盾并不意味着存储本身不一致；它是一次局部化的碰撞，只会使依赖于该碰撞锥形范围的下游结论失效，并触发冲突学习（conflict-learning）。
两种矛盾，两种应对
在一个已固定（pinned）的 world 内部： 这是真正的冲突——分析它、学出对应的 no-good、回跳（backjump）（conflict-learning-and-backjumping）。矛盾在这里是加速搜索的燃料。
在多个 world 之间，或在元存储（meta-store）里的软信念之间： 这根本算不上冲突（world-choice and consistency-gate：不同的 world 本来就可以在事实上互相不一致）。在这些不可靠的、由 LLM 断言得到的信念之间，分歧是预期中的背景噪声——这是与不可靠的 \varepsilon oracle 打交道时固有的特性，不是缺陷。次协调逻辑，就是既能在第二种情形里安然共处、又能在第一种情形里（有用地）照常引爆的那套逻辑。
隔离获得了它的逻辑身份
控制手段 #5（隔离/沙箱化，control-methods）到目前为止一直是一种工程实践；次协调逻辑是它在逻辑层面的名字：对信念做沙箱化 = 从构造上阻断 ex falso。限定范围的存储、按 world 划分的约束集合、被限制在事务内的副作用——这些都是同一个动作：让一个矛盾的爆炸半径始终与它的来源锥形范围成正比，而绝不扩散到全局。SAT 内核的蕴含图（implication graph，即被记录下来的来源信息）正是让这一切得以机械化实现的工具。
一句话总结
一个不可靠的求解器必然会产生矛盾；真正的选择不在于要不要矛盾，而在于是否允许其中一个矛盾杀死整个存储。按来源隔离，只在一个已固定的 world 内部引爆。