The Inexpressible Condition

Interpretability logic reasons about what formal systems can prove about each other. Its semantics uses Veltman frames — relational structures where the accessibility relation captures “this theory can interpret that theory.” Frame conditions characterize which frames validate which formulas.

Frigola Gonzalez, Joosten, Navarro Arroyo, and Perini Brogi (arXiv:2603.16754) discover a first-order frame condition that matters for interpretability logic but that the logic itself cannot express. The condition is well-defined, the frames satisfying it have distinctive properties, but no modal formula distinguishes frames that satisfy it from frames that don’t. The logic is blind to a condition on its own semantics.

This is not a contingent limitation that better axioms might fix. It is a structural boundary of modal expressiveness. The Goldblatt-Thomason theorem provides the criterion: a frame property is modally definable if and only if it is preserved under certain algebraic operations (generated subframes, bounded morphisms, disjoint unions, and reflected by ultrafilter extensions). The new condition fails one of these, proving inexpressibility.

The workaround is ultrafilter extensions — building a larger frame from the original by adding points that correspond to ultrafilters over the frame’s domain. This algebraic construction can “see” what the modal language cannot. The logic works with the extended frame even though it cannot characterize the extension in its own terms.

The gap between a logic and its semantics is structural information about the logic. What it cannot express is as informative as what it can. The inexpressible condition tells you exactly where the logic’s descriptive power ends — not because the logic is weak, but because the condition lives on the wrong side of a precise algebraic boundary.