Intuitionistic Logic: if a satisfies ∀y.P(a,y), then a satisfies P(a,b)∧P(a,c).
(∃x.∀y.P(x,y)⇒∃x.(P(x,b)∧P(x,c)))

This example is similar to the previous one. Abelard moves t.∃x.∀y.P(x,y)⊃∃x.(P(x,b)∧P(x,c)), and Eloise replies f.∃x.∀y.P(x,y). In this initial part of the game, the goal of Eloise is not to win, but only to study how Abelard defends ∃x.∀y.P(x,y). Abelard has to move f.∀y.P(a,y) for some a, and defend ∀y. P(a,y). Thanks to backtracking, Eloise can attack f.∀y.P(a,y) twice in a row, first moving f.P(a,b), then moving f.P(a,c). The goal of Eloise, for the moment, is not win, but to check if, as Abelard claims, both P(a,b) and P(a,c) are true. If this is not the case, Abelard loses. If this is, indeed, the case, then Eloise knows that x=a is the correct move to defend t.∃x.(P(x,b)∧P(x,c). Therefore Eloise backtracks to t.∃x.∀y.P(x,y)⊃∃x.(P(x,b)∧P(x,c)). This time, she moves t.∃x.(P(x,b)∧P(x,c)), then t.P(a,b)∧P(a,c). Eventually, Eloise wins, because both P(a,b) and P(a,c) are true.

In[373]:=

In[374]:=

Out[375]=

Dotted positions (reminder). We mark with a big dot any position to which Eloise can backtrack to: all negative judgements of the tree, and the last positive judgement of the tree.

In[376]:=

Created by Mathematica  (November 11, 2006)