Intuitionistic Common Knowledge
For logicians and computer scientists working on epistemic logic, this work provides a foundational treatment of intuitionistic common knowledge, though it is incremental as it extends existing results.
The paper studies an intuitionistic version of common knowledge logic (ICK), providing axiomatizations, analytic cyclic sequent calculi, and proving soundness, completeness, finite model property, and decidability. It shows that proof-search and validity problems for all considered logics can be solved in exponential time.
We study an intuitionistic version of common knowledge logic (CK), called ICK, which was introduced by Jäger 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 validity problems of all considered logics can be solved in exponential time.