# 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

## marked as duplicate by Mauro ALLEGRANZA logic StackExchange.ready(function() { if (StackExchange.options.isMobile) return; \$('.dupe-hammer-message-hover:not(.hover-bound)').each(function() { var \$hover = \$(this).addClass('hover-bound'), \$msg = \$hover.siblings('.dupe-hammer-message'); \$hover.hover( function() { \$hover.showInfoMessage('', { messageElement: \$msg.clone().show(), transient: false, position: { my: 'bottom left', at: 'top center', offsetTop: -7 }, dismissable: false, relativeToBody: true }); }, function() { StackExchange.helpers.removeMessages(); } ); }); }); May 8 at 15:32

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 – another_name May 8 at 15:27
• Yes, this seems to work. – Frank Hubeny May 8 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/