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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .