Intuitionistic Common Knowledge

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 validity problems of all considered logics can be solved in exponential time.