§5.1 Introducing BCK Games for Cut.

Material and Constructive Implicaton. This is an advanced section. We assume the reader already knows about BCK Games for Limit Computable Mathematics and for Classical Arithmetic. We do not assume the reader knows about game semantic for Constructive Implication A⇒B. Therefore we duplicate most examples, and we write them first using Material Implication A→B, then using Constructive Implication A⇒B. Material Implication A→B is a concept for Classical Logic, and it is just short for ¬A∨B.

A symmetric notion of game. In this section both plays can backtrack, and the play becomes fully symmetric. Also the definition of view-tree and sequent-view become symmetric. Switching t, f switches the role of Abelard and Eloise.
Dual of a strategy. Assume we have a strategy S of Eloise over  t.A. By switching t, f, we obtain a strategy S' of Abelard over f.A. S' is winning for Abelard if S is winning for Eloise.
Dialogue between strategies. Assume we have a strategy S1 of Eloise over t.A⇒B, and a strategy S2 of Abelard over f.A. We can make S1 play against S2 over f.A, and against any strategy of Abelard over t.B. If we skip all moves over f.A, we define a strategy in this way a strategy S3 of Eloise over t.B. We call this operation a dialogue between strategies: it defines a strategy S3 of Eloise over t.B, from a strategy S1 of Eloise over t.A⇒B, and a strategy S2 of Abelard over f.A.If S1 is winning for Eloise, and S2 for Abelard, then S3 is winning for Eloise over t.B. (Indeed, S1 wins over t.A⇒B, but it cannot win over f.A, because S2 is winning for the opponent on f.A. Therefore S1 wins over t.B)
Interpreting Cut Rule. Assume we have a winning strategy S1 of Eloise over t.A⇒B, and a winning strategy S2 of Eloise over t.A. In order to interpret Cut Rule, we have to define a winning strategy for Eloise on t.A. We first turn S2 into a winning strategy S2' for Abelard on f.A. Then, using a dialogue between S1 and S2', we define a winning strategy S3 for Eloise on t.A.

Created by Mathematica  (November 11, 2006)