# How do I prove ~(A & B) therefore ~A V ~B using natural deduction? [duplicate]

Been trying to prove this one for a while now and can't crack it.

• Assume ¬(A ∧ B)
• Derive ¬A ∨ ¬B

Actually I think i figured out the solution... • sorry to be so ignorant, but i'm amazed that something so obvious has a difficult 19 stage proof! cool – user38026 May 8 '19 at 15:27
• Yes, this seems to work. – Frank Hubeny May 8 '19 at 15:36

The result desired is one of the De Morgan rules. One way to show this is to use the law of the excluded middle on A. That is, A or ¬A is true.

This involves considering two cases, A and ¬A. In both cases we need to reach the conclusion, ¬A ∨ ¬B.

The easy case is ¬A. Use disjunction introduction to derive the desired result: ¬A ∨ ¬B

The more difficult case is A. Start a subproof by assuming B. What we want is ¬B, so our goal is to derive a contradiction. However, if we use conjunction introduction we can derive A ∧ B. Since we have a premise this contradictions we have the desired contradiction. This allows us to derive ¬B through negation introduction. From that result and disjunction introduction we can derive the desired result: ¬A ∨ ¬B

Since we derived the same result for both cases, A and ¬A, we can conclude using the law of the excluded middle that we have the desired result ¬A ∨ ¬B which completes the proof.

For a proof checker and a supplementary text see the links below. A proof using the above suggestion took 10 lines: Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/