A simpler derivation of ($\phi \lor (\neg \phi)$)

Question

In Chiswell&Hodges [Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007)] they use this derivation to prove ($\phi \lor (\neg \phi)$):

A page earlier they used a simpler derivation that could also have been used to prove ($\phi \lor (\neg \phi)$). Can you check that I am not mistaken?

At the last step they add $\neg$ to $(\neg(\phi \lor (\neg \phi)))$ and get $(\neg(\neg(\phi \lor (\neg \phi))))$. But they could have used Reduction Ad Absurdum rule and removed the negation and gotten $(\phi \lor (\neg \phi))$.

Answer 1

You are right.

Your second example is [page 28] :

Example 2.7.1 :We prove the sequent $(¬(¬(φ ∨ (¬φ))))$.

See the final comment :

[...] At first sight it looks as if the two ¬ signs at the beginning of the conclusion have made extra work for us. This is not so. The sequent $(φ ∨ (¬φ))$ is certainly valid, but it is just as hard to prove; in fact the proof needs (RAA).