LCM: Weak Koenig's Lemma.
(∀x.∀y.(P(x)∨Q(y))⇒(∀x.P(x)∨∀y.Q(y)))

In[407]:=

We define the classical principle Weak Koenig's Lemma for recursive Lemma. We state it in the form: "if a recursive binary tree is infinite, then either the left or the right-hand side of the tree are infinite". Modulo choice axiom, this says that if a recursive binary tree is infinite, then it has an infinite branch. We get the branch by taking, at each step, left or right according to which side is infinite.

In[408]:=

In[409]:=

Out[409]=

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[410]:=

Created by Mathematica  (November 11, 2006)