模态状态标签：为什么 Kripke 终究值得一席之地

Parent: recursive-harness

早些时候这条讨论线一度半否定了 Kripke("这不过是 CSP/坍缩罢了")。这个判断下得太快了。精确的调和是：

• 作为逻辑的 Kripke（S4/S5 公理、□P→□□P、模态定理证明）——用不上。（丢掉是对的。）
• 作为标签方案的 Kripke（标记每条事实的模态状态：确定 / 可能 / 有条件）——需要，而且比在 SAT 里更需要。

为什么需要，为什么比 SAT 更需要——追溯要难得多

SAT 中的事实是二值的（真/假），传播是精确的，因此蕴含图干净，冲突分析是机械的。agent 的事实活在一片更丰富的模态景观里，传播是不可靠的 / 随机的 / 语义性的。一个"被强制"的值可能是：

• □ 确定——由硬约束蕴含（不可修订）；
• ◇ 可能——一个仍然自由的选择（剩余自由度）；
• 有条件 ◇/□——只在给定某个先前选择的条件下才被强制/可能("一旦我选了世界 W，它就被强制了")——这恰好就是可达性（accessibility）：给定哪些选择后可达；
• （加上一条置信度轴，因为不可靠）机械验证过的 vs LLM 断言但未核实的。

要回溯，你必须知道是哪一种：□ 事实不可能是罪魁祸首（任务强制了它）；◇/有条件的事实可能是，而有条件标签指明该回跳到哪里——回跳到它所依赖的那个选择。没有模态标签，你就分不清什么可以安全保留、什么该修订。 SAT 从不需要这个（二值 + 可靠）；agent 需要（更丰富的模态景观 + 不可靠）——这就是它的追溯难得多的原因。

可达性在这里确实起作用

accessibility（可达性）=「这条事实在给定哪些选择下被强制/可能」= 依赖结构 = 一张加强版的蕴含图。冲突分析正是沿着它回跳到冲突所依赖的、可修订的 ◇/有条件决策。SAT 的蕴含图是二值、可靠的特例；agent 的蕴含图是多模态、不可靠的一般情形——所以标签必须显式给出。

标签集

重访——放到理论层之下

• 在可靠的世界集合上的 □，正是 gates-are-necessary-conditions："在所有（典型的，1−α）成功世界中都成立"= 成功的一个必要条件 = 恰好就是一个可靠的 gate 所检验的东西。标签集和 gate 理论是同一批对象从两个侧面看到的样子。
• 置信度轴不再是定性的了："机械验证过的 vs LLM 断言的"现在是一个被测量出来的 α（operationalizing-tolerances——机械型 α≈0，语义型由变异测试校准）。一个标签自带它自己的假阳性接受率。
• 有条件标签正是 mechanical coordinator 为计算回跳而遍历的溯源边——"在给定哪些选择下被强制"就是内核所存储的依赖图本身，字面意义上的。

一句话

Kripke 作为逻辑：不需要。Kripke 作为标签体系（□ / ◇ / 有条件 + 置信度）：需要，而且是必需的——因为 agent 的追溯运行在一片比 SAT 更丰富、更不可靠的模态景观上，不知道每条事实的模态状态就无法正确回溯。可达性关系就是那张告诉你该回跳到哪里的依赖图。