AbstractThe aim of this work is to propose a logical framework for representing interacting agents in the context of extensive form games. Because of the importance of the temporal dimension provided by such games, we create a modal epistemic logic that allows to quantify over both strategies and vertices within the game tree. The first part of the article is devoted to the logic itself with the definition of its language and its semantics. In order to illustrate the use of this logic, we define, in the following part, the concept of rationality in the case of extensive form games and the backward induction concept, as they are defined by Robert Aumann. Based on these definitions, we then provide a syntactic proof of Aumannʼs theorem that states the following: “for any non degenerate game of perfect information, common knowledge of rationality implies the backward induction solution”. We finally propose an in-depth formal analysis of the hypotheses that are needed to prove such a theorem.