Under the premise, assuming either disjunct would introduce the forbidden logical disjunction. Discharging those two assumptions gives the two separate negations, which can then be conjoined.
Table 1.
Derivation of the two negated disjuncts
. | Line | Open assumptions | Formula | Justification |
|---|---|---|---|
| 1 | 1 | Premise | |
| 2 | 1, 2 | Temporary assumption | |
| 3 | 1, 2 | disjunction introduction L 2 | |
| 4 | 1, 2 | negation elimination rule 3, 1 | |
| 5 | 1 | negation introduction 2, 4 | |
| 6 | 1, 6 | Temporary assumption | |
| 7 | 1, 6 | disjunction introduction R 6 | |
| 8 | 1, 6 | negation elimination rule 7, 1 | |
| 9 | 1 | negation introduction 6, 8 | |
| 10 | 1 | conjunction introduction 5, 9 |
ThusThe redundant closing parenthesis printed after the conclusion on p. 8 does not alter the readable propositional formula.[ref]
Temporarily deny the desired logical disjunction. If held, it would introduce that very logical disjunction, producing logical falsity; double-negation elimination therefore gives . The same argument gives , contradicting the premise. The complete natural deduction derivation is:
| Line | Open assumptions | Formula | Justification |
|---|---|---|---|
| 1 | 1 | Premise | |
| 2 | 1, 2 | Temporary assumption | |
| 3 | 1, 2, 3 | Temporary assumption | |
| 4 | 1, 2, 3 | disjunction introduction L 3 | |
| 5 | 1, 2, 3 | negation elimination rule 4, 2 | |
| 6 | 1, 2 | negation introduction 3, 5 | |
| 7 | 1, 2 | double-negation elimination 6 | |
| 8 | 1, 2, 8 | Temporary assumption | |
| 9 | 1, 2, 8 | disjunction introduction R 8 | |
| 10 | 1, 2, 8 | negation elimination rule 9, 2 | |
| 11 | 1, 2 | negation introduction 8, 10 | |
| 12 | 1, 2 | double-negation elimination 11 | |
| 13 | 1, 2 | conjunction introduction 7, 12 | |
| 14 | 1, 2 | negation elimination rule 13, 1 | |
| 15 | 1 | negation introduction 2, 14 | |
| 16 | 1 | double-negation elimination 15 |
ConsequentlyThe uses of double-negation elimination are justified by the supplied rules. This distinguishes the proof from the preceding constructive direction of De Morgan's laws.
Articles by others on the same topic
There are currently no matching articles.