 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/8/b/solution

v

. Within the assumption of the forbidden universal quantification, eliminate the original existential quantification to obtain logical falsity:

1234567 \exists x R (x) ∣ \forall y \neg R (y) ∣ ∣ R (v) ∣ ∣ \neg R (v) ∣ ∣ ⊥ ∣ ⊥ \neg\forall y \neg R (y) premise assumption witness assumption; v fresh \forall -elim 2 \neg -elim 3, 4 \exists -elim 1, 3 - 5 \neg -intro 2 - 6

The witness

v

appears neither in the exported conclusion

⊥

at line 6 nor in the other undischarged assumptions. The existential quantifier elimination rule is therefore valid, and

\exists x R (x) ⊢ \neg\forall y \neg R (y) .

 New to topics? Read the docs here!