Une stratégie S est dite gagnante si toutes ses parties maximales sont gagnées par B, et si, de plus, elle n'a pas de partie infinie : une partie infinie de S est un chemin infini dans G dont tous les préfixes (finis) pairs sont dans S.
Questions de finitude: la question des parties infinies est toujours embarrassante. On préfère les jeux où il n' y pas de parties infinies. Et on aime encore plus les jeux "fortement finis" où, pour chaque position initiale p, on peut majorer la longueur des parties commençant en p. Mais on ne s'en tirera pas à si bon compte. A défaut de trouver des règles qui proscrivent les parties infinies, il faudra trouver des règles qui permettent de repérer le tricheur qui rend la partie infinie pour empécher son adversaire de gagner. Par exemple on pourra autoriser un nombre fini de coupures, et disqualifier le joueur qui fait, dans une même partie, une infinité de coupures.
Une position est encore un graphe, encore bipartite (B/N) avec
Il faut penser les sommets comme des joueurs formant deux équipes (B/N), chaque joueur cherchant à prouver son séquent, qu'on peut former en y mettant à gauche les formules entrantes et à droite les formules sortantes. Et chaque équipe cherchant à se débarrasser définitivement du jeton. Pour la commodité, on considérera aussi des graphes avec des formules négatives, pour représenter la position obtenue en changeant, là où il faut le signe des arcs et des formules.
Pour les formules, il y a quatre constantes , 0 et 1 qui sont positives, et \top et \bot qui sont négatives. Et puis quatre opérations : \oplus et \otimes qui donnent un résultat positif et \avec et \par qui donnent un résultat négatif.
La négation (linéaire) F \mapsto nonF est une involution définie comme suit: elle échange 1 et \bot, ainsi que 0 et \top. Ensuite elle échange A \oplus B et nonA \avec nonB, ainsi que A \otimes B et nonA \par nonB.
Maintenant on explique les coups de ce jeu.
Il y a d'abord les coups passifs, qui sont très simples. Il s'agit tout simplement, pour le joueur qui a le jeton, de le faire passer, le long d'un arc entrant, au joueur voisin. Il faut penser qu'il demande à son voisin d'activer, ou de déstructurer la formule concernée.
Et maintenant il y a les coups actifs, en gros un par formule positive.
Maintenant, à la demande générale, on va donner des exemples. Pour que ces exemples ressemblent à ce dont on a l'habitude, on utilisera l' implication linéaire -o , qui est définie par A -o B := nonA \par B.