Intuitionistic Games: Determinacy,Completeness, and Normalization

We investigate a simple game paradigm for intuitionistic logic, inspired by Wajsberg’s implicit inhabitation algorithm and Beth tableaux. The principal idea is that one player,  ?ros, is trying to construct a proof in normal form (positions in the game represent his progress in proof construction) while his opponent, ?phrodite,  attempts to build a counter-model (positions or plays can be seen as states in a Kripke model). The determinacy of the game (a proof-construction and a model-construction game in one) implies therefore both completeness and semantic cut-elimination.