 Failure of bivalence. There are sentences \(\phi\) of \(\mathbf{IFL}\) and models \(M\) such that \(\phi\) is neither true nor false in \(M\). Consider evaluating the sentence \((\forall x)(\exists y/\forall x) x = y\) on a model whose domain has exactly two elements, \(a\) and \(b\). Player 1 has no winning strategy. If he chooses \(a\) to interpret \(\forall x\), he loses the play in which player 2 chooses \(a\) to interpret \((\exists y/\forall x)\). Similarly, if player 1 chooses \(b\), he loses the play in which player 2 likewise chooses \(b\). Neither does player 2 have a winning strategy. Her strategy functions for \((\exists y/\forall x)\) are constants (zero-place functions). There are two such constants available: \(a\) and \(b\). Whichever one of these strategy functions player 2 assumes, there is a move by player 1 defeating it. If player 2 opts for \(a\), player 1 wins the play in which he chooses \(b\); and if player 2 applies \(b\), player 1 wins the play in which he chooses \(a\). Game \(G(\phi , M)\) is non-determined: neither player has a winning  strategy.[26]  The notion of non-determinacy may be extended to formulas as well: