 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2015/digital-systems-linear-algebra-introduction-to-formal-proof-resit/8/a/i/solution

Apply the negation introduction rule to an assumed existential statement and the existential quantifier elimination rule with a fresh witness

u

1234567 \forall x \neg P (x) [\exists x P (x)]^{a} [P (u)]^{b} \neg P (u) ⊥ ⊥ \neg\exists x P (x) premise assumption fresh witness assumption \forall E 1 \neg E 3, 4 \exists E 2, (3 - 5) \neg I (2 - 6) .

u

is absent from the surrounding premise, the existential assumption and the exported conclusion

⊥

. Its local assumption is discharged before the final negation introduction rule.

\forall x \neg P (x) ⊢ \neg\exists x P (x) .

 New to topics? Read the docs here!