Common knowledge: finite calculus with a syntactic cut-elimination procedure

Brian Hill (1) , Francesca Poggiolesi (1)

1 IHPST - Institut d'Histoire et de Philosophie des Sciences et des Techniques

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.

Mots clés: philosophy of science

Domaines: Histoire, Philosophie et Sociologie des sciences

Brian Hill, Francesca Poggiolesi. Common knowledge: finite calculus with a syntactic cut-elimination procedure. Logique et Analyse, 2015, 58 (230), pp.279-306. ⟨halshs-00775822⟩