 For the remainder of this section, \(\mathcal{L}\) is a first-order language built as usual upon the propositional connectives, the quantifiers, a denumerable set of individual variables, a denumerable set of individual constants and a denumerable set of predicate symbols (each with a fixed arity). This first-order language is then extended with two labels O and P, standing for the players of the game, and the two symbols “\(\state\)” and “\(\rqst\)” standing respectively for statements and requests.