Modal interpolants on fixed finite frames

29^th January 2026, 11:00 Ashton 208
Louwe Kuijer

Abstract

Suppose that φ implies ψ. A Craig interpolant for φ and ψ is then a formula 𝜒 such that (1) φ implies 𝜒, (2) 𝜒 implies ψ and (3) the signature of 𝜒 (i.e., the atoms used in 𝜒) is contained in the intersection of the signatures of φ and ψ. We can think of 𝜒 as an explanation of why φ implies ψ. In some logics (including propositional logic and the basic modal logic K), Craig interpolants are guaranteed to exists, in others they are not. For many logics we can even choose a uniform interpolant that works for any ψ with a given signature, i.e., a formula 𝜒 with signature σ such that (1) φ implies 𝜒, (2) for every ψ, if ψ is implied by φ and sig(φ)∩sig(ψ)⊆σ then 𝜒 implies ψ.

In general, we have a pretty good idea for which logics Craig interpolants and uniform interpolants exist. What we don't know is how large interpolants have to be. There are some logics where it is known that the smallest interpolant can be of exponential size, but for most logics we don't know, although it is generally believed that interpolants for propositional logic are super-polynomial.

Here, we investigate the size of interpolants for tabular logics, which are modal logics that are based on a single finite frame. We don't give an absolute result, but we show that interpolants for these logics are at most polynomially larger than interpolants for propositional logic.