A generic position of the play in tree form.

Drawing a position in tree form. For each position we draw the current node and all previous nodes, numbered as they are in the play. The usual moves of Tarski plays are denoted by edges. The positions Eloise can backtrack to are dotted by a big dot. The positions Eloise cannot backtrack to (all positive judgements, but the last one) are dotted with a small dot. Each node and each move has the color of the player it belongs to. All edges are thick. The golden ball marks the current position of the play. We call this picture, including all backtracking by Eloise: Eloise's view-tree. The background of the picture is a pale pink, Eloise's color. Here is Eloise's view-tree at step 14 of the play of the previous subsection.

With respect to a Tarski play, a BCK-play is a tree, not a single branch. A forking in the tree correspond to a move changed by Eloise. Non-retracted moves form a Tarski play we call the current Tarski play. The current Tarski play is the only part of the play which matters to Abelard, who cannot backtrack to any previous node. We call the tree form of the current Tarski play Abelard's view-tree. This is a picture of it, at step 14 of the same play. The background is a pale blue, Abelard's color.

View-trees for Eloise and Abelard are asymmetric. The reason is that the notion itself of backtracking game is asymmetric, biased in favor of Eloise.

Created by Mathematica  (November 11, 2006)