On Infinitary Proof Theory of Logics of Information and Common Belief

摘要

Recently there has been a growing interest in applying non-classically based modal logics in the context of logics for agency and social behaviour. In particular, substructural or other information-based modal logics of knowledge and belief, or similar versions of PDL, have been designed. While basic modal extensions of substructural logics on one side, and classically based logics of common belief and other fixed point modalities, are relatively well understood when it comes to complete6ness and proof theory, with logics we have in mind it is not so. In this talk, we will mainly concentrate on logics of common belief. We will consider two natural ways of axiomatizing the common belief over a basic modal logic (Belnap-Dunn logic or distributive substructural logics, extended by normal diamond and box modalities): one finitary, which is the standard Kozen's axiomatization, and the other infinitary, with an infinitary rule replacing the induction rule and using finite approximations of the fixed points. The finitary axiomatization is used to obtain, using an algebraic (and coalgebraic) insight, the soundness of the infinitary rule. We will then concentrate on the infinitary part of the story and draw a general, duality based picture connecting the syntax and poset-based frame semantics of the infinitary axiomatizations, including a completeness argument based on a canonical model construction. Here, the infintary case differs from the usual finitary account of (non-classical) modal logics: in particular, one needs to use an appropriate version of Lindenbaum or Belnap Pair-Extension lemma. Finally, we use the above insight to discuss proof theory of such logics within the framework of display calculi.