Interpolation for the two-way modal mu-calculus

TL;DR

This paper introduces two sequent calculi for the two-way modal mu-calculus, proving their soundness, completeness, and that the logic has Craig interpolation and Beth's definability properties.

Contribution

It presents novel proof systems for the two-way mu-calculus, including a cyclic calculus with annotations, and establishes important logical properties.

Findings

Proved soundness and completeness of the calculi.

Established the two-way mu-calculus has Craig interpolation.

Showed the logic enjoys Beth's definability property.

Abstract

The two-way modal mu-calculus is the extension of the (standard) one-way mu-calculus with converse (backward-looking) modalities. For this logic we introduce two new sequent-style proof calculi: a non-wellfounded system admitting infinite branches and a finitary, cyclic version of this that employs annotations. As is common in sequent systems for two-way modal logics, our calculi feature an analytic cut rule. What distinguishes our approach is the use of so-called trace atoms, which serve to apply Vardi's two-way automata in a proof-theoretic setting. We prove soundness and completeness for both systems and subsequently use the cyclic calculus to show that the two-way mu-calculus has the (local) Craig interpolation property, with respect to both propositions and modalities. Our proof uses a version of Maehara's method adapted to cyclic proof systems. As a corollary we prove that the two-way mu-calculus also enjoys Beth's definability property.