this issue
previous article in this issuenext article in this issue

Document Details :

Title: Common Knowledge
Subtitle: A Finitary Calculus with a Syntactic Cut-elimination Procedure
Author(s): POGGIOLESI, Francesca , HILL, Brian
Journal: Logique et Analyse
Volume: 230    Date: 2015   
Pages: 279-306
DOI: 10.2143/LEA.230.0.3141811

Abstract :
In this paper we present a finitary sequent calculus for the S5 multi-modal system with common knowledge. The sequent calculus is based on indexed hypersequents which are standard hypersequents refined with indices that serve to show the multi-agent feature of the system S5. The calculus has a non-analytic right introduction rule. We prove that the calculus is contraction- and weakening-free, that (almost all) its logical rules are invertible, and finally that it enjoys a syntactic cut-elimination procedure. Moreover, the use of the non-analytic rule can be restricted so that the calculus can be considered as suitable for proof search.

Download article