Propositional game logic

We define a propositional logic of games which lies in expressive power between the Propositional Dynamic Logic of Fischer and Ladner [FL] and the µ-calculus of Kozen [K]. We show that the logic is decidable and give a very simple, complete set of axioms, one of the rules being Brouwer's bar induction. Even though decidable, this logic is powerful enough to define well orderings. We state some other results, open questions and indicate directions for further research.