= Solution
Assume the <logical conjunction> temporarily, then eliminate the premise's <logical disjunction> by cases. A <natural deduction> proof, with each indented assumption delimiting its own subproof, is:
``
1. not P or not Q premise
2. | P and Q temporary assumption
3. | P and-elim-L, 2
4. | Q and-elim-R, 2
5. | | not P first disjunction case
6. | | false not-elim, 3,5
7. | | not Q second disjunction case
8. | | false not-elim, 4,7
9. | false or-elim, 1, cases 5-6 and 7-8
10. not (P and Q) not-intro, discharge 2-9
``
Lines 5–6 and 7–8 are separate sibling subproofs, not one nested inside the other. Both derive the same contradiction under the common assumption on line 2. <Logical disjunction> elimination discharges the two case assumptions, and <negation> introduction then discharges the <logical conjunction> assumption. The sole undischarged premise is the required one. This proof uses only the supplied <logical conjunction>, <logical disjunction> and <negation> rules; no converse form of <De Morgan's laws> is being assumed as an extra rule.
Back to article page
