Backtracking Games (with reversible backtracking).

Defining reversible backtracking. The backtracking Game for t.A (or f.B) with reversible backtracking is played over the judgement tree of t.A (of f.B). The positions of the game are the nodes of the tree. The goal of Eloise is to convince Abelard that A is true (that B is false). The goal of Abelard is always the opposite of the goal of Eloise. In t.A, we say that Eloise defends A and Abelard attacks A. In f.B, we say that Eloise attacks B and Abelard defends B.
The play runs as Tarski play (see the section ``Tarski plays''), except that Eloise has a new kind of moves: backtracking moves. Instead of moving from the current node i, Eloise can come back, or ``backtrack'' to some node number j<i, and temporarily retracts the nodes j+1, ..., i from the Tarski play. What happens next depends on which player made the move from position j. If Eloise moved from node j, now Eloise makes the move number i from the node j, instead of from position i-1, as she would in Tarski games. If Abelard moved from node j, now Abelard makes move number i from the node j, instead of from position i-1, has he would in Tarski games. The obvious yet relevant feature of backtracking is: the new move from node j can be different from the original move from node j.
In games with reversible backtracking, retracting a node is reversible: Eloise can, later, backtrack to some node k among the retracted nodes j+1, ..., i-1. A way of picturing it is to imagine that there is one Eloise but an array of Abelard, and that whenever the nodes j+1, ..., i-1 are retracted, one Abelard per node is detached from the array to defend the node. Whenever Eloise recover the node, she finds some Abelard acquainted with the position and waiting to face her.
Winner of a play. As in Tarski play, the first player who should move, and cannot, loses. There is an additional rule: Eloise cannot change a move infinitely many times, that is, she cannot come back infinitely many times to the same node j. We express this by the following rule:
                         Eloise loses all infinite plays.

Reversible backtracking and "non-monotonic learning". In reversible backtracking, when we find out that we were wrong in retracting a previous move, we can restore it. Reversible backtracking is a sound and complete translation of the informal notion of learning by ``trial-and-error''. Indeed, if we learn by trial-and-error, we may later find out we were wrong, but also find out that we were wrong in believing we were wrong. In this case, we can recover an hypothesis that we retracted for a while. Indeed, recovering a retracted move is allowed in reversible backtracking. This is not possible, instead, with irreversible backtracking. With irreversible backtracking, we can only retract an hypothesis, we never recover it.
From a theoretical viewpoint, reversible backtracking fits in a programming style called "non-monotonic learning". Eloise has a knowledge base  growing with time in a non-monotonic way: sometimes, she can replace a fact by its negation. In this case, a move retracted because it was wrong according to the previous knowledge, can be considered correct and un-retracted if some fact in the knowledge base is replaced by its negation.

Abelard cannot backtrack. We assume Abelard is "omniscient", and knows the better move without learning it by "trial-and-error". In other word, we do not allow Abelard to backtrack, but also, we do not bound Abelard to have an effective strategy, expressible by a program. Eloise, instead, can retract (or un-retract) a move finitely many times, but she is bounded to have an effective strategy, expressible by a program.

Backtracking. Reversible backtracking is also called just backtracking, for short. It is the most general notion of backtracking.

In which case is reversible backtracking useful? In all cases in which we can use irreversible backtracking, we can use reversible backtracking as well. Therefore all examples from the previous section apply. For some formulas, we have no effective winning strategy using irreversible backtracking, but some effective winning strategy with reversible backtracking. This is the case of Excluded Middle for 2-quantifier formulas, and of Stolzenberg Principle: see the end of this section. This is also the case of Tarski games associated to Koenig's Lemma for effectively enumerable trees, and of many theorems of Elementar Analysis, like the Intermediate Value Theorem.

Theorem (Completeness of backtracking). Let S be the set of formulas A of L (the language with material implication) for which there is some computable winning strategy for Eloise, in the game over A with irreversible backtracking. S is exactly the set of true formulas in Classical Arithmetic.

Created by Mathematica  (October 20, 2006)