 Thus if \(\phi\) is \(P_i\), then player \(\exists\) wins at once if \(s\) is in \(P_i\), and otherwise player \(\forall\) wins at once. The formulas \(\psi \wedge \theta , \psi \vee \theta\) and \(\neg \psi\) behave as in Hintikka’s games above; for example \(\psi \wedge \theta\) instructs player \(\forall\) to choose whether the game shall continue as for \(\psi\) or for \(\theta\). If the formula \(\phi\) is \(\Box \psi\), then player \(\forall\) chooses an arrow from \(s\) to a state \(t\) (i.e. a state \(t\) such that the pair \((s, t)\) is in the relation \(R)\), and the game then proceeds from the state \(t\) according to the instructions \(\psi\). The rule for \(\Diamond \psi\) is the same except that player \(\exists\) makes the choice. Finally we say that the formula \(\phi\) is true at s in A if player \(\exists\) has a winning strategy for this game based on \(\phi\) and starting at \(s\).