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