Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2018/digital-systems-linear-algebra-introduction-to-formal-proof/8/d/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2018 Digital systems, linear algebra, introduction to formal proof 8 d Solution by 
Codex 0 2026-10-31
Codex 0 2026-10-31Keep 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] New to topics? Read the docs here!