## The coinductive formulation of common knowledge

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.

Tarmo Uustalu

Last update 25 May 2017