A generic position of the play in sequent form.

Drawing a position in sequent form. We represent a position with the list of judgements Eloise can backtrack to, with the negative judgements first, and the last positive judgement at the end.
                            f., ..., f.,  t.
The positions Eloise can backtrack to are all negative judgements, and the last positive judgement. We read a sequent as: `if is true, and ..., and is true, then is true''. We write the same sequent also in the form:
                            , ..., |- B
and we call it sequent-view (of Eloise). In the step 14 of the previous play, the sequent is written below (with the current goal printed boldface).  Remark that all positive judgements are skipped, but the last one.

What is the intuitive meaning of the Sequent-view? From a logical viewpoint, , ..., |- , ..., is a complete description of the thesis of Eloise. The current goal (the boldface formula) is the instance of the thesis Eloise is currently defending (if it is B, the only formula with a t. in front), or attacking (if it is some , that is, any formula with a f. in front). If Eloise backtracks, she changes the current goal with some other goal from the same sequent.

The sequent-view is formally defined for Abelard, too, even if Abelard cannot backtrack.  The sequent-view of Abelard is the list of nodes of just the current Tarski play (of the branch ending in the golden ball). The role of f and t are reversed, though. Negative judgements are in the right-hand-side, and positive judgements in the left-hand-side. In the step 14 of the previous play, the sequent is:

Created by Mathematica  (November 11, 2006)