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

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)$$

$$(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.)

• No one should lose sleep over proving that $\neg (\phi \leftrightarrow \psi) \vdash \neg \phi \leftrightarrow \psi$ ... Why are we still torturing our students this way? – Bram28 Feb 15 '17 at 4:48
• You can try with a long sub-proof : assuming $\lnot \phi$ and $\lnot \psi$ derive (by contraposition) $\phi \leftrightarrow \psi$. Then you have a contradiciton with the premise and, by double negation, you can derive $\psi$ discharging $\lnot \psi$ and conclude with $\lnot \phi \to \psi$ by $\to$-intro, discharging $\lnot \phi$. – Mauro ALLEGRANZA Feb 15 '17 at 6:58
• @Bram28 Why not? I'm not in a class, I'm doing this to myself. I took a long distance degree in philosophy, but it had no formal logic, which as an engineer I found interesting. However, I've yet to appreciate where people actually use formal logic (I've seen people say how important it is in many texts, but no actual use). So my question is genuine - why IS this a waste of time? Is it impractical? – Lugh Feb 15 '17 at 14:32
• @MauroALLEGRANZA I was afraid someone would suggest a strategy not yet introduced in the book, but in my midnight wisdom I was not sure how to head this off, and hoped an answer within the constraints simply appeared. A little more awake, the only rules available are elimination/introduction of $\land$, $\rightarrow$, $\leftrightarrow$, and $\lnot$. I believe the authors intend the problem to be solved using only these rules. I've since edited the original question. – Lugh Feb 15 '17 at 14:47
• @Lugh Concerning the practical relevance of logic, consider program verification. Microsoft has a computer farm running their theorem prover Z3 24/7 to expose security vulnerabilities. They do it because it's effective. There are many other examples. – Fabio Somenzi Feb 15 '17 at 15:20

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].

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)$$

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.