# Fitch style proof of $(\neg B \to \neg A) \leftrightarrow (A \to B)$

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

• This is the second question in propositional calculus which you tagged as first order logic. Please be aware of the difference. – 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.

• I am sorry but I am not quite sure what u mean. Can u please explain? Thank you – user3727903 Jun 11 '14 at 0:01
• @user3727903 Don't apologize. See the edit. – Git Gud Jun 11 '14 at 0:19
• 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 – user3727903 Jun 11 '14 at 0:28
• @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. – Git Gud Jun 11 '14 at 0:31
• @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. – Git Gud Jun 11 '14 at 0:37

Premises:

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

Logical consequence: (A ↔ C)??