PAnaMoL · Proof-theoretic Analysis of Modal Logics

Proof-theoretic Analysis of Modal Logics

One of the most successful branches of modern symbolic logic is that of modal logics. Due to their favourable balance between expressivity and complexity, logics from this family have found many applications in disciplines such as Mathematics, Computer Science, Philosophy or Economics. In fact, modal logics are so successful that new specimens emerge almost on a daily basis. The downside of this is that often a lot of effort is spent reproving standard results for newly introduced logics. Hence there is a significant demand for general results about such logics, which could be easily instantiated for new specimens. Due to its independence of a particular semantics, the purely syntactic proof-theoretical approach is very promising in this regard. With this in mind, the PAnaMoL project aimed at systematising proof theory for modal logics. We intended to provide a unified perspective on so-called sequent-style calculi and a deeper understanding of the general connections between modal axiom systems and sequent-style calculi for such logics. In detail the research objectives were: The systematic development of suitable syntactic characterisations of modal axioms corresponding to natural formats of rules in different sequent-style frameworks. A systematic comparison of the different sequent-style frameworks. The exploitation of these results in: classification results stating necessary and sufficient proof-theoretic strength for important examples of logics; uniform decidability and complexity results for large classes of logics; general consistency proofs. During the course of the project we established significant results towards these objectives. The resulting deeper understanding of the established proof-theoretic frameworks led to the identification of novel important proof-theoretic frameworks, the introduction of a number of general methods and techniques for the construction of suitable calculi for modal logics, and their application in the investigation of important classes of modal logics.

Data: CORDIS, © European Union