= Solution
Assume the conjunction and obtain a contradiction in each of the two cases supplied by the premise:
|| Line
|| Formula
|| Justification
| 1
| $\neg\phi\lor\neg\psi$
| Premise
| 2
| $\phi\land\psi$
| Assume locally
| 3
| $\phi$
| <Conjunction elimination rule>, left, 2
| 4
| $\psi$
| <Conjunction elimination rule>, right, 2
| 5
| $\neg\phi$
| Assume first case
| 6
| $\bot$
| <Negation elimination rule>, 3 and 5
| 7
| $\neg\psi$
| Assume second case
| 8
| $\bot$
| <Negation elimination rule>, 4 and 7
| 9
| $\bot$
| <Disjunction elimination rule>, 1, 5–6 and 7–8
| 10
| $\neg(\phi\land\psi)$
| <Negation introduction rule>, discharging 2–9
The two case assumptions disappear at line 9, while the conjunction assumption remains available until line 10. The <proof> uses only the primitive rules printed in the paper.
Back to article page
