 The syntax of \(\mathbf{IFL}\) can be generalized by removing the restriction according to which the negation sign may only appear as prefixed to an atomic  formula.[24].  In order to interpret negation in GTS, two roles are added as a new ingredient in the specification of the games: those of ‘verifier’ and ‘falsifier.’ Initially, player 1 has the role of ‘falsifier’ and player 2 that of ‘verifier.’ The roles may get switched, but only for one reason: when an occurrence of the negation symbol is encountered. All clauses defining semantic games must be rephrased in terms of roles instead of players. It is the player whose role is ‘verifier’ who makes a move for disjunctions and existential quantifiers, and similarly the player whose role is ‘falsifier’ who moves for conjunctions and universal quantifiers. When a formula \({\sim}\psi\) is encountered, the players change roles and the game continues with \(\psi\). Finally, if the encountered atomic formula is true, ‘verifier’ wins and ‘falsifier’ loses, otherwise the payoffs are reversed. The negation \({\sim}\) is variably referred to as strong negation, dual negation, or game-theoretical  negation.[25]  It works as one would expect: \(\phi\) is false in \(M\) iff its negation \({\sim}\phi\) is true therein (cf. Sandu 1993). 