Trouble understanding proof to $\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$?

I am having trouble understanding the natural deduction proof of $$\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$$ (question 2.6.2 (b)) in Hodges and Chiswell's Mathemaical Logic.

The natural deduction proof is as follows.

Image of proof

My questions are

1. Why is

\begin{align} \dfrac{\phi \qquad \qquad \neg\phi} {\qquad \quad \dfrac{\quad \bot\quad} { \quad\psi \quad} (RAA) }(\neg E) \end{align} a valid argument? Isn't RAA supposed to discharge an assumption when an absurdity is deduced?

2. Why can the derivation be continued before resolving the absurdity? (eg.①)
• Maybe I am missing something, but I do not believe the sentence is valid. If $\psi$ is true and $\phi$ is false, the first implication is false, so its negation is true, so the outer implication is false. I believe the final conclusion should be $\lnot \phi$. That makes the sentence true for all assignments to $\psi, \phi$ – Ross Millikan Dec 26 '18 at 6:21
• @RossMillikan The positions of $\phi$ and $\psi$ should be changed. I'll just edit it. Thanks for pointing that out. – Daigo C Dec 26 '18 at 6:30
• @MauroALLEGRANZA - As far as I understand, the question is about the fact that the first (from the top) occurrence of RAA in the derivation does not discharge anything. – Taroccoesbrocco Dec 26 '18 at 8:28

The reductio ad absurdum rule RAA (I use $$\ulcorner \!\cdot\! \urcorner$$ to mark discharged assumptions, with a superscript to point at the discharging rule) $$\begin{equation} \dfrac{\ulcorner \lnot \psi \urcorner^1 \\ \quad \vdots D \\ \quad \bot}{\psi}{\text{RAA}^1} \end{equation}$$ means that any arbitrary number (possibly none) of occurrences of the assumption $$\lnot \psi$$ in the derivation $$D$$ has been discharged by the last rule. In the particular case where RAA discharges no occurrences of the assumption $$\lnot \psi$$, the rule is also called ex falso quodlibet (EFQ), where the conclusion $$\psi$$ seems to pop out of nowhere: it means that from a contradiction you can correctly derive everything (see also Wikipedia's page).

The intuition behind the fact that EFQ is just a special case of RAA is the following: if you can derive a contradiction (the derivation $$D$$), then you can derive it even when you assume an extra hypothesis $$\lnot \psi$$ that actually you never uses in the derivation $$D$$.

Therefore, the answer to your first question is: yes, the derivation is perfectly valid, and the instance of RAA legitimately does not discharge any occurrence of the assumption $$\lnot \psi$$ (i.e. it is an instance of EFQ).

Concerning your second question, why do you want to/must stop before or after deriving a contradiction? All the inference rules in natural deduction are valid and hence they can be concatenated indefinitely preserving the validity of the argument. In particular, you can correctly carry on with your derivation before and after an EFQ.

Concerning the fact that an inference rule can discharge any arbitrary number (possibly none) of occurrences of the assumption, see p. 17 in Chriswell and Hodge's Mathematical Logic: the discussion is about the rule $$\to_I$$ (introduction of $$\to$$), but mutatis mutandis it is valid for RAA as well.

This is valid, but I would call the rule used that line ex falso (EFQ) rather than RAA. The rule looks like $$\dfrac{\quad \bot\quad }{\phi}(EFQ)$$ and is also valid intuitionistically (unlike RAA).

I'm not familiar enough with your book to know if what is written is 'wrong' or not, since you can make an application of ex falso into an application of RAA pretty easily: Simply add an assumption of $$\lnot \psi$$ anywhere up the tree from the $$\bot$$, then you can use the falsity you derived to conclude $$\psi$$ by RAA (and discharge the assumption).

Isn't $$\text {RAA}$$ supposed to discharge an assumption when an absurdity is deduced ?

Discharging an assumption is not compulsory.

See page 17 :

if $$\phi$$ is an assumption written somewhere in [a derivation] $$D$$, then we discharge $$\phi$$ by writing a dandah through it : $$\not \phi$$. In the rule $$(→ \text I)$$ below, and in similar rules later, the $$\not \phi$$ means that in forming the derivation we are allowed to discharge any occurrences of the assumption $$\phi$$ written in $$D$$. The rule is still correctly applied if we do not discharge all of them; in fact the rule is correctly applied even if $$\phi$$ is not an assumption of $$D$$ at all, so that there is nothing to discharge.

Why can the derivation be continued before resolving the absurdity ?

Because there are still open (i.e. undischarged assumptions) after the application of $$\text {RAA}$$ rule, and we can go on applying the rules of the calculus to them.