The Inductive and Modal Proof Theory of
             Aumann's Theorem on Rationality

    Rene Vestergaard* & Pierre Lescanne & Hiroakira Ono


Aumann's Theorem on Rationality says, slightly contentiously, that
``common knowledge of rationality leads to backwards-induction
equilibria''. We present a formalist development of the result in a
meta-theory with primitive support for proof and definition by
induction. Being proof-theoretic, rather than model-theoretic as
other efforts, our analysis shows in part that validity of the
result reduces to a so-called modal axiom T. Complementing the
particular axiom T of Aumann's set-up, we propose an alternative
axiom that results in ``decidable (local) rationality leads to
backwards-induction equilibria''. Aumann's result follows from ours
but not vice versa and the two axioms T appear to be independent.
Our development has been verified in full in the Coq proof assistant
(an auspiciously simple task, as it turns out) and we additionally
account for the formal underpinning of such tools.

*: corresponding