Intuitionistic Logic: a prenex operation for ∃.
(∃x.P(x)∧∃y.Q(y))⇒∃x.∃y.(P(x)∧Q(y))

We already considered the same sample in the first section about constructive implication. We include a copy of the discussion here, in order to make this section self-contained.

Let A = ∃x.P(x) ∧ ∃y.Q(y) and B = ∃x'.∃y'.(P(x')∧Q(y')). A⇒B says we can always move ∃ outside ∧. The operational meaning of A⇒B is: there is an effective way of turning any evidence in favor of A into an evidence in favor of B. In this particular case, and evidence in favor of A is some vale x=a such that P(x), and some value y=b such that Q(b). An evidence in favor of B is a pair of values for x', y' such that P(z)∧Q(t). The obvious choice is taking x'=a, y'=b (we chose a trivial example on purpose).

We translate the informal argument above into a recursive winning strategy for Eloise, validating t.A⇒B.
  (move 1) The initial position is t.A⇒B  (a conjunctive judgement).
  (move 2) Abelard moves t.A⊃B.
  (move 3) Eloise moves f.A, attacking the hypothesis A.
  (move 4) Eloise moves f.∃x.P(x), attacking the left-hand side of A. (Normally, in a conjunction, Abelard would attack, but since there is an ``f.'' in front of A, roles are reversed, and Eloise attacks.) Abelard moves next, defending the truth of ∃x.P(x) (again, roles are reversed because there is an ``f.'').
  (move 5) Abelard replies moving some f.P(t), and claiming P(t) is true. Eloise claims P(t) is false (again, roles are reversed because there is an ``f.'').
  (move 6) Suppose P(t) is true. Then Abelard moves f.T and Eloise loses, but only temporarily.
  (move 7) Eloise backtracks to f.A (position 3). She plays f.∃y.Q(y) this time.
  (move 8) Abelard moves from f.∃y.Q(y), defending the truth of ∃y.Q(y) Therefore he replies choosing some f.Q(u), and claiming Q(u) is true.
  (move 9) Suppose it is. Then Abelard moves f.T and Eloise loses. Eloise has lost twice in a row, but this was expected. The primary goal of Eloise on f.A is not to win. If she does, she wins the whole play, but she does not expect to win. The primary goal of Eloise is to obtain from Abelard some arguments in favor of A, that is, some t,u such that P(t), Q(u) are true. This is indeed the case.
  (move 10) Eloise backtracks to t.A⊃B (the last positive judgement, position 2). This time, she moves t.B, a disjunctive judgement.
  (move 11) Eloise moves t.∃y'.(P(t)∧Q(y')).
  (move 12) Eloise moves t.P(t)∧Q(u).
  (move 13) Abelard replies t.P(t). Now Abelard loses, because P(t) is true. Indeed,
  (move 14) Eloise moves t.T, a true conjunctive atom. Abelard drops out (there are no ordinary moves, and Abelard cannot backtrack).
Remark that if Abelard, at step 13, moves t.Q(u), he loses as well, because Q(u) is true.

In[368]:=

In[369]:=

Out[370]=

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

Created by Mathematica  (November 11, 2006)