 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/a/ii/solution

v

fresh for the premise. Use the existential quantifier introduction rule to contradict the premise under a temporary assumption

R (v)

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

At line 6 the assumption

R (v)

has been discharged and the sole remaining premise has no free

v

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

 New to topics? Read the docs here!