Merging intuitionistic and irreversible backtracking.

In a proof we can merge the use of constructive implication and Classical Logic. Even in Classical reasoning, proofs with constructive implication are easier to follow.

In order to interpret Classical proofs with constructive implication, we merge intuitionistic backtracking with irreversible backtracking (if we want Limit Computable Mathematics and constructive implication) or with reversible bactracking (if we want full Classical Logic and constructive implication). The language is LCons (see the first subsection of this section). The game rules are obtained merging the rules of the two games. We assume here the reader is familiar with the content of the sections about reversible and irreversible backtracking.

Backtracking games for LCM and constructive implication. The backtracking game for t.A (or f.B) and LCM and constructive implication 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 new kinds of moves: intuitionstic and LCM 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. If either i is the index of any negative judgement, or i is the index of the last positive judgement, then the retracted nodes can be recovered (intuitionistic backtracking), otherwise they cannot (irreversible backtracking). 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.

Created by Mathematica  (November 11, 2006)