3. Adding Reversible BacktrackingHighly non-effective parts of proofs: Excluded Middle over non-semidecidable statements. There are, in Mathematics, class of statements we cannot even semi-decide. Recall that we can semi-decide a class of statements if we can compute their truth value by some algorithm which is terminating if the statement is true, but which, possibly, can continue forever when the statement is false. Not semi-decidable statements are highly non-effective. If we cannot semi-decide a statement, then, as we said in the previous section, we cannot we cannot learn its truth value using learning in the limit as described in the previous section. But there is more: assume a proof uses Excluded Middle over these (not semi-decidable) statements. Then, as we said again in the previous section, we cannot interpret it as a programs using Tarski with "irreversible backtracking". This kind of proofs, unfortunately, is quite common in classical logic. Reversible backtracking and non-monotonic learning. These proofs can be interpreted by adding "reversible backtracking" to Tarski Games. Reversible backtracking allows to restore a move belonging to a part of the history we previously erased, because it was coming after a retracted move. Indeed, it can happen, in a play, that we retract a move because we consider it wrong. Later on, however, we can find out that we were wrong in believing that we were wrong. In this case, using reversible backtracking we restore the retracted moves, and all moves which were erased because of this retraction. The only constraint, as in the case of irreversible backtracking, is that we cannot retract infinitely many times the same move, otherwise we lose the play. This way of learning in the limit fits in a programming style called non-monotonic learning . In non-monotonic learning, indeed, a statement in our knowledge base can be replaced by its negation. Any guess retracted because in contradiction with this knowledge, therefore, can be un-retracted. Not surprisingly, Tarski Games with reversible backtracking are complex. It is curious that they were discovered several years before Tarski Games with Irreversible Backtracking, which are much simpler. Reversible backtracking as a one-to-many play. In order to form a mental picture of reversible backtracking, it is useful to imagine that the player defending a statement, Eloise, is not fighting again a single opponent attacking one statement, Abelard. Rather, she is playing a tournament, against a whole array of Abelards, but she is fighting against only one of them at the time. Consider the case Eloise retracts a move and erases some positions which are part of the history of the play. Then the particular Abelard fighting Eloise never cares about these positions again, yet these positions are not forgotten. Some other Abelards are detached from the array to defend them, one Abelard per position. Each Abelard waits (possibly forever) for Eloise to change her knowledge base, un-retract the move she just retracted, and restore the position he belongs to. If and when this happen, this particular Abelard starts again defending the position. Eloise can choose which Abelard to attack next, by choosing which move to restore (if any). The situation is similar to some games played over the net using a service called "auto-match". If we use auto-match, we can have several open plays with different opponents, and we can choose which play to continue (in real plays, of course, our opponent will not wait forever our move). For sake of simplicity, we do not allow Abelard to backtrack. This means that Eloise will face an array of Abelards, while each Abelard is facing the same Eloise. The idea is that Eloise learns the correct move by trial-and-error, retracting moves. Each Abelard, instead, is omniscient, and knows the best move without having to learn it. As long as we have to provide a strategy for Eloise, but not for a whole array of omniscient Abelards, this idea works. Later on, when interpreting a logical rule called Cut Rule, we will have to provide a strategy for each Abelard, too, and this idea will no more work. More information and examples are available in the subsite:
We also provide a Mathematica program, BCK, helping two players taking the role of Eloise and of (the array of) Abelards, and providing a tree-like picture of the state of the play (positions, moves, backtracking, erased moves etc.). Reversible Backtracking in principle can interpret all proofs using classical logic and reasoning by induction, but ... ... Reversible Backtracking cannot interpret some logical rules which are superfluous in principle, yet are useful to make proofs simpler and shorter. A logical rule which we cannot interpret is the rule for constructive implication ("if we proved B using A, then we proved A=>B"). Another logical rule we cannot interpret is Cut Rule ("if we proved B using A, and we proved A, then we proved B"). These rules will be considered in the last two sections of this site.  |