Tarski Games with retractable moves

A Game Semantic for Mathematical Proofs

Menu

1. Introduction to Tarski Game Semantic
2. Adding Irreversible Backtracking
3. Adding Reversible Backtracking
4. A Semantic of Constructive Implication
5. A Semantic of Cut
6. A Program implementing Tarski Games with backtracking

4. A Semantic of Constructive Implication


Intuitionistic Logic and constructions . A proof of a mathematical statement using Excluded Middle is called a classical proof, a proof not using Excluded Middle an intuitionistic proof. Intuitionistic proof are naturally interpreted as "constructions". A construction is more than a proof: a construction is a kind of program, computing (and not just "learning" by retracting previous choices) some extra information about the statement. For instance, a construction for a disjunction "A or B" provides a construction either for A or for B, therefore it says whether A is true or B is true. A construction for "for some x, P(x)" provides some value v for x, and some "construction" for P(v), therefore it says which instance of P(x) is true. For more details we refer to the section "Intuitionistic Logic" of Stanford on-line Encyclopedia of Philosophy .

Material implication and constructive implication. "A implies B" is interpreted in classical logic as the so-called material implication: "either A is false or B is true". "A implies B" is interpreted in intuitionistic logic with the more natural constructive implication: "if we assume A, we can prove B". A construction for "A implies B" is map, waiting for a construction for A as input, then returning as output a construction for B. In Classical Logic, the two implications are equivalent, therefore in principle we could drop constructive implication. But it is not wise to do so, because constructive implication is often used, even in classical proofs, in order to make proofs simpler and shorter. For this reason, in this section we extend Game Semantic from the previous sections in order to include Intuitionistic Logic.

Interpreting Intuitionistic Logic in Game Theory. The first game semantic for Intuitionistic Logic was defined by Lorenzen in 1960. This semantic can be re-expressed in our framework, by modifying Tarski Game Semantic with "reversible backtracking" outlined in the previous sections. Suppose we want to interpret "A implies B" as a game.
  • (Input/Output). We intepret the hypothesis A by a game in which the roles of the two players are switched. Eloise, who is usually defending the truth of a formula, is attacking the truth of the hypothesis A. Abelard, who is usually attacking the truth of a formula, is defending the truth of the hypothesis A.
  • (Input Reusing). We allow to Eloise to retract moves, and then possibly retract her retraction, and so forth, but with some restrictions.Eloise can retract a move only if the move was done to attack some hypothesis (say, A). Eloise cannot retract a move done defending a conclusion (say, B).
  • (Waiting for an Input). The play over "A implies B" is started by Abelard. The only move available by Abelard is asking to Eloise to argue in favor of "A implies B". Eloise cannot start playing on "A implies B" until Abelard allows her to do it.


    • Game Rules and constructions. All the game rules above can be explained thinking that Eloise takes the role of a construction for "A implies B".
  • (Input/Output). A construction for "A implies B" takes a construction for A and returns a construction for B. The construction for A is taken from the outside world: we assume this is Abelard's task. Therefore it is considered to be unsafe. Thus, Eloise attacks it, in order to check if it is correct. The construction for B, instead, is returned by Eloise, therefore Eloise must defend its correctness.
  • (Input Reusing). The fact that Eloise can retract a move from A means that Eloise can check the correctness of the "input construction" for A given by Abelard as many times as she wants to. The fact that Eloise cannot retract a move from B means that Eloise plays the role of a construction for B. As we said, a construction for B has to compute some extra information about B, and cannot "learn" it: therefore no retracting of moves is allowed to Eloise while defending B.
  • (Waiting for an Input). The fact that Eloise starts defending "A implies B" only when Abelard asks her to do so expresses the fact that Eloise takes the role of a map from constructions for A to constructions for B. A map is not active by its own: a map has to wait until the program it belongs to applies it to some input. Therefore Eloise waits for Abelard to allow her to move.


    • For sake of simplicity, we do not allow Abelard to backtrack. As we said in the previous section, this can be explained by saying that Eloise faces an array of Abelards. There is one Abelard defending each previous position of the play, waiting for Eloise to retract the move from this position, and to play again from this position. Each Abelard, instead, is facing the same Eloise. Later on, when interpreting a logical rule called Cut Rule, the situation will change.

    For more information and examples, visit the subsite:

    4. Backtracking Games for Constructive Implication



    We also provide a Mathematica program, BCK, helping two players taking the role of Eloise and of (the array of) Abelards in a game for Intuitionistic Logic, and providing a tree-like picture of the state of the play (positions, moves, backtracking, erased moves etc.).



    Above: Paul Lorenzen introduced in 1960 a game semantic for Intuitionistic Logic.
    Prev.: 3. Adding Reversible Backtracking . Up: 4. A Semantic of Constructive Implication. Next: 5. A Semantic of Cut .
    This site has been generated using a Small Site Generator, written in the Mathematica language by Stefano Berardi.