From Interpolating Formulas to Separating Languages and Back Again

TL;DR

This paper explores generalizations of Craig interpolation, including implications in non-CIP logics, weaker languages, and separation problems, connecting these concepts to decidability results in formal languages and temporal logic.

Contribution

It introduces a unified framework linking Craig interpolation variations, language separation, and decidability, extending traditional interpolation to broader logical and language classes.

Findings

Decidability of Craig interpolant existence in non-CIP logics.

Connection between language separation and Craig interpolation in formal languages.

Decidability results for LTL based on regular language separation.

Abstract

Traditionally, research on Craig interpolation is concerned with (a) establishing the Craig interpolation property (CIP) of a logic saying that every valid implication in the logic has a Craig interpolant and (b) designing algorithms that extract Craig interpolants from proofs. Logics that lack the CIP are regarded as `pathological' and excluded from consideration. In this chapter, we survey variations and generalisations of traditional Craig interpolation. First, we consider Craig interpolants for implications in logics without the CIP, focusing on the decidability and complexity of deciding their existence. We then generalise interpolation by looking for Craig interpolants in languages L' that can be weaker than the language L of the given implication. Thus, do not only we restrict the non-logical symbols of Craig interpolants but also the logical ones. The resulting L/L'-interpolation problem generalises L/L'-definability, the question whether an L-formula is equivalent to some L'-formula. After that, we move from logical languages to formal languages where interpolation disguises itself as separation: given two disjoint languages in a class C, does there exist a separating language in a smaller class C'? This question is particularly well-studied in the case when the input languages are regular and the separating language is first-order definable. Finally, we connect the different research strands by showing how the decidability of the separation problem for regular languages can be used to prove the decidability of Craig interpolant existence for linear temporal logic LTL.