Proof, is $\lnot p \land \lnot q \vdash p \iff q$? I have derived the proof to some extent, mentioned below:-
$$\begin{array}{rll}
    1. &\lnot p \land \lnot q     &\text{Premise} \\
    2. &\lnot p                   &\land\text{elim},1 \\
    3. &\lnot q                   &\land\text{elim},1 \\
    4. &p                         &\lnot\text{elim},2 \\
    5. &q                         &\lnot\text{elim},3 \\
    6. &p \rightarrow q           &\rightarrow\text{intro},4,5     \\
    7. &q \rightarrow p           &\rightarrow\text{intro},4,5 \\
    8. &p \Leftrightarrow q       &\Leftrightarrow\text{intro},6,7
\end{array}$$
Is the above proof correct? Please correct me.
 A: No, that is not correct.
I'm assuming it's supposed to be some kind of natural deduction system, but the deductions you annotate with $\neg$elim and $\to$into don't follow any sane negation elimination or implication introduction rules I know.
For example you try to conclude $p$ from $\neg p$. That makes no logical sense "Socrates is mortal, ergo Socrates is not mortal"??
And your introduction of the $\to$s look like you think you have a rule saying "from $p$ and $q$ conclude $p\to q$". This rule is actually sound, but it is far too weak to be useful in general, and is almost certainly not the introduction rule your text has presented.
A: The proof must be :
1) $\lnot p \land \lnot q$ --- premise
2) $\lnot p$ --- form 1) by $\land$-elim
3) $\lnot q$ --- form 1) by $\land$-elim
4) $p$ --- assumed [a]
5) $\bot$ --- from 2) and 4) by $\lnot$-elim
6) $q$ --- from 3) and 5) by RAA (or Double negation)
7) $p \rightarrow q$ --- from 4) and 6) by $\rightarrow$-intro, discharging [a]
8) $q$ --- assumed [b]
9) $\bot$ --- from 3) and 8) by $\lnot$-elim
10) $p$ --- from 2) and 9) by RAA (or Double negation)
11) $q \rightarrow p$ --- from 8) and 10) by $\rightarrow$-intro, discharging [b]

12) $p \leftrightarrow q$ --- from 7) and 11) by $\leftrightarrow$-intro.

