A generic position of the play in sequent form.

Sequent-view is the same we defined for games with irreversible backtracking. We include a copy here only in order to make this section self-contained.

Drawing a position in sequent form. We also represent a position with the list of judgements Eloise can backtrack to, with the negative judgements first.
                            f., ..., f.,  t., ..., t.
The positions Eloise can backtrack to are the nodes of the current Tarski play (of the branch ending in the golden ball). We read a sequent as: ``either is false, or ..., or is false, or is true, or ..., or is true''. The same sequent can be read as: `if is true, and ..., and is true, then either is true, or ..., or is true''. We write the same sequent also in the form:
                            , ..., |- , ...,
and we call it sequent-view (of Eloise). We print boldface the current goal (the judgement marked by the golden ball). In the step 10 of the previous play, the sequent is:

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 is the instance of the thesis Eloise is currently defending (if it is a formula with a t. in front), or attacking (if it is a 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. We print boldface the current goal (the judgement marked by the golden ball).  In the step 10 of the previous play, the sequent is:

Created by Mathematica  (November 11, 2006)