The supplied double-negation elimination rule provides the classical step needed to recover each positive component:
LineFormulaJustification
1Premise
2Assume locally
3Disjunction introduction rule, left, 2
4Negation elimination rule, 1 and 3
5Negation introduction rule, discharging 2–4
6Double-negation elimination, 5
7Assume locally
8Disjunction introduction rule, right, 7
9Negation elimination rule, 1 and 8
10Negation introduction rule, discharging 7–9
11Double-negation elimination, 10
12Conjunction introduction rule, 6 and 11
Both local negated assumptions have been discharged. The proof establishes the positive conjunction without assuming an unproved derived version of De Morgan's laws.

Ancestors (11)

  1. 7
  2. Digital systems, linear algebra, introduction to formal proof resit
  3. 2019
  4. Past exam of the year 1 of the computer science course of the University of Oxford
  5. Year 1 of the computer science course of the University of Oxford
  6. Computer science course of the University of Oxford
  7. Undergraduate course of the University of Oxford
  8. Course of the University of Oxford
  9. University of Oxford
  10. List of universities
  11. Home

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