 of elements of \(\Omega\). Infinite sequences of elements of \(\Omega\) are called plays. Finite sequences of elements of \(\Omega\) are called positions; they record where a play might have got to by a certain time. A function \(\tau\) (the turn function or player function) takes each position \(\mathbf{a}\) to either \(\exists\) or \(\forall\); if \(\tau(\mathbf{a}) = \exists\), this means that when the game has reached \(\mathbf{a}\), player \(\exists\) makes the next choice (and likewise with \(\forall)\). The game rules define two sets \(\W_{\forall}\) and \(\W_{\exists}\) consisting of positions and plays, with the following properties: if a position \(\mathbf{a}\) is in \(\W_{\forall}\) then so is any play or longer position that starts with \(\mathbf{a}\) (and likewise with \(\W_{\exists})\); and no play is in both \(\W_{\forall}\) and \(\W_{\exists}\). We say that player \(\forall\) wins a play \(\mathbf{b}\), and that \(\mathbf{b}\) is a win for \(\forall\), if \(\mathbf{b}\) is in \(\W_{\forall}\); if some position \(\mathbf{a}\) that is an initial segment of \(\mathbf{b}\) is in \(\W_{\forall}\), then we say that player \(\forall\) wins already at \(\mathbf{a}\). (And likewise with \(\exists\) and \(\W_{\exists}\).) So to summarise, a logical game is a 4-tuple \((\Omega , \tau\), \(\W_{\forall}\), \(\W_{\exists})\) with the properties just described.