Fiche du document
2015
- handle: 10670/1.yplls0
- halshs: halshs-00775822
info:eu-repo/semantics/OpenAccess
Mots-clés
philosophy of scienceSujets proches
Infinitesimal calculus Analysis (Mathematics) Fluxions (Mathematics) Limits (Mathematics)Citer ce document
Brian Hill et al., « Common knowledge: finite calculus with a syntactic cut-elimination procedure », HAL-SHS : histoire, philosophie et sociologie des sciences et des techniques, ID : 10670/1.yplls0
Métriques
Partage / Export
Résumé
In this paper we present a finitary sequent calculus for the S5 multi-modalsystem with common knowledge. The sequent calculus is based on indexed hypersequentswhich are standard hypersequents refined with indices that serve to showthe multi-agent feature of the system S5. The calculus has a non-analytic rightintroduction 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 syntacticcut-elimination procedure. Moreover, the use of the non-analytic rule can berestricted so that the calculus can be considered as suitable for proof search.