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

Table of contents
- Solution c

Solution

Proof by contradiction, or reductio ad absurdum, has the form

\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.

To derive double-negation elimination using RAA without assuming double-negation elimination itself, use

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.

 Ancestors (11)

 View article source

 Discussion (0) New discussion

There are no discussions about this article yet.

 Articles by others on the same topic (0)

There are currently no matching articles.

  See all articles in the same topic Create my own version