School of Computer Science
University of Nottingham
Thursday, 25 May 2017, 14:00
Cybernetica Bldg (Akadeemia tee 21B), room CYB-101
Slides from the talk [pdf]
Abstract: Common knowledge is a modality in epistemic logic: a group of agents has common knowledge of an event if they all know it and this knowledge is recursively known by everyone. It seems natural to see it as a coinductive operator: common knowledge of an event means that everyone knows it, everyone knows that everyone knows it, everyone knows that everyone knows that everyone knows it, and so on ad infinitum. We define it in a type-theoretic setting, with formalisations in the proof assistants Agda and Coq, and prove that it is equivalent to the traditional characterisation.
In the semantics of epistemic logic, a propositional formula is interpreted as an event, that is, a set of states or possible worlds (those in which the formula holds). Knowledge is represented as an equivalence relation on states: two states are equivalent if an agent can't distinguish them on the basis of individual information. Common knowledge is defined in terms of the transitive closure of the union of the individual knowledge relations.
We prove that our approach is equivalent to the traditional one in two ways. Firstly, our way of talking about knowledge as an operator on events satisfying some properties (essentially a semantic version of the modal logic S5) is equivalent to frame semantics, the traditional approach using equivalence relations. Secondly, we prove that our coinductive definition of common knowledge is equivalent to the one using transitive closure of the equivalence relations for each agent.
These results have been formalised in the two proof assistants Agda and Coq.
This is joint work with Colm Baston.