Split Interpolation: Refining Craig's Theorem via Three-Valued Logics
Quentin Blomet
TL;DR
The paper addresses split interpolation for pairs of logics built on a shared $3$-valued Boolean normal monotonic scheme, extending Craig's interpolation to a broad non-classical setting. It shows that among $400$ possible scheme/standard combinations, $40$ satisfy the split interpolation property, with eight yielding stronger refinements than classical Craig interpolation. The authors develop constructive interpolants via ideas like partial sharpening and explicit forms such as $C_{oldsymbol{\phi,\psi}}$, $D_{oldsymbol{\phi,\psi}}$, $E_{oldsymbol{\phi, ext{-}\psi}}$, and $F_{oldsymbol{\phi, ext{-}\psi}}$, and map how paracomplete and paraconsistent logics constrain interpolants. The results illuminate a refined landscape of interpolation, identify eight robust refinements, and suggest future work on related logics (e.g., $ ext{ETL}$, $ ext{NFL}$) and broader scheme extensions with potential practical impact for explanation, verification, and SAT-based reasoning.
Abstract
Which choices of truth tables and consequence relations for two logics $\mathsf{L}_1$ and $\mathsf{L}_2$ ensure the satisfaction of the following split interpolation property: If two formulas $φ$ and $ψ$ share at least one propositional atom and $φ$ classically entails $ψ$, then there is a formula $χ$ that shares all its propositional atoms with both $φ$ and $ψ$, such that $φ$ entails $χ$ in $\mathsf{L}_1$ and $χ$ entails $ψ$ in $\mathsf{L}_2$? We identify the cases in which this property holds for any pair of propositional logics based on the same three-valued Boolean normal monotonic scheme for connectives and two monotonic consequence relations. Since the resulting logics are subclassical, every instance of this property constitutes a particular refinement of Craig's deductive interpolation theorem, as it entails the latter and further restricts the range of possible interpolants.