2. Adding Irreversible BacktrackingThe non-effective part of proofs: Excluded Middle. If we want an effectively given game model of proof, with the ultimate goal of "running" proofs, we face the following problem. Mathematical reasoning includes classical logic, and classical logic includes some steps with no obvious "effective" interpretation at all. We are speaking of the logical axiom of Excluded Middle, used in proofs under many different forms. Excluded Middle allows to reason by case over the truth value of a statement, even if the actual truth value of the statement is, in fact, unknown. We choose a statement and we say that if the statement is true, the proof is done in some way, if the statement is false the proof is done in some other way. An effective interpretation of this statement would require first to decide, in some mechanical way, whether a generic statement is true or false. By Godel's incompleteness Theorem, however, there is no mechanical way of deciding whether a generic mathematical statement is true or false. Therefore no "naive"effective interpretation of Excluded Middle exists. Learning algorithms. Computing the truth value of a generic mathematical statement is not effectively possible: the next better thing we can do is "learning in the limit" these truth values. "Learning in the limit"is a programming style allowing to produce guess about the value we are looking for, and retract these guesses finitely many times if our knowledge increases, and our guess contradicts a new knowledge. A value is considered to be "learned in the limit" if it "stabilizes", that is, if it is no more retracted. Learning in the limit fits in the Monotonic Learning paradigma: we assume our knowledge base can only increase, and therefore if a guess contradicts the knowledge base at some step, it will contradict it forever.(more on Monotonic Learning can be found in theAI site of Michigan University).At first sight, a Learning in the limit could look a too weak solution for a problem, but this is not the case. Many practical problems do not require an exact solution, only a solution surviving to many checking, and this kind of solution can, indeed, be obtaining by a learning algorithm. Besides, when we can decide whether a result is correct (and this is often the case), we can decide when a learning algorithm "stabilizes"to the correct value. In this case we can turn any algorithm learning in the limit a value into an algorithm computing the same value. Learning the truth value of a statement by retractable guesses. A statement is semi-decidable if there is a possibly divergent algorithm computing its truth value, andwhenever the statement is true the algorithm converges to true.We can learn the truth of any semi-decidable statement by a single retractable guess, as follow. We first assume that the statement is false. If, eventually, the semi-decision algorithm stops saying that the statement is true, we retract our guess and we say that the statement is true. If the statement is indeed true, the semi-decision procedure will eventually stop saying that the statement is true, if the statement is false, this will never happen. In both cases, the learning algorithm stabilizes to the correct truth value. Therefore we can use learning algorithms to model at least some classical proofs, those using Excluded Middle over semi-decidable statements. Tarski games with Irreversible Backtracking. We represent (monotonic) learning algorithms in Tarski game semantic by adding the possibility of retracting finitely many times a move, erasing each time the whole play history after this move. If a player retract infinitely many times the same move loses. We call "irreversibly bactracking" the act of retracting a move and erasing (forever) the rest of the history. Later on, we will also consider a reversible form of backtracking (see the Menu). For sake of simplicity, we only allow the player defending the statement, Eloise, to "backtrack". The player attacking the statement, Abelard, cannot "backtrack". The idea is that Eloise learns the correct move by trial-and-error, retracting moves. 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 the "omniscient" Abelard, this idea works. Later on, when interpreting a logical rule called Cut Rule, we will have to provide a strategy for Abelard, too, and this idea will no more work: we are not omniscient, therefore we cannot provide an omniscient strategy. We include some examples of Tarski play with "irreversible backtracking" in the subsite:
We also provide a Mathematica program, BCK, helping two players taking the role of Eloise and ofAbelard, and providing a tree-like picture of the state of the play (positions, moves, backtracking, erased moves etc.). Tarski Games with Irreversible Backtracking are not an interpretation of all proofs. These examples also show that, even adding Irreversible Backtracking, Tarski game interpretation is falling short from our goal. Indeed, we can interpret in this way only proofs using Excluded Middle over semi-decidable statements. These proofs are called Limit Computable Mathematical proofs, or LCM proofs for short. Not all proofs fall in this class. What we need is an interpretation of all mathematical proofs, and this will be achieved in the next section by allowing backtracking to be "reversible".  |