Common Knowledge as a Coinductive Modality

Abstract

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