Common knowledge logic in a higher order proof assistant?

TL;DR

This paper explores the formalization of common knowledge logic within the Coq proof assistant, focusing on the inductive nature of the shared knowledge modality and analyzing the structure of provable theorems.

Contribution

It introduces a fixpoint approach to formalize common knowledge logic in Coq and examines the interaction between theory implementation and metatheoretical properties.

Findings

The fixpoint approach effectively captures common knowledge modalities.

The structure of provable theorems reveals insights into the interplay between theory and metatheory.

Experiments demonstrate the feasibility of formalizing common knowledge logic in proof assistants.

Abstract

This paper presents experiments on common knowledge logic, conducted with the help of the proof assistant Coq. The main feature of common knowledge logic is the eponymous modality that says that a group of agents shares a knowledge about a certain proposition in a inductive way. This modality is specified by using a fixpoint approach. Furthermore, from these experiments, we discuss and compare the structure of theorems that can be proved in specific theories that use common knowledge logic. Those structures manifests the interplay between the theory (as implemented in the proof assistant Coq) and the metatheory.