The question asked for a formal proof, by natural deduction, of:
⊢N ( A ∧ B ) ↔ ¬( A → ¬B)
I can use the rules of system N and the rule 'repetitive inward' (RI)
I started backwards by establishing that I have to prove
Box 1: ( A ∧ B ) ⊢ ¬( A → ¬B) and
Box 2: ¬( A → ¬B) ⊢ ( A ∧ B ) so that I can apply the (↔ I) rule.
Box 1:
A --- Assumption
B --- Assumption
A ∧ B -- ( ∧I)
Is this correct?
Also, can someone help me in proving box 2 by natural deduction? I have no idea where to start.
Indeed.
$$\def\fitch#1#2{\quad\begin{array}{|l|}\hline #1\\\hline#2\\\hline \end{array}} \fitch{}{\fitch{A\wedge B}{~~\vdots\\\neg (A\to\neg B)}\\\fitch{\neg(A\to\neg B)}{~~\vdots\\A\wedge B}\\(A\wedge B)\leftrightarrow\neg(A\to\neg B)}$$
No. You have assumed $A\wedge B$. From this you may derive $A$ and $B$ using the $\wedge$ elimination rules. Then you seek to derive from that $\neg(A\to\neg B)$. For that use the $\neg$ Introduction rule, which requires assuming $A\to\neg B$.
Oh, but look, you may derive $A$ from $A\wedge B$, and assumed $A\to\neg B$, so now you may use the $\to$ elimination rule to derive $\neg B$. And you may also derive $B$ from $A\wedge B$ too.
I'll through a tip for the second box in too. You are going to want to introduce that $\wedge$. To derive the $A$ and $B$ use the $\neg$ elimination rule (so assume their negations, aiming to derive contraditions).
But what are you going to contradict in each box?
$$\fitch{}{\fitch{A\wedge B}{\fitch{A\to\neg B}{A\hspace{16ex}\wedge\mathsf E\\\neg B\hspace{14ex}\to\mathsf E\\B\hspace{16ex}\wedge\mathsf E}\\\neg (A\to\neg B)\hspace{10ex}\neg~\mathsf I}\\\fitch{\neg(A\to\neg B)}{\fitch{\neg A}{\vdots}\\A\\\fitch{\neg B}{\vdots}\\B\\A\wedge B}\\(A\wedge B)\leftrightarrow\neg(A\to\neg B)\hspace{2ex}\leftrightarrow\mathsf I}$$