5. A Semantic of CutA Game Semantic for Cut Rule. In this section we extend our Game Semantic in order to include a rule which is in principle superfluous, because it is derivable from the other rules: Cut Rule. Abbreviate "B assuming A" with "A|-B". Then Cut Rule says: "if we derive A|-B, and we derive A, then we derive B". In the term of games, we have to show that if Eloise has a winning strategy for A|-B, and for A, then she has a winning strategy for B. The winning strategy for A|-B is not yet a winning strategy defending B, because sometimes it moves attacking the assumption A. In some plays, this strategy can win not while it is defending B, but while it is attacking A. In this case, the victory is not a victory in the game for B. Interpreting Cut Rule by switching the role of the two players. A first idea is: whenever Eloise moves over A instead of over B, we make her play against a winning strategy for Abelard defending A. In this way Eloise cannot win over A, and she has eventually to move over B again, and to win while defending B. The problem is now to define a winning strategy for Abelard defending A. We have by assumption a winning strateg for Eloise defending A, and a second idea is: switch the role of the two players over A, in order to define a winning strategy for Abelard defending A. From a logical viewpoint this idea works, because Eloise and Abelard use the same kind of arguments while defending a formula A. From the viewpoint of game rules this idea does not work, because we allow Eloise to backtrack, we do not allow Abelard to backtrack, therefore we cannot exchange the role of the two players. A Tarski game in which both players can "backtrack": a many-to-many play. In order to interpret Cut Rule by switching the role of the two players, we have to extend our Game Semantic making it symmetrical. Therefore we allow both players to "backtrack", or retract moves. A colorful way of describing the resulting situation is that one array of Eloises and one array of Abelards face in a tournament, but only one Eloise and one Abelard are fighting at each step of the tournament. Consider the case the particular Eloise on turn retracts a move and erases some positions which are part of the history of the play. Then the particular Abelard fighting this particular Eloise never cares about these positions again: yet, these positions are not forgotten. Some Abelards are detached from the array to defend them, one per position. Each of theses Abelards is paired with this particular Eloise, and waits (possibly forever) for her to restore the position he belongs to. If and when this happen, this particular Abelard starts again defending the position against this particular Eloise. Each Eloise can choose which Abelard to attack next, among the ones she is paired with, by choosing which move to restore (if any). The situation of each Abelard is perfectly symmetrical, he is paired with many Eloises, if he erases some positions then the Eloise fighting him never cares about them again, yet these positions are not forgotten. Some Eloises are detached from the array to defend them, one per position. Each of these Eloises is paired with this particular Abelard, and waits (possibly forever) for him to restore the position she belongs to. Each Abelard can choose which Eloise to fight, among the ones she is paired to. For more informations and examples, look at the subsite:
 |