 Solution

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

\frac{Γ , \neg A ⊢ ⊥}{Γ ⊢ A} RAA .

Given the subproof under

\neg A

Γ ⊢ \neg\neg A

A

. This justification uses the stated classical rules; unrestricted RAA would not follow from intuitionistic rules alone.

 New to topics? Read the docs here!