Proof, is $\lnot p \land \lnot q \vdash p \iff q$?

Question

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.

Answer 1

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.

Answer 2

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.