Modal status labels: why Kripke earns its place after all

Parent: recursive-harness

Earlier the thread half-dismissed Kripke ("it's just CSP/collapse"). That was too hasty. The precise reconciliation:

• Kripke as logic (S4/S5 axioms, □P→□□P, modal theorem-proving) — not used. (Correct to drop.)
• Kripke as a labeling scheme (mark each fact's modal status: definite / possible / conditional) — needed, and more needed than in SAT.

Why needed, and why more than SAT — the tracing is much harder

SAT facts are binary (true/false) and propagation is exact, so the implication graph is clean and conflict analysis is mechanical. The agent's facts live on a richer modal landscape and propagation is unsound / stochastic / semantic. A "forced" value may be:

• □ definite — entailed by a hard constraint (don't revise);
• ◇ possible — a still-free choice (residual freedom);
• conditional ◇/□ — forced/possible only given some prior choice ("forced once I chose world W") — this is exactly accessibility: reachable-given-which-choices;
• (+ a confidence axis, since unsound) mechanically-verified vs LLM-asserted-but-unchecked.

To backtrack you must know which: a □ fact can't be the culprit (the task forces it); a ◇/conditional fact can be, and the conditional label says where to backjump — to the choice it depends on. Without the modal labels you can't tell what's safe to keep vs what to revise. SAT never needs this (binary + sound); the agent does (richer modal landscape + unsound) — that's why its tracing is so much harder.

Accessibility does pull weight here

accessibility = "this fact is forced/possible given which choices" = the dependency structure = an enriched implication graph. It's what conflict analysis follows to backjump to the revisable ◇/conditional decisions a conflict depends on. SAT's implication graph is the binary, sound special case; the agent's is the multi-modal, unsound general case — so the labels must be explicit.

The label set

Revisited — under the theory layer

• □ over the reliable worlds is exactly gates-are-necessary-conditions: "holds in all (typical, 1−α) success worlds" = a necessary condition of success = precisely what a sound gate checks. The label set and gate theory are the same objects seen from two sides.
• The confidence axis is no longer qualitative: "mechanically-verified vs LLM-asserted" is now a measured α (operationalizing-tolerances — mechanical ≈ 0, semantic calibrated by mutation testing). A label carries its own false-accept rate.
• The conditional labels ARE the provenance edges that the mechanical coordinator traverses to compute backjumps — "forced given which choices" is literally the dependency graph the kernel stores.

One line

Kripke-as-logic: no. Kripke-as-labeling (□ / ◇ / conditional + confidence): yes, and essential — because the agent's tracing runs over a richer, unsound modal landscape than SAT's, and you can't backtrack correctly without knowing each fact's modal status. The accessibility relation is the dependency graph that tells you where to backjump.