I am working on a problem for an online class that I'm struggling to figure out.

I'm given these premises: 1. (H > (A > B)) (The > sign here represents conditional) 2. (~K & ~B) 3. (~A > K)

The desired conclusion is ~H.

My hunch tells me I need to use negation introduction on premises 2 and 3 to derive ~~A and ~~B, from which point I can use negation elimination to derive A and B. Does anyone have an idea of how to approach this?

Edit: Here is what I have so far. My work as of 6:05PM, 6/18.

  • 1
    Are you sure this is correct? ~K in 2 contradicts K in 3.
    – MarkOxford
    Jun 18, 2018 at 22:09
  • My bad. It's actually 3. (~A > K). Sorry! I'm going to revisit this now myself, but help would still be appreciated.
    – ephemeron
    Jun 18, 2018 at 22:44

4 Answers 4


Using the natural deduction proof checker associated with the forall x: Calgary Remix, I get the following:

enter image description here

  • Thanks for your answer! Can you explain to me what MT and DNE mean?
    – ephemeron
    Jun 18, 2018 at 23:10
  • MT means Modus Tollens and DNE means Double Negative Elimination. @ephemeron Jun 18, 2018 at 23:13
  • 2
    I worked it out and this works well - we don't use MT in this class but I figured out how to get there already with our own methods. I didn't think to use H as an assumption, which was the key here. Thank you for your help!
    – ephemeron
    Jun 18, 2018 at 23:38

The desired conclusion is ~H.

  1. H thus (A thus B). Premise.

  2. If (A thus B) is false, then not-H is true, by modus tollens. So proving not-H is our goal. Do the premises show that (A thus B) is false?

  3. (A thus B) means (not-A or B). Equivalence.

  4. The denial of (not-A or B) is (not-(not-A or B)).

  5. (not-(not-A or B)) means (A and not-B). Equivalence. Thus (A and not-B) is what we must show to be true. Proof of this relation will negate H.

  6. Not-K and not-B. Premise

  7. Not-B. Simplification.

  8. Not-K. Simplification

  9. Not-A thus K. Premise

  10. A is true. By modus tollens, as (not-A thus K) is the premise, but not-K is true.

  11. (A and not-B). Adjunction. Thus the negation of (A thus B) has been shown.

  12. Not-H is true. By modus tollens


From 2 we have ~K.

(~K & ~B) > ~K

Putting it to 3 we have A.

((~A > K) & K) > A

Now let's assume A > B. From 2 we have ~B. Therefore, if A > B then ~A.

((A > B) & ~B) > ~A

For simplicity, let us use new variable C to denote A > B.

C = (A > B)

Thus, C is false and we conclude ~H.

((H > C) & ~C) > ~H

  • What do you mean by "putting it into 3"? Also, I updated the question since it had a typo - hopefully you caught that. Also, can you explain your 4th line a little more? I think I got to that point on my own, but I don't know how you can conclude ~H from it.
    – ephemeron
    Jun 18, 2018 at 23:01
  • "Putting it into 3" means conjunction, as you can see from next string. Yes, I saw you updated the question, otherwise I would not answer since it led to 0 answer instead of ~H.
    – rus9384
    Jun 18, 2018 at 23:10

The original post mostly had the right idea. Negation Elimination subproofs are required, we just need to nest them. Assume H and then assume A, aiming to derive contraditions to eliminate the assumptions.

  1|  H > (A > B)         Promise
  2|  ~K & ~B             Promise
  3|_ ~A > K              Promise
  4|  |_ H                Assumed
  5|  |  A > B            > Elimination 4,1
  6|  |  |_ A             Assumed
  7|  |  |  B             > Elimination 6,5
  8|  |  |  ~B            & Elimination 2
  9|  |  ~A               ~ Introduction 5,7,8
 10|  |  K                > Elimination 9,3
 11|  |  ~K               & Elimination 2
 12|  ~H                  ~ Introduction 4,10,11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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