A logic satisfies Craig interpolation if whenever one formula in the logic entails another formula in the logic, there is an intermediate formula --- one entailed by the first and entailing second --- using only relations in the common signature of the two formulas. Uniform interpolation strengthens this by requiring the interpolant to depend only on the antecedent formula and the common signature. A uniform interpolant can thus be thought of as a minimal upper approximation of a formula within a subsignature. For first-order logic, interpolation holds but uniform interpolation fails. Uniform interpolation is known to hold for several modal and description logics, but little is known about uniform interpolation for fragments of predicate logic over relations with arbitrary arity. Further, little is known about ordinary Craig interpolation for logics over relations of arbitrary arity that have a recursion mechanism, such as fixpoint logics. In this work we take a step towards filling these gaps, proving interpolation for a decidable fragment of least fixpoint logic called unary negation fixpoint logic. We prove this by showing that for any fixed k$ uniform interpolation holds for the k-variable fragment of the logic. In order to show this we develop the technique of reducing questions about logics with tree-like models to questions about modal logics, following an approach by Gradel, Hirsch, and Otto. While this technique has been applied~to expressivity and satisfiability questions before, we show how to extend it to reduce interpolation questions about such logics to interpolation for the mu-calculus.
Accepted at LICS 2015. 12 pages.
© 2015 Michael Benedikt, Balder ten Cate , and Michael Vanden Boom.