💻 computer science

A non-uniform view of Craig interpolation in modal logics with linear frames

This paper demonstrates that while normal modal logics extending K4.3 generally lack the Craig interpolation property, the specific problem of deciding whether a Craig interpolant exists for any given pair of formulas is decidable and coNP-complete, a result that also extends to Priorean temporal logics over standard linear time flows.

Original authors: Agi Kurucz, Frank Wolter, Michael Zakharyaschev

Published 2026-06-19

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Agi Kurucz, Frank Wolter, Michael Zakharyaschev

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are a detective trying to solve a mystery involving two suspects, Formula A and Formula B. You know for a fact that if A is true, then B must also be true (A implies B).

In the world of logic, there's a special rule called the Craig Interpolation Property. It says that whenever A implies B, there must be a "middleman" statement, let's call it I, that acts as a bridge. This middleman I has a very specific job:

It only uses words (variables) that appear in both A and B.
A implies I, and I implies B.

Think of I as a translator. If A is speaking "English" and B is speaking "French," the interpolant I is a sentence that uses only words common to both languages, proving that the meaning of A flows logically into B.

The Problem: The Missing Bridge

For many logical systems (like standard math or basic computer logic), this bridge I always exists. But the authors of this paper are looking at a specific, tricky family of logics called K4.3 and its relatives. These logics describe "linear" worlds—think of time moving in a single, straight line from past to future, or a line of people waiting in a queue.

In these linear worlds, the "Bridge Rule" (the Craig Interpolation Property) breaks. Sometimes, A implies B, but there is no middleman sentence I that fits the rules. It's like having a conversation where the logic holds, but you can't find a single sentence that summarizes the connection using only shared vocabulary.

Usually, when a logic breaks this rule, researchers throw up their hands and say, "Well, we can't find a bridge, so we can't study this connection anymore."

The New Approach: The "Does a Bridge Exist?" Game

The authors decided to take a different, "non-uniform" approach. Instead of asking, "Does a bridge always exist for every pair of sentences?" (which the answer is no), they asked a more practical question:

"For these two specific sentences, A and B, does a bridge exist?"

They call this the Interpolant Existence Problem (IEP). It's like asking a mechanic: "Does this specific car have a working engine?" rather than asking "Do all cars in this factory have engines?"

The Big Discovery: It's Not Harder Than Checking Validity

The authors proved something surprising. Even though the "Bridge Rule" is broken for these logics, figuring out if a bridge exists for a specific pair of sentences is not a super-hard, impossible task.

In computer science terms, the difficulty of finding out if a bridge exists is exactly the same as the difficulty of checking if the original statement (A implies B) is true. They call this complexity coNP-complete.

The Analogy:
Imagine you are trying to cross a river.

The Old View: "The bridge is broken, so you can never cross."
The Authors' View: "The bridge is broken, but we can check if a specific boat exists to get you across. And guess what? Checking if the boat exists is just as easy as checking if the river is actually there."

They showed that for these linear logics, you don't need a super-computer to solve this; a standard computer can do it efficiently. This is a big deal because, in other similar logical systems, finding out if a bridge exists is much, much harder than just checking if the original statement is true.

How They Did It: The "Descriptive Frame" Map

To solve this, the authors used a tool called descriptive frames. Imagine these as detailed, high-resolution maps of the logical world.

Sometimes, the maps look like simple, finite lines.
Sometimes, they look like infinite chains of clusters (groups of points) that stretch on forever, like a "tadpole" shape with a head and an infinite tail.

The authors discovered that even though these maps can get complicated, the "bad" cases where no bridge exists always follow a very specific, understandable pattern. They proved that you can always shrink these infinite, complex maps down to a manageable, polynomial-sized version that still tells you the truth about whether a bridge exists.

They applied this method to:

Standard Linear Logics: The logic of straight lines (K4.3).
Temporal Logics: Logics that handle both "future" and "past" (like time). They looked at specific time flows like the Integers (..., -2, -1, 0, 1, 2...), Rationals (fractions), Reals (continuous numbers), and Finite time.

For all of these, they proved that checking for a bridge is computationally manageable (coNP-complete).

The Takeaway

The paper turns a "negative" fact (these logics don't have the interpolation property) into a positive research question. They showed that even in a world where the perfect bridge doesn't always exist, we can still efficiently decide if a bridge exists for any specific situation.

In short: Just because the "perfect bridge" rule is broken in these linear worlds doesn't mean we are stuck in the dark. We have a reliable, efficient flashlight to check if a path exists for any specific pair of statements.

Technical Summary: A Non-Uniform View of Craig Interpolation in Modal Logics with Linear Frames

Problem Statement
The Craig Interpolation Property (CIP) is a fundamental property in logic stating that for any valid implication $\phi \to \psi$ , there exists an interpolant $\iota$ using only the shared vocabulary of $\phi$ and $\psi$ such that $\phi \to \iota$ and $\iota \to \psi$ are also valid. It is a well-established "negative" fact that many normal modal logics extending K4.3 (the logic of linear transitive frames) lack the CIP, particularly those with frames of unbounded depth. Traditionally, the absence of CIP has terminated research into interpolants for a given logic.

This paper reframes the absence of CIP as a research question by investigating the Interpolant Existence Problem (IEP): given two formulas $\phi$ and $\psi$ such that $\phi \to \psi$ is valid in a logic $L$ , does there exist a Craig interpolant in $L$ ? Unlike the uniform CIP, the IEP does not reduce to simple validity checking because the validity of the implication does not guarantee the existence of an interpolant. The central question addressed is whether the IEP is computationally harder than the validity problem (entailment) for these logics. Previous results on other logics (e.g., modal logics with nominals, fragments of first-order logic) suggested the IEP could be significantly harder (e.g., 3ExpTime). This paper investigates whether this holds for propositional modal logics containing K4.3.

Methodology
The authors employ a non-uniform, model-theoretic approach based on bisimulations and descriptive frames.

Bisimulation Characterization: The paper utilizes a known criterion (Theorem 3.2) stating that $\phi \to \psi$ lacks an interpolant in $L$ if and only if there exist two models, $M_1$ and $M_2$ , based on descriptive frames for $L$ , such that $M_1$ satisfies $\phi$ , $M_2$ satisfies $\neg\psi$ , and the root points of these models are $\sigma$ -bisimilar (where $\sigma$ is the shared signature).
Descriptive Frames: The analysis relies heavily on the structure of descriptive frames (frames equipped with a specific algebra of internal sets satisfying differentiation, tightness, and compactness conditions). This is crucial because, for logics like GL.3 and Log{(N, <)}, counterexamples to the CIP cannot be witnessed by standard Kripke frames but require infinite descriptive frames.
Structural Decomposition: The core technical innovation involves analyzing the structure of these bisimilar models. The authors partition the models into $\sigma$ -blocks (intervals of points with specific bisimulation properties) and show that any pair of bisimilar models witnessing the lack of an interpolant can be transformed into a pair of "quasi-finite" models. These models are constructed as ordered sums of simple models based on specific atomic frames (finite chains, finite clusters, or "tadpole" structures like $C(\bigcirc_k, \bullet)$ ).
Quasi-Polysize Property: For finitely axiomatisable logics, the authors prove that these witnessing models can be bounded in size by a polynomial in the size of the input formulas and the logic's axioms. This is termed the quasi-polysize bisimilar model property.

Key Contributions and Results

Decidability and Complexity: The paper proves that for all finitely axiomatisable normal modal logics containing K4.3, the IEP is decidable and coNP-complete.
- This result is significant because it shows the IEP is not harder than the validity problem (which is also in coNP for these logics). This stands in sharp contrast to recent non-uniform interpolation results in other logical frameworks where the IEP is strictly harder.
- The proof involves a non-deterministic algorithm that guesses polynomial-sized models satisfying the bisimulation criterion and verifies the logic's axioms.
Quasi-Polysize Bisimilar Model Property: The authors establish that all finitely axiomatisable extensions of K4.3 possess the "quasi-polysize bisimilar model property." This means that if an interpolant does not exist, there exists a pair of bisimilar models witnessing this fact where the models are ordered sums of a polynomial number of simple models based on atomic frames of polynomial size.
- For d-persistent cofinal subframe logics (a subclass), the property is even stronger: they possess the polysize bisimilar model property, where the models are standard Kripke frames of polynomial size.
Extension to Priorean Temporal Logics: The methodology is extended to Priorean temporal logics (containing both future and past modalities) over standard time flows:
- Lin (all linear frames), LinQ (rationals), and LinR (reals): These logics are shown to have the polysize bisimilar model property, and their IEP is coNP-complete.
- Lin<ω (finite strict linear orders) and LinZ (integers): These logics do not have the polysize property but possess the quasi-polysize bisimilar model property. Their IEP is also proven to be coNP-complete.
- The proof for temporal logics requires handling bidirectional chains and limit clusters in both directions, necessitating new frame constructions (e.g., symmetric "tadpole" frames $C(\bullet, \bigcirc_k, \bullet)$ ).

Significance and Claims
The paper claims to provide the first general result on Craig interpolant existence covering a large family of modal logics (extensions of K4.3) that lack the CIP. By demonstrating that the IEP is coNP-complete for these logics, the authors challenge the intuition that the absence of the CIP necessarily leads to a higher complexity class for the existence problem.

The work suggests that the complexity of the IEP is not inherently tied to the failure of the CIP but rather depends on the structural properties of the models required to witness the failure. The authors position this as a step toward a classification of modal logics based on the complexity of their IEP.

The paper explicitly notes that its proof is not constructive regarding the computation of interpolants; it provides a decision procedure for existence but does not yield an efficient algorithm for computing the interpolant itself or upper bounds on its size. The authors also highlight that descriptive frames are essential for their proofs, raising the open question of whether Kripke frames suffice for the IEP in logics that are not d-persistent but are strongly Kripke complete (like LinR).