A tree-like picture of a generic position of the play.
A picture of Tarski Games in tree form. We draw one node for the current position (i.e., judgement) of the play, and also one node for each previous position (i.e., judgement) of the play. We number nodes 1,...,n, according to the order they have in the play. Moves are represented by edges, having the color of the player who did the move.
An example. Consider the Tarski game t.(A∧B)∨((A∧¬B)∨(¬A∧B)), assuming: A,B atomic, and A true, and B false. Consider the following play of 6 positions, or 6 ``nodes''.
In node 1, the judgement t.(A∧B)∨((A∧¬B)∨(¬A∧B)) itself, Eloise chooses to defend the subjudgement t.(A∧¬B)∨(¬A∧B) in right-hand side of the formula.
In node 2, Eloise chooses to defend the subjudgement t.A∧¬B in the left-hand side.
In node 3, Abelard choose to attack the subjudgement t.¬B in right-hand side.
In node 4, Eloise chooses to defend the only subjudgement f.B of a negation t.¬B.
In node 5, Abelard chooses to attack the only subjudgement f.F of f.B (remember that B is assumed false).
The node 6, f.F, is the current position of the play. Abelard should move from f.F (``False is false'', a judgement which is trivially true). Abelard cannot move, he give up and loses.
This is a picture of the play.
Created by Mathematica (October 17, 2006)