Intuitionistic Logic: double negation for a simply universal formula.
(¬¬∀x.P(x)⇒∀x.P(x))

Usually, the Classical law of double negation: ¬¬A⇒A is not intutionistically derivable, because it is equivalent to Excluded Middle. We can intuitionistically derive ¬¬A⇒A, though, when A = ¬¬∀x.P(x) and P is decidable. Here is the proof. Assume ¬¬∀x.P(x), and fix any x, in order to prove P(x). Either P(x) is true or ¬P(x) is true, because P is recursive and we can compute its truth value. If P(x) is true, we are done. If ¬P(x) is true, then ¬∀x. P(x), because if we assume ∀x.P(x) we derive P(x), contradicting ¬P(x). From ¬∀x. P(x) and our assumption ¬¬∀x.P(x) we conclude F, as wished.

Here is a recursive winning strategy for Eloise. Abelard moves t.¬¬∀x.P(x)⊃∀x.P(x) from t.¬¬∀x.P(x)⇒∀x.P(x). Eloise replies f.¬¬∀x.P(x).  Eloise moves from f.¬¬∀x.P(x), because a negation is considered as a conjunction, and when a negation has an "f." in front, is considered as a disjunction. In particular Eloise can backtrack from f.¬¬∀x.P(x) to t.¬¬∀x.P(x)⇒∀x.P(x). This time, Eloise moves  t.∀x.P(x), and Abelard replies  t.P(a) for some a, claiming that P(a) is false. If P(a) is true then Abelard loses. Assume P(a) is false. Then Abelard temporarily wins. Then Eloise backtracks to f.¬¬∀x.P(x), then she moves t.¬∀x.P(x). Abelard replies f.∀x.P(x). Eloise moves f.P(a), claiming that P(a) is false. Eloise wins, because P(a) is, indeed, false.

In[390]:=

In[391]:=

Out[392]=

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.

We choose the parameter of the game.

In[393]:=

In this game, it is essential for Eloise the fact that negation are taken conjunctive. Assume instead all negations are taken disjunctive. Then Abelard can win, as follows. Abelard moves t.¬¬∀x.P(x)⊃∀x.P(x) from t.¬¬∀x.P(x)⇒∀x.P(x). Either Eloise moves f.¬¬∀x.P(x), and Abelard replies t.¬∀x.P(x), or Eloise moves t.∀x.P(x). In both cases, the last positive judgement is no more t.¬¬∀x.P(x)⊃∀x.P(x), but it is t.¬∀x.P(x) in the first case, and t.∀x.P(x) in the second case. Therefore Eloise cannot backtrack to t.¬¬∀x.P(x)⊃∀x.P(x) any more, and her move from t.¬¬∀x.P(x)⊃∀x.P(x) should be the best one on the first try. Eloise should move f.¬¬∀x.P(x) if ∀x.P(x) is false, and should move t.∀x.P(x) if ∀x.P(x) is true. Eloise has to decide whether ∀x.P(x) is true or not, and this cannot be done uniformly on P.

Created by Mathematica  (November 11, 2006)