= Solution
Keep the two <existential elimination> scopes nested. Let $b$ witness the outer existential and $a$ the inner one, both fresh. Inside them, <negation introduction> proves the required counterexample to $P$ without invoking an unproved contraposition lemma.
``
1. ∀x ∀y (P(x,y) → Q(x,y)) premise
2. ∃y ∃x ¬Q(x,y) assumption [i]
3. ∃x ¬Q(x,b) fresh witness assumption [j]
4. ¬Q(a,b) fresh witness assumption [k]
5. ∀y (P(a,y) → Q(a,y)) ∀E, 1
6. P(a,b) → Q(a,b) ∀E, 5
7. P(a,b) assumption [l]
8. Q(a,b) →E, 6, 7
9. ⊥ ¬E, 4, 8
10. ¬P(a,b) ¬I, 7–9, discharging [l]
11. ∃x ¬P(x,b) ∃I, 10
12. ∃y ∃x ¬P(x,y) ∃I, 11
13. ∃y ∃x ¬P(x,y) ∃E, 3, 4–12, discharging [k]
14. ∃y ∃x ¬P(x,y) ∃E, 2, 3–13, discharging [j]
15. (∃y ∃x ¬Q(x,y)) → (∃y ∃x ¬P(x,y))
→I, 2–14, discharging [i]
``
The result at lines 12–14 has no free occurrence of either fresh witness. At the inner discharge, $a$ is absent from the remaining assumptions; at the outer discharge, $b$ is absent from the premise and final conclusion. Hence the <eigenvariable conditions> hold at both eliminations.
Back to article page
