 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2016/digital-systems-linear-algebra-introduction-to-formal-proof/7/c/solution

\frac{Γ , \neg ϕ ⊢ ⊥}{Γ ⊢ ϕ} RAA,

discharging the assumption

\neg ϕ

. This is the classical rule that concludes

ϕ

directly, as opposed to the negation introduction rule, which concludes a negation.

1  ¬¬φ   premise
2  | ¬φ  assumption
3  | ⊥   ¬-elim 2,1
4  φ     RAA 2–3

Here line 1 is the negation of line 2. Thus only negation elimination rule inside the subproof, followed by RAA, is needed.

 New to topics? Read the docs here!