LCM: Markov Principle.
(¬¬∃x.P(x)⇒∃x.P(x))

In[402]:=

In[403]:=

In[404]:=

Out[404]=

Thin and thick edges in Eloise's view-tree (a reminder). Whenever we backtrack from position i to position j<i, we retract all positions j+1, ..., i. We mark this fact by drawing the edges leading to the positions j+1, ..., i thinner. If the position j was retracted, and now we recover it, the whole play comes back to the state it was in position j. We mark this fact by drawing the edges leading to positions 1, ..., j either thin or thick, according if they were thin or thick in the view-tree for position j. A single move can change the look of the view-tree deeply, because we can recover an older state of the tree.

Dotted positions (reminder). We mark with a big dot any position to which Eloise can backtrack to using intuitionistic backtracking: all negative judgements of the tree, and the last positive judgement, in the part of the tree having thick edges.

We choose the parameters of the game.

In[405]:=

Created by Mathematica  (November 11, 2006)