How to prove this: ¬C → B , C → ¬B ⊢ ¬B ↔ C in TFL with natural deduction?

Question

I'm really stuck on how to prove ¬C → B , C → ¬B ⊢ ¬B ↔ C. I know I have $C \implies \sim B$ but in order to introduce the biconditional I have to prove $\sim B \implies C$ and I have no idea how. Any help is greatly appreciated. So far this is what I have:

1. $\quad \sim C \implies B :PR$

2. $\quad C \implies \sim B :PR$

3. $\quad \sim B :AS$

4. $\quad ?????$

5. $\quad \sim B \implies C :\implies I\;(???)$

6. $\quad \sim B \iff C : \iff I2,5$

Answer 1

Heres one potential way to do it,

$$\begin{align} \neg C \to B , C \to \neg B, C &\vdash C &&\text{($\in$)}\\ \neg C \to B , C \to \neg B, C &\vdash C \to \neg B &&\text{($\in$)}\\ \neg C \to B , C \to \neg B, C &\vdash \neg B &&\text{($\to -$), (1), (2)}\\ \neg C \to B , C \to \neg B, \neg B, \neg C &\vdash \neg B &&\text{($\in$)}\\ \neg C \to B , C \to \neg B, \neg B, \neg C &\vdash \neg C &&\text{($\in$)}\\ \neg C \to B , C \to \neg B, \neg B, \neg C &\vdash \neg C \to B &&\text{($\in$)}\\ \neg C \to B , C \to \neg B, \neg B, \neg C &\vdash B &&\text{($\to -$), (5), (6)}\\ \neg C \to B , C \to \neg B, \neg B &\vdash C &&\text{($\neg -$), (4), (7)}\\ \neg C \to B , C \to \neg B &\vdash \neg B \leftrightarrow C &&\text{($\leftrightarrow +$), (3), (8)} \end{align}$$

Answer 2

Using TFL's fundamental rules, here's a derivation for $C\to\neg B\vdash_{\tiny\!\! TFL} B\to\neg C$ : $$\def\fitch#1#2{~~~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~C\to\neg B}{\fitch{~~2.~B}{\fitch{~~3.~C}{~~4.~\neg B\qquad{\to}E~1,3\\~~5.~\bot~~\qquad\neg E~4,2}\\~~6.~\neg C\qquad\neg I~3{-}5}\\~~7.~B\to\neg C\qquad{\to}I ~2{-}6}$$

The derivation you want is similar.

$$\fitch{~~1.~\neg C\to B}{\fitch{~~2.~\neg B}{~~~~\vdots\\~~7.~C}\\~~8.~\neg B\to C\qquad{\to}I ~2{-}7}$$