14. Classical De Morgan

MediumProofAcademy Pass20 points

Prove ¬(P ∧ Q) → ¬P ∨ ¬Q. Unlike the other De Morgan laws, this direction cannot be proven constructively: you have to decide whether P holds.

The standard axioms of classical logic are accepted by the judge.

Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.

Solution.lean

1theorem solution (P Q : Prop) : ¬(P ∧ Q) → ¬P ∨ ¬Q := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

P Q:Prop

⊢¬(P ∧ Q) → ¬P ∨ ¬Q

ReadyLn 1, Col 1Lean 4

Draft saved in this browser