= Solution
Assuming $\neg P$ lets the <disjunction introduction rule> produce the <logical disjunction> excluded by the premise. This gives a <contradiction>, so conclude by <negation introduction> and <double-negation elimination>:
|| Line
|| Context
|| Formula
|| Justification
| 1
| $\{1\}$
| $\neg(\neg P\lor\neg Q)$
| Premise
| 2
| $\{1,2\}$
| $\neg P$
| Temporary assumption
| 3
| $\{1,2\}$
| $\neg P\lor\neg Q$
| <disjunction introduction rule> $\lor\text{-intro-L}$ on 2
| 4
| $\{1,2\}$
| $\bot$
| <negation elimination rule> $\neg\text{-elim}$ on 3, 1
| 5
| $\{1\}$
| $\neg\neg P$
| <negation introduction rule> $\neg\text{-intro}$ on 4; discharge 2
| 6
| $\{1\}$
| $P$
| <double-negation elimination> $\neg\neg\text{-elim}$ on 5
Thus
$$
\boxed{\neg(\neg P\lor\neg Q)\vdash P.}
$$
No separate result about $Q$ or use of a derived De Morgan rule is needed.
Back to article page
