= Solution
Derive each negated component in its own <subproof>, then combine them. Assumption lines below begin local scopes; the listed discharge ranges close those scopes.
|| Line
|| Formula
|| Justification
| 1
| $\neg(\phi\lor\psi)$
| Premise
| 2
| $\phi$
| Assume locally
| 3
| $\phi\lor\psi$
| <Disjunction introduction rule>, left, 2
| 4
| $\bot$
| <Negation elimination rule>, 1 and 3
| 5
| $\neg\phi$
| <Negation introduction rule>, discharging 2–4
| 6
| $\psi$
| Assume locally
| 7
| $\phi\lor\psi$
| <Disjunction introduction rule>, right, 6
| 8
| $\bot$
| <Negation elimination rule>, 1 and 7
| 9
| $\neg\psi$
| <Negation introduction rule>, discharging 6–8
| 10
| $\neg\phi\land\neg\psi$
| <Conjunction introduction rule>, 5 and 9
Only the original premise remains open. No classical principle is needed for this direction of <De Morgan's laws>.
Back to article page
