Lyndon Interpolation for the Modal mu-Calculus

ABSTRACT. We prove Lyndon interpolation for the modal mu-calculus by applying so-called circular proofs. One of the proof systems for the modal mu-calculus is based on non-well-founded derivation trees with a global condition which roughly says that in each infinite branch, there must be an outermost greatest fixed point unfolded infinitely many often. We analyse regular proof trees (so-called circular proofs) in this proof system and obtain the Lyndon interpolation for the modal mu-calculus.