Logic: Proving ~(a ↔ b) and (a ↔ ~b) are equivalent in LPL's Fitch I am working on a proof where I was able to derive this general form: 


  ~(a ↔ b)


From this I would like to obtain:


  a ↔ ~b


I have made sure that the two statements are equivalent by drawing out truth-tables. The problem is that I am not really sure how to go from the first statement to the second statement in Fitch. 

If it helps in answering the question, the specific proof I am working on is LPL's Exercise 8.50. It is the following: 

1.| Cube(b) ↔ (Cube(a) ↔ Cube(c))
2.| | Dodec(b)                            (assumption)
3.| | | Cube(a)↔Cube(c)                   (assumption)
4.| | | Cube(b)                           ↔Elim 1, 3
5.| | | ⊥                                 AnaCon 2, 4
6.| | ~(Cube(a)↔Cube(c))                  ~Intro 3-5
∴ Dodec(b) → (Cube(a) ↔ ¬Cube(c))


Lines 2-6 are my work. I know that this argument is valid because if b was anything besides a cube (a dodec or a tet), then if Cube(a), it would necessarily follow that ~Cube(c) and vice versa, because if Cube(a) implied Cube(c) or vice versa, it would necessitate that b would have to be a cube.
0) $\lnot (a \leftrightarrow b)$ --- premise

1) $a$ --- assumed [a]

2) $b \to a$ --- from 1) by $\to$-intro

3) $b$ --- assumed [b]

4) $a \to b$ --- from 3) by $\to$-intro

5) $a \leftrightarrow b$ --- from 2) and 4)

6) $\bot$ --- from 0) and 5)

7) $\lnot b$ --- from 1) and 6) by $\lnot$-intro, discharging [b]


  8) $a \to \lnot b$ --- from 1) and 7) by $\to$-intro, discharging [a].


9) $\lnot b$ --- assumed [c]

10) $b$ --- assumed [d]

11) $\bot$ --- from 9) and 10)

12) $a$ --- from 11)

13) $b \to a$ --- from 10) and 12) by $\to$-intro, discharging [d]

14) $\lnot a$ --- assumed [e]

15) $a$ --- assumed [f]

16) $\bot$ --- from 14) and 15)

17) $b$ --- from 16)

18) $a \to b$ --- from 15) and 17) by $\to$-intro, discharging [f]

19) $a \leftrightarrow b$ --- from 13) and 18)

20) $\bot$ --- from 0) and 19)

21) $a$ --- from 14) and 20) by Double Negation, discharging [e]


  22) $\lnot b \to a$ --- from 9) and 21) by $\to$-intro, discharging [c]
  
  
    23) $a \leftrightarrow \lnot b$ --- from 8) and 22).
One direction of the equivalence is relatively easy to show: $A ↔ ¬B ∴ ¬(A ↔ B)$. The basic plan is to negate the goal, derive a contradiction which will then allow one to derive the goal.

Here is a proof using a Fitch-style natural deduction proof checker:



To show the other direction is more involved. Again, one can negate the goal, $A ↔ ¬B$, but one should rewrite the goal as a conjunction of disjunctions, $(¬A ∨ ¬B) ∧ (A ∨ B)$, so one can use other inference rules. Once one reaches a contradiction this will give one the rewritten goal from which one can derive the desired biconditional.  

Here is a proof of the other direction, $¬(A ↔ B) ∴ A ↔ ¬B$:



For the proof checker and the associated textbook see the links below.



Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf