Dtyjlui

I am having trouble understanding the natural deduction proof of $vdash ((neg(phirightarrow psi))rightarrowphi)$ (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 negphi} {qquad
   quad dfrac{quad botquad} { quadpsi 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.①)

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.

See also this question and this question about EFQ and RAA.

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 botquad }{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.