§2. BCK Games (with irreversible backtracking)
for Material Implication and Cut-free proofs

We introduce an interpretation of a generic mathematical statement through a game, representing a debate between two players, Eloise and Abelard, about the statement. Eloise claims the statement is true. Abelard claims that the statement is false. Each step in the game represents a logical argument in favor of the truth of the statement A (if given by Eloise), or against the truth of the statement (if given by Abelard). The new features of our games are the possibility, for Eloise, of "backtracking", i.e, of retracting any move finitely many times, in order to "learn" a better move.This game semantic does not allow to restore a retracted move. It can interpret implication and negation only as defined connectives, and only proofs without Cut rule. It can interpret some, yet not all, proofs using Excluded Middle.

Web page on Tarski Games with Backtracking:

Created by Mathematica  (October 20, 2006)