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.