Problem understanding $\lnot$E, $\lnot$I, and RAA rule in Gentzen style proofs I am self-studying Chiswell and Hodges' book and I am really confused about $\lnot$E, $\lnot$I, and RAA rule in Gentzen style proofs. (I learned Fitch style proof before, maybe that's why?) Specifically, this problem: 

I understand that $\phi$ comes as an assumption since we are proving a conditional; but where does $\lnot\phi$ come from?
Also, the application of $\lnot$I here looks like the principle of explosion to me? Why are we then able to apply the result ($\lnot\lnot\phi$) from an absurdity to the conclusion? Surely from an absurdity the only thing we can infer is that there is something wrong with our assumption.
Furthermore, here are the rules as laid out in the book; isn't $\lnot$I just the same as RAA, i.e. assume the negation of what we want to prove, then prove otherwise by deriving an absurdity? Why are they distinct from each other?



 A: Since you understand why $\varphi$ was added as an assumption, then you can understand why $\neg\varphi$ is added. You can easily show that the $\neg E$ and $\neg I$ are instances of $\to\!\!E$ and $\to\!\!I$ if we were to take $\neg\varphi$ as just a shorthand for $\varphi\to\bot$.
A: You are proving $\vdash \phi\to\lnot\lnot\phi$ by way of Gentzen's presentation, which has a Fitch-style equivalent.$$\def\fitch#1#2{\hspace{1.75ex}\begin{array}{|l}#1 \\\hline #2\end{array}}\require{enclose}\require{cancel}
\enclose{circle}{\small 1}\dfrac{\enclose{circle}{\small 2}\dfrac{\dfrac{\cancelto 1{~~\phi~~}\cancelto 2{~~\lnot\phi~~}}{\bot}{\small\lnot\textsf E}}{\lnot\lnot\phi}{\small\lnot\textsf I}}{\phi\to\lnot\lnot\phi}{\small\to\!\textsf I}\qquad\fitch{}{\fitch{~1.~\phi}{\fitch{~2.~\lnot\phi}{~3.~\bot\hspace{4.25ex}\lnot\textsf E,1,2}\\~4.~\lnot\lnot\phi\hspace{4.5ex}\lnot\textsf I, 2{-}3}\\~5.~\phi\to\lnot\lnot\phi\hspace{2.5ex}{\to}\textsf I,1{-} 4}$$

I understand that $ϕ$ comes as an assumption since we are proving a conditional; but where does $¬ϕ$ come from?

They are both assumptions. As indicated by the indices on the strikethroughs, assumption of $\phi$ is discharged by the rule of conditional introduction, while the assumption of $\lnot\phi$ is discharged by the rule of negation introduction.   The Fitch presentation also shows where the assumptions are raised and discharged.

Also, the application of $¬$ I here looks like the principle of explosion to me? Why are we then able to apply the result ($¬¬ϕ$) from an absurdity to the conclusion? 

The distinction is that ex falso quodlibet derives a new proposition within the same context as the absurdity, while negation introduction is a rule that discharges the assumption from which the absurdity was derived.
The usage of this rule is similar to conditional introduction; indeed, if negation is defined as the implication of absurdity ($\lnot\phi\equiv\phi\to\bot$), then the above proofs would only use the conditional rules.
$$\enclose{circle}{\small 1}\dfrac{\enclose{circle}{\small 2}\dfrac{\dfrac{\cancelto 1{~~\phi~~}\cancelto 2{~~\phi\to\bot~~}}{\bot}{\small\to\textsf E}}{(\phi\to\bot)\to\bot}{\small\to\textsf I}}{\phi\to((\phi\to\bot)\to\bot)}{\small\to\!\textsf I}\qquad\fitch{}{\fitch{~1.~\phi}{\fitch{~2.~\phi\to\bot}{~3.~\bot\hspace{15ex}{\to}\textsf E,1,2}\\~4.~(\phi\to\bot)\to\bot\hspace{6ex}{\to}\textsf I, 2{-}3}\\~5.~\phi\to((\phi\to\bot)\to\bot)\hspace{2ex}{\to}\textsf I,1{-} 4}$$

Surely from an absurdity the only thing we can infer is that there is something wrong with our assumption.

Precisely so.   Since an absurdity is derived from the assumption then we may discharge that assumption and deduce that its negation is true.   In this proof, the assumption being discharged is $\lnot\phi$. 
That is that from $\Gamma,\lnot\phi\vdash\bot$ we infer $\Gamma\vdash\lnot\lnot\phi$. 

Furthermore, here are the rules as laid out in the book; isn't $¬$I just the same as RAA, i.e. assume the negation of what we want to prove, then prove otherwise by deriving an absurdity? Why are they distinct from each other? 

RAA is a combination of negation introduction and double negation elimination. $$\dfrac{\enclose{circle}{\small 1}\dfrac{\cancelto 1{~~ \lnot\phi~~}\\\quad\vdots\\\quad\bot}{\lnot\lnot\phi}{\lnot\textsf I}}{\phi}{\lnot\lnot\textsf E}$$
Negation Elimination is the rule for a Proof of Negation: where one assumes a claim aiming to derive a contradiction and so deduce that its negation holds.   From $\psi\vdash\bot$ infer that $\vdash\lnot\psi$.
Reduction to Absurdity is the rule for a Proof by Contradiction, where one assumes the negation of a claim aiming to derive a contradiction and so deduce that the claim holds.  From $\lnot\psi\vdash\bot$ infer that $\vdash\psi$.
A: 
I understand that $\phi$ comes as an assumption since we are proving a conditional; but where does $\lnot\phi$ come from?

The $\lnot\phi$ is also an assumption, and since that assumption together with the $\phi$ leads to a contradiction, you use $\neg$ I to derive $\neg (\neg \phi)$.   

Also, the application of $\lnot$I here looks like the principle of explosion to me? 

No ... it's the formalization of the proof by contradiction.

Why are we then able to apply the result ($\lnot\lnot\phi$) from an absurdity to the conclusion? 

Again, they don't use the principle of explosion here. That is, they don;t derive $\neg (\neg \phi)$ form the contradiction, but rather derive $\neg (\neg \phi)$ from the fact that the assumption $\neg \phi$ leads to a contradiction.

Surely from an absurdity the only thing we can infer is that there is something wrong with our assumption.

Not true. From a contradiction we can infer anything! Typically, this would be formalized using a $\bot$ E rule:  from $\bot$ derive any statement $\phi$

isn't $\neg$ I just the same as RAA

No, it is not. $\neg I$ infers $\neg \phi$ if $\phi$ leads to a contradiction, whereas RAA infers $\phi$ if $\neg \phi$ leads to a contradiction. In non-classical logics, that makes a big difference.
Finally, their $\neg $ E is pretty weird in that it doesn't seem to eliminate any $\neg$'s at all ... I would call that rule $\bot$ I
