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 '21 at 14:47
  • 1
    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.
    – Eudoxus
    Mar 29 '21 at 15:20
  • From ~A=>(~B=>C) then (~A & ~B)=>C exp.
    – Eudoxus
    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
    – Eudoxus
    Mar 30 '21 at 21:37
  • Who downvoted me? Can l be upvoted.
    – Eudoxus
    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
    – Eudoxus
    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
    – Eudoxus
    Apr 3 '21 at 1:00
  • Prover is pretty cool but figuring out which rule for each statement is kind of tricky
    – Eudoxus
    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.

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.