A Proof Theory for Modal Fixed Point Logics
Temporal logics are widely used to specify and verify the correctness of information systems when system reliability is crucial. Epistemic logics with common knowledge are important for reasoning about knowledge. Both types of logics are examples of modal fixed point logics. While these logics are well-understood semantically, our syntactic understanding of them is lacking. The state of proof theory for modal logics in general is widely recognised as unsatisfactory. For modal fixed point logics in particular there are no satisfactory cut-free sequent systems. Such systems generally are suitable for automated proof search and, together with their cut elimination procedures, can serve as a basis for declarative programming languages. We intend to address the problem of designing cut-free sequent systems for modal fixed point logics on two levels:
1. Whenever possible we plan to develop such systems together with syntactic cut elimination procedures. If possible, we aim for traditional sequent systems in Gentzen style, but if needed we will also employ ideas from richer proof theoretic formalisms such as the display calculus or deep inference.
2. On the other hand, if no cut-free systems exist for modal fixed point logics, we hope to gain a better understanding of why they do not exist. In this case we are interested in good syntactic approximations.
The development of a proof theory for modal fixed point logics is an important theoretical contribution to the understanding of inference and deduction in these logics, and thus in particular a relevant underpinning of specification and verification of information systems. It is central ground work concerning the procedural aspects of frameworks dealing with information.
