Backtracking Games (for intuitionistic logic).

Defining backtracking for intuitionistic logic. The backtracking game for t.A (or f.B) and intuitionistic logic is played over the judgement tree of t.A (of f.B). 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. When there is an ``f.'' in front, the roles of Eloise and Abelard are reversed. 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. The main feature of intuitionistic games is a strong restriction in the choice of i: either i is the index of any negative judgement, or i is the index of the last positive judgement. If Eloise moved from node j, now Eloise makes the move number i+1 from the node j. If Abelard moves from node j, now Abelard makes move number i+1 from the node j. The new move from node j can be different from the original move from node j.
Winner of the play. As in Tarski play, the first player who should move, and cannot, loses. 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.
Intuitionistic backtracking is reversible: Eloise can temporarily retract some negative judgement, then come back to the same node later, and recover it. Eloise can also retract a positive judgement, then come back to it, but only in the case the judgement is still the last positive judgement.

Intuitionistic Backtracking. Backtracking for intuitionistic games is also called just intuitionisitc backtracking, for short.

How Intuitionistic backtracking works. In intuitionistic backtracking, Eloise can move from a positive disjunctive judgement to any negative judgement of the play, and from a negative disjunctive judgement to the last positive judgement. If Eloise wins the play, the current position is usually a conjunctive positive judgement. Eloise can move to any negative judgement any finite number of times. If Eloise wins when the current position is a negative judgement, she wins the play, but she does not expect to win in this way. Eloise expects to win when the current position is a positive judgement. Eloise moves to a negative judgement only to observe the replies of Abelard. Eloise uses the re-plies of Abelard to find the right move from the last positive judgement. A move of Eloise from a disjunctive positive judgement must be the correct one first try, because Eloise cannot come back to any positive judgement before the last one, and change her previous move from a positive judgement. Eloise, instead, can play any number of times from the same negative judgement.

Intuitionistic backtracking and the notion of input/ouput. In intuitionistic backtracking, we interpret a move  t.A⊃B from t.A⇒B as a function call in programming language. Moves from t.A⊃B are f.A, t.B. We interpret the negative judgement f.A as an input gate Eloise to which Eloise can move any number of times, in order to observe the replies from Abelard, defending A. We interpret the positive judgement t.B as an output gate Eloise can use just once, sending the winning moves of the play, defending B. Moves of Eloise defending B are in function of the replies of Abelard defending A.

Theorem (Completeness of backtracking). The set of formulas of LCons (the language with constructive implication) for which there is some computable winning strategy for Eloise, in the game with intuitionistic backtracking, is exactly the set of formulas deducible in Intuitionistic Arithmetic extended with recursive ω-rule.

A sample game. Let A = ∃x.P(x) ∧ ∃y.Q(y) and B = ∃x'.∃y'.(P(x')∧Q(y')). We define an effective game semantic with backtracking for the formula  A⇒B and for Intuitionistic Arithmetic. The operational meaning of A⇒B is: there is an effective way of turning any evidence in favor of A into an evidence in favor of B. In this particular case, and evidence in favor of A is some vale x=a such that P(x), and some value y=b such that Q(b). An evidence in favor of B is a pair of values for x', y' such that P(z)∧Q(t). The obvious choice is taking x'=a, y'=b (we chose a trivial example on purpose).

We translate the informal argument above into a recursive winning strategy for Eloise, validating t.A⇒B.
  (move 1) The initial position is t.A⇒B  (a conjunctive judgement).
  (move 2) Abelard moves t.A⊃B.
  (move 3) Eloise moves f.A, attacking the hypothesis A.
  (move 4) Eloise moves f.∃x.P(x), attacking the left-hand side of A. (Normally, in a conjunction, Abelard would attack, but since there is an ``f.'' in front of A, roles are reversed, and Eloise attacks.) Abelard moves next, defending the truth of ∃x.P(x) (again, roles are reversed because there is an ``f.'').
  (move 5) Abelard replies moving some f.P(t), and claiming P(t) is true. Eloise claims P(t) is false (again, roles are reversed because there is an ``f.'').
  (move 6) Suppose P(t) is true. Then Abelard moves f.T and Eloise loses, but only temporarily.
  (move 7) Eloise backtracks to f.A (position 3). She plays f.∃y.Q(y) this time.
  (move 8) Abelard moves from f.∃y.Q(y), defending the truth of ∃y.Q(y) Therefore he replies choosing some f.Q(u), and claiming Q(u) is true.
  (move 9) Suppose it is. Then Abelard moves f.T and Eloise loses. Eloise has lost twice in a row, but this was expected. The primary goal of Eloise on f.A is not to win. If she does, she wins the whole play, but she does not expect to win. The primary goal of Eloise is to obtain from Abelard some arguments in favor of A, that is, some t,u such that P(t), Q(u) are true. This is indeed the case.
  (move 10) Eloise backtracks to t.A⊃B (the last positive judgement, position 2). This time, she moves t.B, a disjunctive judgement.
  (move 11) Eloise moves t.∃y'.(P(t)∧Q(y')).
  (move 12) Eloise moves t.P(t)∧Q(u).
  (move 13) Abelard replies t.P(t). Now Abelard loses, because P(t) is true. Indeed,
  (move 14) Eloise moves t.T, a true conjunctive atom. Abelard drops out (there are no ordinary moves, and Abelard cannot backtrack).
Remark that if Abelard, at step 13, moves t.Q(u), he loses as well, because Q(u) is true.

Created by Mathematica  (November 11, 2006)