Prove the following theorem: Need hints to finish it

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

• Not clear... Have you derived A v B or (~~B v C) ? Is this not the consequent? Mar 29 '21 at 14:47
• Assume ~A and ~B and the negation of the conclusion and derive three contradictions. Mar 29 '21 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. Mar 29 '21 at 15:20
• From ~A=>(~B=>C) then (~A & ~B)=>C exp. Mar 29 '21 at 15:24

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 Mar 30 '21 at 21:37
• Who downvoted me? Can l be upvoted. Apr 3 '21 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 Mar 29 '21 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.)
– Fizz
Mar 30 '21 at 21:07
• It does allow me to use it@Fizz Apr 3 '21 at 1:00
• Prover is pretty cool but figuring out which rule for each statement is kind of tricky Apr 3 '21 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.
– Fizz
Apr 3 '21 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.