Cut-free completeness for modal mu-calculus
Bahareh Afshari, Graham E. Leigh · 2017
We present two finitary cut-free sequent calculi for the modal μ-calculus. One is a variant of Kozen's axiomatisation in which cut is replaced by a strengthening of the induction rule for greatest fixed point. The second calculus derives annotated sequents in the style of Stirling's `tableau proof system with names' (2014) and features a generalisation of the ν-regeneration rule that allows discharging open assumptions. Soundness and completeness for the two calculi is proved by establishing a sequence of embeddings between proof systems, starting at Stirling's tableau-proofs and ending at the original axiomatisation of the μ-calculus due to Kozen. As a corollary we obtain a new, constructive, proof of completeness for Kozen's axiomatisation which avoids the usual detour through automata and games.