Talk by B. Afshari (LTCS)
Room 105, Main Building, Hochschulstrasse 5, 3012 Bern
Cut-free completeness for modal mu-calculus
Almost all modal logics are known to admit finite cut-free sequent calculi with modal mu-calculus being a notable exception. I will present a finitary cut-free axiomatisation for the mu-calculus that features a strengthening of the standard induction rule for greatest fixed point. The system is readily seen to be sound and its completeness is established by utilising a novel calculus of circular proofs which will also be discussed. Furthermore, I will look at how these new calculi relate to Kozen’s original axiomatisation (1983) and the semi-formal system of Jäger, Kretz and Studer (2008).