Logical questions concerning the <i>μ</i>-calculus: Interpolation, Lyndon and Łoś-Tarski (Q4953222)

The paper deals with the modal mu-calculus, i.e., modal logic extended with least and greatest fixpoints, which has turned out to be very useful in computer science, in particular in the area of specification and verification. The authors look at the mu-calculus from a classical logician's point of view, studying three model theory issues. First they show that the mu-calculus enjoys a uniform interpolation property: given a mu-sentence \(\phi\) and a language \(L'\subseteq L(\phi)\), there is \(\theta\) with \(L(\theta)\subseteq L'\) such that \(\phi\models\theta\) and whenever \(\phi\models\psi\) where \(L(\phi)\cap L(\psi)\subseteq L'\) then \(\theta \models\psi\). We can note that this is a stronger property than the Craig interpolation lemma for first-order logic. The second issue is the Lyndon theorem: a mu-sentence which is monotone in (valuations of) propositions is equivalent to a positive sentence (propositions appear under an even number of negations). The third issue is the Loś-Tarski theorem for modal mu-calculus: mu-sentences which are preserved under substructures are equivalent to universal sentences (no diamond operation, i.e. no ``there is a possibility \dots'', is used). As the main tool in the proofs, the authors use the mu-automata of Janin and Walukiewicz.