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...

enter image description here

| improve this answer | |
  • 1
    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:

enter image description here

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/

| improve this answer | |

Not the answer you're looking for? Browse other questions tagged or ask your own question.