Explicit Evidence Systems with Common Knowledge

TL;DR

This paper introduces a multi-agent justification logic incorporating evidence for individual agents and common knowledge, providing a formal semantics, and analyzing its properties and relation to existing logics.

Contribution

It develops a new multi-agent justification logic with semantics, extending previous logics and relating to multi-agent modal logic S4 with common knowledge.

Findings

Soundness and completeness of the logic established

Finite model property proven

Relation to existing logics clarified

Abstract

Justification logics are epistemic logics that explicitly include justifications for the agents' knowledge. We develop a multi-agent justification logic with evidence terms for individual agents as well as for common knowledge. We define a Kripke-style semantics that is similar to Fitting's semantics for the Logic of Proofs LP. We show the soundness, completeness, and finite model property of our multi-agent justification logic with respect to this Kripke-style semantics. We demonstrate that our logic is a conservative extension of Yavorskaya's minimal bimodal explicit evidence logic, which is a two-agent version of LP. We discuss the relationship of our logic to the multi-agent modal logic S4 with common knowledge. Finally, we give a brief analysis of the coordinated attack problem in the newly developed language of our logic.