Backtracking Games with irreversible backtracking are no complete semantic for the Language of Arithmetic.

Irreversible backtracking is an incomplete semantic. For several classical theorems, Eloise has some winning strategy, but no recursive winning strategy in Tarski Games. Many theorems of Algebra, like Hilbert Base Theorem, can be interpreted through a recursive winning strategy by adding irreversible backtracking to Tarski Games. However, many theorems of Analysis, like Intermediate Value Theorem, cannot. For instance, Excluded Middle over ∀∃-formula is not valid in game semantic with irreversible backtracking (see §3 for an explanation).

There is a common reason for these incompletenesses. Assume Eloise makes a move, then she later believes she was wrong, and she retracts it. Still later, Eloise can find out she was wrong in believing to be wrong. In this case, she should come back to the retracted move, restore it, and continue the play from it. However, she cannot do it: in play with irreversible backtracking, retracting is irreversible, once you retract a move you never restore it back. Sometimes, the possibility of restoring a retracted move is essential in order to have a recursive winning strategy. This happens only for quite involved games, though.

When irreversible backtracking is not enough: Stolzenberg Principle. Stolzenberg principle says that all infinite 0/1 sequences (represented by some map f:N→{0,1}) have either infinitely many 0's, or infinitely many 1's. This formula is clearly true: if both 0's and 1's were finite, then the sequence itself would be finite, contradiction. Eloise has a winning strategy for this formula, but no recursive winning strategy, even if she uses irreversible backtracking.
Indeed, assume Abelard gives to Eloise some sequence f:N→{0,1}, claiming f has no infinitely many 0's, nor infinitely many 1's. Assume Eloise re-plays saying that there are infinitely many 0's, that is: t.∀x.∃y.(x≤y∧f(y)=0). Then Abelard re-plays giving some x=n, and asking for some y=m≥n such that f(m)=0. Assume Eloise finds none. Since Eloise can only look at finitely many values of f, this can happens because there is no such an m. Unfortunately, this can also happen because there is such a m, but Eloise is unable to find it. Therefore Eloise can believe she is wrong, and there are no infinitely many 0's, while in fact, she is right, and there are infinitely many 0's. She retracts the move t.∀x.∃y.(x≤y∧f(y)=0), she backtracks to the initial position of the game, and she moves t.∀x.∃y.(x≤y∧f(y)=1) this time. If she later finds out she is wrong, and there is some m≥n such that f(m)=0, she cannot restore the move t.∃y.(n≤y∧f(y)=0), and play y=m this time, because 1-backtracking is irreversible. Once Eloise retracts a move, the move is lost forever.

Is there any way Eloise can win in the game for Stolzenberg Principle, using only irreversible backtracking? No, there is not. Of course, Eloise can backtrack again to the initial position of the game, and move again t.∀x.∃y.(x≤y∧f(y)=1), hoping Abelard will play again x=n. But this is no winning strategy. Abelard could move x=n' this time. Again, Eloise could be unable to find some y=m'≥n' such that f(m')=0, even if, actually, there is some. Eloise could continue forever bactracking to the initial position, changing infinitely many times her move between t.∀x.∃y.(x≤y∧f(y)=0) and t.∀x.∃y.(x≤y∧f(y)=1). According to the rules of games with backtracking, if Eloise backtracks infinitely many times to the same position, she loses.

More incompleteness. In our semantic, there is no interpretation of Constructive Implication, and there is no interpretation of Cut Rule. We will add Constructive implication in §4, and Cut rule in §5.

Created by Mathematica  (October 20, 2006)