Understanding ex falso quodlibet together with proof by contradiction in a Gentzen style ND Proof

If you discharge an assumption labelled $z$ you should remember to actually label the assumption.

Also, ex falso quodlibet is not a rule of discharging; the rule to discharge $y$ is negation introduction, which needs to be followed by double negation elimination (though some do combine it into Reduction Ad Absurdum (RAA)).

$$ \dfrac{ \dfrac{ \dfrac{ \dfrac{ \lower{1.5ex}{[\neg (P \to Q)]^z} \quad \dfrac{ \dfrac{ \dfrac{[\lnot P]^y\quad[P]^x}{\bot}{\lnot E} }{Q}{\rm efq} }{P\to Q}{\to I^x} }{\bot}{\rm efq} }{\lnot\lnot P}{\lnot I^y} }{P}{\lnot\lnot E} }{\neg (P \to Q) \to P}{\to I^z} $$

---

This was an example in Jean Gallier's Discrete Mathematics book. I feel like I got the mechanical parts understood. Still, my head hurts when thinking about how I assumed both $P$ and $¬P$ to prove something. How do you guys understand this? How can we assume both $P$ and $¬P$, isn't that absurd?

Yes, that is how Reduction to Absurdity proofs operate: "If this assumption was true it, then what follows would be absurd, so therefore it cannot be true."

In this proof: When given $\lnot (P\to Q)$ should we also assume $\lnot P$, then we could prove $P\to Q$ (through the ex falso quodlibet subproof), which is absurd, so therefore $\lnot (P\to Q)$ entails $P$, and so we deduce $\lnot(P\to Q)\to P$.

Here's the fitch style representation which may be easier to follow. $$\def\fitch#1#2{\quad\begin{array}{|l}#1 \\\hline #2\end{array}}\fitch{}{\fitch{~1.~\lnot(P\to Q)}{\fitch{2.~\lnot P}{\fitch{~3.~P}{~4.~\bot\hspace{14ex}\lnot e, 2,3\\~5.~Q\hspace{14ex}\text{efq},4}\\~6.~P\to Q\hspace{12ex}{\to}i,3-5\\~7.~\bot\hspace{17ex}\lnot e,1,6}\\~8.~\lnot\lnot P\hspace{18ex}\lnot i,2-7\\~9.~P\hspace{21ex}\lnot\lnot e,8}\\10.~\lnot(P\to Q)\to P\hspace{10ex}{\to}i,1-9}$$

In this notation we keep track of the order in which assumptions are raised and discharged by indentation. Here we see that a contradiction can be derived on raising the third assumption, and so we may validly derive $Q$ within that context (because whatever $Q$ may be, it is at least as true as an absurdity).

Ex falso Quodlibet: If we can say "false is true", then we may say anything is true.

Here's how we can organize things (informally) to make a bit more sense.

1. We want to prove $\lnot(P\to Q)\to P,$ so we assume $\lnot(P\to Q)$ and our goal is to prove $P$.
2. We will prove $P$ by assuming $\lnot P$ and deriving a contradiction.
3. We will derive a contradiction by proving $P\to Q,$ which contradicts with our assumption of $\lnot(P\to Q).$
4. We will prove $P\to Q$ by assuming $P$ and then proving $Q.$
5. We will prove $Q$ by proving a contradiction, from which we can prove anything (ex falso.)
6. There is a contradiction between our assumption of $\lnot P$ and our assumption of $P.$

So we did assume $\lnot P$ and assume $P$ and get nonsense, but the assumptions had an orderly motivation and nonsense was exactly what we needed to prove $Q,$ which was a goal we had at that moment in the proof. (And this was certainly not an unconditional proof of an absurdity, it was under specific assumptions that were framed up in the larger structure of the proof.) Perhaps a better way to think about it is that what we wanted to prove was $P\to Q$ under the assumption that $P$ is false... which should seem quite plausible.

As Graham Kemp points out in his answer, the convention of using 'efq' to discharge an assumption is a little bit non-standard and usually this is called RAA or framed as double negation elimination.