Keep the two existential elimination scopes nested. Let witness the outer existential and the inner one, both fresh. Inside them, negation introduction proves the required counterexample to without invoking an unproved contraposition lemma.The result at lines 12–14 has no free occurrence of either fresh witness. At the inner discharge, is absent from the remaining assumptions; at the outer discharge, is absent from the premise and final conclusion. Hence the eigenvariable conditions hold at both eliminations.
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] Articles by others on the same topic
There are currently no matching articles.