Need help with natural deduction logic proof (Chiswell/Hodge exercise 2.6.2d)

Question

in Chiswell/Hodge exercisee 2.6.2d it asks for the proof of $\{\lnot(\phi\leftrightarrow\psi)\}\vdash((\lnot\phi)\leftrightarrow\psi)$. I've managed to produce half the proof, but I'm unable to produce the other half indicated at D.

$$ \frac{(1)\frac{D^{(1)}}{((\lnot\phi)\rightarrow\psi)}(\rightarrow I) \qquad \frac{\cfrac{(6)\frac{\phi^{(6)}\quad\psi^{(2)}}{\phi\rightarrow\psi}(\rightarrow I)\quad (5)\frac{\psi^{(5)}\quad\phi^{(4)}}{\psi\rightarrow\phi}(\rightarrow I)}{\phi\leftrightarrow\psi}(\leftrightarrow I)\qquad \lnot(\phi\leftrightarrow\psi)}{(4)\cfrac{\bot}{(2)\cfrac{\lnot \phi}{(\psi\rightarrow(\lnot\phi))}(\rightarrow I)}(\lnot I)}(\lnot E)} {((\lnot\phi)\leftrightarrow\psi)}(\leftrightarrow I) $$

I had considered...

$$(1)\frac{\cfrac{\phi\quad\lnot\phi^{(1)}}{\cfrac{\bot}{\psi}(RAA)}(\lnot E)} {((\lnot\phi)\rightarrow\psi)}(\rightarrow I)$$

But that leaves me with an undischarged $\phi$. I'm otherwise unsure of how to produce the $\psi$ for the $(\rightarrow I)$ in the left branch, as an absurdity (other than as proposed) discharges $\lnot\psi$, and I can't use this to construct an absurdity against the assumption $\lnot(\phi\leftrightarrow\psi)$ similar to how I did in the right branch.

At this point in the text, the only rules available are elimination/introduction of $\land$, $\rightarrow$,$\leftrightarrow$,$\lnot$ and RAA.

I would be very grateful to understand this particular exercise further as I'm losing sleep over it.

(Also if someone has formatting advice regarding \frac or some suitable alternative via PM, I would be further grateful.)

Answer 1

This answer is only possible due to the answer provided by MauroAllegranza; however, their answer is in Fitch style, and I wanted to provide a Gentzen style to match the question, in case someone searches for this in the future.

The following is only the solution to D, as provided by Mauro, to sub into the overall proof. For formatting reasons I had to further break it down, hence D1.

Part#1 (D1) $$ D1=\dfrac{(4)\cfrac{\cfrac{\cfrac{\psi^{(4)}\quad\lnot\psi^{(3)}}{\bot}(\lnot E)}{\phi}(RAA)}{\psi\rightarrow\phi}(\rightarrow I)\quad (2)\cfrac{\cfrac{\cfrac{\phi^{(2)}\quad\lnot\phi^{(1)}}{\bot}(\lnot E)}{\psi}(RAA)}{\phi\rightarrow\psi}(\rightarrow I)}{(\phi\leftrightarrow\psi)}(\leftrightarrow I) $$

Part#2 (D)

$$ D= (1)\dfrac{(3)\cfrac{\cfrac{\cfrac{D1^{(3)(1)}}{(\phi\leftrightarrow\psi)}\qquad\lnot(\phi\leftrightarrow\psi)}{\bot}(\lnot E)}{\psi}(RAA)}{((\lnot\phi)\rightarrow\psi)}(\rightarrow I) $$

Answer 2

1) $\lnot (\phi \leftrightarrow \psi)$ --- premise

2) $\lnot \phi$ --- assumed [a]

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

4) $\lnot \psi$ --- assumed [c]

5) $\bot$ --- from 3) and 4)

6) $\phi$ --- from 2) and 5) by Double Negation, discharging [a]

7) $\psi \to \phi$ --- from 3) and 6) by $\to$-intro, discharging [b]

8) $\lnot \phi \vdash \phi \to \psi$ --- repeat the derivation above, with assumption [d] : $\lnot \phi$

9) $\lnot \psi, \lnot \phi \vdash (\phi \leftrightarrow \psi)$ --- from 7) and 8) by $\leftrightarrow$-intro

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

11) $\psi$ --- from 4) and 10) by Double Negation, discharging [c]

12) $\lnot \phi \to \psi$ --- from 8) and 12) by $\to$-intro, discharging [d].

We have discharged all the "temporary" assumptions; thus, the above derivation amounts to :

$\lnot (\phi \leftrightarrow \psi) \vdash (\lnot \phi \to \psi)$

---

You can also simplify the other part a little bit...

1) $\lnot (\phi \leftrightarrow \psi)$ --- premise

2) $\phi$ --- assumed [a]

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

4) $\phi \to \psi$ --- from 3) by $\to$-intro

5) $\psi \to \phi$ --- from 2) by $\to$-intro

6) $\phi \leftrightarrow \psi$ --- from 4) and 5) by $\leftrightarrow$-intro

7) $\bot$ --- from 1) and 6)

8) $\lnot \phi$ --- from 2) and 7) by $\to$-intro, discharging [a]

9) $\psi \to \lnot \phi$ --- from 3) and 8) by $\to$-intro, discharging [b].

Answer 3

The quickest proof of all would simply involve noticing that the negation of "if and only if" is an XOR operation. Then to notice that $\lnot p\leftrightarrow q$ will read: $p(\lnot q)\lor (\lnot p)q$ . Which, (funnily enough) is an XOR operation.

As $\ \lnot(A\leftrightarrow B)=\ A\oplus B$

And as $\ \lnot p\leftrightarrow q=\ p(\lnot q)\lor (\lnot p)q\ $

which in turn is $\ p\oplus q$

$\therefore \lnot(p\leftrightarrow q) = \lnot p\leftrightarrow q$

It may not be in the style of the question but I thought you might appreciate the brevity of this proof.

Answer 4

Since I wrote the proof during my own study, I might as well post it here.