I have been stuck on this proof for a while. Here's where I'm at:

Goal $(\neg B \to \neg A) \leftrightarrow (A \to B)$

l 1. $A \to B$

ll 2. $\neg B$

lll 3. $A$

lll 4. $B$ Elim 1,3

lll 5. $\neg B$ Reit

ll 6. $A \to \neg B$ Into 3-5

ll 7. $\neg A$ ????

l $\neg B \to \neg A$ Into 2-7

If someone can help it will be great. Thank you

  • $\begingroup$ This is the second question in propositional calculus which you tagged as first order logic. Please be aware of the difference. $\endgroup$ – Git Gud Jun 10 '14 at 23:33

I don't get where you're going from step 6, but note the following.

In 4. you got $B$ and in the same subproof you got $\neg B$. You can infer a contradiction and proceed with $\neg$-$\text{Intro}$.

The other subproof should be similar.

Edit: See what I mean below.

enter image description here

  • $\begingroup$ I am sorry but I am not quite sure what u mean. Can u please explain? Thank you $\endgroup$ – user3727903 Jun 11 '14 at 0:01
  • $\begingroup$ @user3727903 Don't apologize. See the edit. $\endgroup$ – Git Gud Jun 11 '14 at 0:19
  • $\begingroup$ lol that was so helpful. thank you but any suggestions on connecting both sentences or that's how I would end the proof? I am still new at this. thanks again $\endgroup$ – user3727903 Jun 11 '14 at 0:28
  • $\begingroup$ @user3727903 From where I left off you should start a new subproof with premise $\neg B\to \neg A$ and infer $A\to B$. When you have both subproofs, you can use $\leftrightarrow$-$\text{Intro}$ on them to conclude. $\endgroup$ – Git Gud Jun 11 '14 at 0:31
  • 1
    $\begingroup$ @user3727903 In case it wasn't clear, the new subproof I mention should be at the same level as the one I did, not inside it. $\endgroup$ – Git Gud Jun 11 '14 at 0:37


  1. A ∨ B
  2. C → ¬B
  3. ¬C → ¬A
  4. ¬B

Logical consequence: (A ↔ C)??


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.