 From the vantage point of GTS, independence friendly first-order logic differs from first-order logic in that semantic games correlated with formulas of the former are, in general, games of imperfect information, while any game associated with a first-order formula is a game of perfect information. Consider the game for \(\forall x\exists y\forall z(\exists w/\forall x) R(x, y, z, w)\), played on a model \(M\). A play of this game proceeds exactly as plays of the game corresponding to \(\forall x\exists y\forall z\exists w R(x, y, z, w)\). First, player 1 chooses an individual \(a\), whereafter player 2 chooses an individual \(b\). Then player 1 proceeds to pick out a further individual \(c\), to which player 2 responds by choosing an individual \(d\). So a play of the game has come to an end. The play is won by player 2, if indeed \(R(a, b,c, d)\) holds in \(M\); otherwise it is won by player 1. But \(\exists w\) was marked as independent of \(\forall x\) – why does not this fact show in any way in the course of a play?