The Negative Proof

Craig’s interpolation theorem says: if A implies B, then there exists a formula C — the interpolant — using only the vocabulary shared by A and B, such that A implies C and C implies B. The interpolant is the common ground between premises and conclusion.

Finding interpolants is useful in verification, automated reasoning, and model checking. Standard methods derive them from proofs of A → B, extracting the shared content from the proof structure. Trybus, Rozko, and Skura (arXiv:2603.15876) invert this: instead of proving what’s true, build a calculus that proves what should be rejected. The refutation system — the logical mirror — turns out to be better at finding interpolants than direct proof.

The method works in non-classical modal logics where standard proof-theoretic interpolation methods struggle. By systematically building refutations (demonstrations that a formula fails in specific models), the shared vocabulary constraints emerge naturally from the structure of the counterexample. The interpolant is read off from what the refutation cannot avoid mentioning.

This is structurally surprising because interpolation is about what two formulas share in common — a constructive, positive question. Yet the answer emerges more naturally from the negative image. What A and B have in common is best seen not through what they jointly prove but through what they jointly refuse to deny. The shared ground is defined by the shape of the shared rejection.

The principle extends beyond logic. To understand what two people agree on, don’t ask what they both believe — observe what they both refuse to accept. The common ground is carved by the negatives, not the positives. Agreement is the complement of shared rejection, and shared rejection is easier to map.