1

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

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

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))
2
  • Thanks ,but I solved by Fizz’s tip. Though your Pro Tip will solve the last one,l hope – Eudoxus Mar 30 at 21:37
  • Who downvoted me? Can l be upvoted. – Eudoxus Apr 3 at 1:24
1

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.

5
  • Actually l got to (Av B)v C . I didn’t know about Y . Thanks – Eudoxus Mar 29 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 at 21:07
  • It does allow me to use it@Fizz – Eudoxus Apr 3 at 1:00
  • Prover is pretty cool but figuring out which rule for each statement is kind of tricky – Eudoxus Apr 3 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 at 9:31

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.