Common Knowledge as a Coinductive Modality

Venanzio Capretta
Institute for Computing and Information Science (ICIS), Radboud University Nijmegen


I prove in Coq Aumann’s Theorem: In perfect information games, common knowledge of rationality implies backward induction equilibrium. The notion of common knowledge is formalized, using a coinductive definition, as a modality containing an infinite amount of information.

Full text