
TL;DR
This paper introduces an intuitionistic version of common knowledge logic (ICK), providing axiomatizations, sequent calculi, and complexity results for various models, including S4 and S5.
Contribution
It extends intuitionistic propositional logic with common knowledge operators, offering sound, complete, and decidable systems with automated proof-search.
Findings
Soundness and completeness of the axiomatizations and calculi.
Finite model property and decidability established.
Proof-search and validity problems are solvable in exponential time.
Abstract
We study an intuitionistic version of common knowledge logic (CK), called ICK, which was introduced by J\"ager and Marti. ICK extends intuitionistic propositional logic (IPL) by multiple box modalities interpreted as knowledge operators for various agents and a common knowledge operator. Formulae are interpreted over birelational Kripke models satisfying a simple interaction principle between the intuitionistic order and the modal accessibility relations. Furthermore, we consider the restriction to reflexive, S4 and S5 models. We present axiomatizations as well as analytic cyclic sequent calculi for all considered logics and prove them to be sound and complete. Furthermore, we establish the finite model property and decidability, show that proof-search in the cyclic calculi can be automated, provide a translation of CK over S5 into ICK over S5 and establish that the proof-search and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
