This is not homework. I do it for fun and learning.

I use the Logic Book.

Problem has to be done in SD+.

How to prove the following argument :

|- [~A =>(~B=>C)]=>[(A v B) v (~~B v C )]

I started by assuming the antecedent and using ND to the best of my ability to get the conclusion. But I only land up getting A vB or (~~B v C) which is ~B=>C (impl) but not both

Maybe in order to get B deriving a contradiction would help, since if I assume ~A =>~B

In effect, I was able to derive one of the consequents,but not the other

I tried working backwards and still got stuck

I request help or hints on how to resolve this dilemma

  • 1
    Not clear... Have you derived A v B or (~~B v C) ? Is this not the consequent? Mar 29, 2021 at 14:47
  • 1
    Assume ~A and ~B and the negation of the conclusion and derive three contradictions. Mar 29, 2021 at 15:02
  • I was able to derive one but could not get the other somehow.l got Av B easily enough. I edited my inquiry.
    – Eudoxus
    Mar 29, 2021 at 15:20
  • From ~A=>(~B=>C) then (~A & ~B)=>C exp.
    – Eudoxus
    Mar 29, 2021 at 15:24

3 Answers 3


I started by assuming the antecedent and using ND to the best of my ability to get the conclusion.

Pro Tip: Whenever you cannot see how get the conclusion, then attempt to show you cannot get its negation.

IE: Sometimes Reduction to Absurdity maybe the way to go. Indeed, it is, here.

|  |_ ~A => (~B => C)
|  |  |_ ~((A v B) v (~~B v C))
|  |  |  |_ ~B
|  |  |  |  :
|  |  |  |  :
|  |  |  |  #
|  |  |  ~~B
|  |  |  ~~B v C
|  |  |  (A v B) v (~~B v C)
|  |  |  #
|  |  ~~((A v B) v (~~B v C))
|  |  (A v B) v (~~B v C)
|  (~A => (~B = C)) => ((A v B) v (~~B v C))
  • Thanks ,but I solved by Fizz’s tip. Though your Pro Tip will solve the last one,l hope
    – Eudoxus
    Mar 30, 2021 at 21:37
  • Who downvoted me? Can l be upvoted.
    – Eudoxus
    Apr 3, 2021 at 1:24

Hint: Let X := ~A =>(~B=>C) is by un-currying (~A & ~B) => C. And further by "spelling out the def of =>" and De Morgan and double-negation elimination:

~(~A & ~B) v C = (A v B) v C.

Whereas Y := (A v B) v (~~B v C ) is really A v B v C by associativity of v and double-negation elimination (and B v B = B). So it's even the case that X <=> Y.

  • Actually l got to (Av B)v C . I didn’t know about Y . Thanks
    – Eudoxus
    Mar 29, 2021 at 18:08
  • @Eudoxus: if your (SD+) system doesn't allow you use associativity, it's possible to prove it as a derived rule, but that's pretty painful in a Fitch-style system. i.stack.imgur.com/pG8VN.png (+ which means "or" there, associate on the left in the default notation in that prover.) Mar 30, 2021 at 21:07
  • It does allow me to use it@Fizz
    – Eudoxus
    Apr 3, 2021 at 1:00
  • Prover is pretty cool but figuring out which rule for each statement is kind of tricky
    – Eudoxus
    Apr 3, 2021 at 1:23
  • @Eudoxus: click "annotate proof" for that... and you need to allow browser pop-ups from that site. It's kinda annoying that's not the default (and in the main proof window). The image I linked to in my last comment has rule-use annotations. Apr 3, 2021 at 9:31

If you look at it for a minute, it's just converting conditionals (P => Q) to disjunctions (~P V Q) through material implication. There are some negations to be dealt with, but you just treat ~A (for example) as a unit and apply the same rules, and then apply double negation introduction or double negation elimination as needed. So I think the simplest derivation strategy here is to assume the antecedent and then derive the consequent from that assumption through the aforementioned transformations.

You must log in to answer this question.

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