FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
The Coinductive Formulation of Common Knowledge

Authors: Venanzio Capretta and Colm Baston

Paper Information

Title:The Coinductive Formulation of Common Knowledge
Authors:Venanzio Capretta and Colm Baston
Proceedings:ITP Papers
Editors: Jeremy Avigad and Assia Mahboubi
Keywords:epistemic logic, common knowledge, coinductive types, type theory, proof assistants
Abstract:

ABSTRACT. We study the coinductive formulation of common knowledge in type theory. We formalise both the traditional relational semantics and an operator semantics, similar in form to the epistemic system S5, but at the level of events on possible worlds rather than as a logical derivation system. We have two major new results. Firstly, the operator semantics is equivalent to the relational semantics: we discovered that this requires a new hypothesis of semantic entailment on operators, not known in previous literature. Secondly, the coinductive version of common knowledge is equivalent to the traditional transitive closure on the relational interpretation. All results are formalised in the proof assistants Agda and Coq.

Pages:16
Talk:Jul 09 15:00 (Session 49C)
Paper: