Talk by B. Afshari (LTCS)

Short Title: 
Talk by B. Afshari
Event Date(s): 
Thursday, 2. March 2017 -
10:15 to 11:00

Room 105, Main Building, Hochschulstrasse 5, 3012 Bern

B. Afshari

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).