= Solution
The supplied <double-negation elimination> rule provides the classical step needed to recover each positive component:
|| Line
|| Formula
|| Justification
| 1
| $\neg(\neg\phi\lor\neg\psi)$
| Premise
| 2
| $\neg\phi$
| Assume locally
| 3
| $\neg\phi\lor\neg\psi$
| <Disjunction introduction rule>, left, 2
| 4
| $\bot$
| <Negation elimination rule>, 1 and 3
| 5
| $\neg\neg\phi$
| <Negation introduction rule>, discharging 2–4
| 6
| $\phi$
| <Double-negation elimination>, 5
| 7
| $\neg\psi$
| Assume locally
| 8
| $\neg\phi\lor\neg\psi$
| <Disjunction introduction rule>, right, 7
| 9
| $\bot$
| <Negation elimination rule>, 1 and 8
| 10
| $\neg\neg\psi$
| <Negation introduction rule>, discharging 7–9
| 11
| $\psi$
| <Double-negation elimination>, 10
| 12
| $\phi\land\psi$
| <Conjunction introduction rule>, 6 and 11
Both local negated assumptions have been discharged. The <proof> establishes the positive conjunction without assuming an unproved derived version of <De Morgan's laws>.
Back to article page
