The following natural deduction tables record the active assumption lines explicitly. A rule may use an earlier line only while all of that line's assumptions remain available; assumption discharge closes the indicated case or hypothesis. The first proof makes the case split first, constructs the whole required logical conjunction in each case, and then closes the cases.
Table 1.
First proof: one case split constructs both conjuncts
.
LineOpen assumptionsFormulaJustification
11Premise
21, 2Temporary assumption
31, 2disjunction introduction L 2
41, 2disjunction introduction L 2
51, 2conjunction introduction 3, 4
61, 6Temporary assumption
71, 6conjunction elimination L 6
81, 6conjunction elimination R 6
91, 6disjunction introduction R 7
101, 6disjunction introduction R 8
111, 6conjunction introduction 9, 10
121disjunction elimination 1, 2, 5, 6, 11
The second proof instead splits the goal first. It proves each required logical disjunction by a separate use of disjunction elimination, then applies conjunction introduction at the end.
The essential difference is the order of proof construction: the first shares one case split between both goals, whereas the second duplicates that split and combines the results outside the cases. Both use only the stated natural deduction rules, and both conclude
(1)

Ancestors (11)

  1. 7
  2. Digital systems, linear algebra, introduction to formal proof
  3. 2013
  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