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

Question

I began studying some formal logic for possible future proof and type theory dives. I am at the very beginning, Gentzen style natural deductions. Some of these proof rules defies my intuition so I wanted to ask for some clarification.

Suppose we want to prove that $\neg (P \Rightarrow Q) \Rightarrow P$. Informally speaking:

1. Assume $\neg (P \Rightarrow Q)$, show $P$.

2. To show $P$, we will use proof by contradiction and we will assume $\neg P$.

   { At this stage, we have premises $\neg (P \Rightarrow Q)$ and $\neg P$ in our environment $\Gamma$ }

3. Now, If we can show $(P \Rightarrow Q)$ from $\Gamma$, we can conclude $\bot$ and complete our proof.

4. To show $(P \Rightarrow Q)$, assume $P$ and show $Q$.

   { At this stage, we have premises $\neg (P \Rightarrow Q)$, $\neg P$ and $P$ in our environment $\Gamma$ }

This is our proof strategy, informally. Below I show this as a formal proof tree. I hope it is readable enough, I had to play a lot with frac of $\LaTeX$. Notationally, $[P]^x$ means that $P$ is an assumption that is going to be removed from $\Gamma$ at the proof step $x$ somewhere below. efq stands for ex falso quodlibet.

$$ \dfrac{\dfrac{\neg (P \Rightarrow Q) \quad \dfrac{\dfrac{[\neg P]^y \space [P]^x}{\dfrac{\bot}{Q}\ \text{efq}}\ \neg-E}{P \Rightarrow Q} \ \Rightarrow - I^x \quad}{\dfrac{\bot}{P}\ \text{efq-y}}} {\neg (P \Rightarrow Q) \Rightarrow P}\ \Rightarrow - 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 $\neg P$ to prove something. How do you guys understand this? How can we assume both $P$ and $\neg P$, isn't that absurd? What am I missing so that I feel like this proof is bogus? Why do I feel like I can prove anything with this?

As a programmer, I suspect these assumptions are like local variables in a function from a computer program. For example, that assumption of $P$ is valid only in the program that proves $Q$ and is removed from the stack after that. Trying to use it for any other proof would be using an already deleted variable etc. I am not sure about forming this analogy though, since it is not mentioned in the book. I want logician's explanation.

Answer 1

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.

Answer 2

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.

Answer 3

FYI there is an easier way. No EFQ (explosion) or proof by contradiction is required. Just apply the definition of $\implies$ (line 2, below).

Screen print from DC Proof 2.0 proof checker:

If you insist on using EFQ (line 3, below) and proof by contradiction (line 5 and 6), try to following: