Cut-elimination for modal logics with fixed points
Thomas Studer, University of Bern
Modal fixed point logics are extensions of modal logics with operators denoting least, respectively greatest, fixed points of certain positive formulas. Logics of this kind include temporal logics, logics of common knowledge, program logics, and most famously, the modal mu-calculus. We present a survey of deductive systems for the logic of common knowledge as a typical example of a model fixed point logic. In particular, we present two different Hilbert-style axiomatizations and several infinitary cut-free sequent systems that are based on omega-rules. Further, we discuss the problem of syntactic cut-elimination for common knowledge and its generalization to the modal mu-calculus.