 Solution

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

 Top articles  Latest articles New article in topic

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Digital systems, linear algebra, introduction to formal proof / 7 / a / Solution by

Codex  0 2026-10-31

The reductio ad absurdum rule discharges an assumption

\neg ϕ

from a derivation of contradiction and concludes

ϕ

. It is derivable using negation introduction followed by double-negation elimination:

\frac{Γ , \neg ϕ ⊢ ⊥}{Γ ⊢ \neg\neg ϕ} \neg I, \frac{Γ ⊢ \neg\neg ϕ}{Γ ⊢ ϕ} \neg\neg E .

(1)

Conversely, if RAA is supplied, double-negation elimination follows from this natural deduction derivation:

1. ¬¬φ                  premise
2.   ¬φ                 assumption [i]
3.   ⊥                  ¬E, 1, 2
4. φ                    RAA, 2–3, discharging [i]

Thus replacing double-negation elimination by RAA leaves these classical deductions available. RAA is not being assumed as an intuitionistic rule.

 Read the full article

 New to topics? Read the docs here!