 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/iii/solution

Choose

v

fresh. Here double-negation elimination is necessary to turn the negation of a possible counterexample into the positive statement:

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

The remaining context at line 7 contains no free

v

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

 New to topics? Read the docs here!