Intuitionistic Logic: propositional logic.
(F⇒A), (A⇒T), (A⇒A).

We start considering examples taken from propositional logic: (F⇒A) (False implies anything), (A⇒T) (anything implies true), (A⇒A) (anything implies itself). For simplicity, we assume that A is atomic. All these formulas can be proved intuitionistically, that is, without using Excluded Middle in any form. Recursive winning strategies for Eloise are immediate:
- In t.F⇒A, Abelard moves t.F⊃A, and Eloise replies f.F, claiming that F is false. This is indeed the case and Eloise wins.
- In t.A⇒T, Abelard moves t.A⊃T, and Eloise replies t.T, claiming that T is false. This is indeed the case and Eloise wins.
- In t.A⇒A, Abelard moves t.A⊃A, and Eloise replies f.A, claiming that A is false. If this is indeed the case, then Eloise wins. If A is true, then Eloise backtracks to t.A⊃A, and she moves t.A this time, claiming that A is true. This is indeed the case and Eloise wins.

In[356]:=

In[359]:=

Out[359]=

Out[360]=

Out[361]=

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 games.

In[362]:=

In[364]:=

In[366]:=

Created by Mathematica  (November 11, 2006)