What is an example of a proof that uses the principle of explosion/ex falso quodlibet?

Question

I am reading through Mathematical Logic by Ian Chiswell and Wilfrid Hodges. In chapter 2 they introduce natural deduction rules. Before stating a rule, the authors (usually) motivate the rule by showing some informal proof that uses that rule's reasoning. For example, to motivate the rule (RAA), which I've thrown at the bottom of this post for reference, the authors point to the following proof that there are infinitely many prime numbers:

"Assume not. Then there are only finitely many prime numbers

$$ p_1,...,p_n $$

Consider the integer

$$ q = (p_1 \times ... \times p_n) + 1 $$

The integer $q$ must have at least one prime factor $r$. But then $r$ is one of the $p_i$, so it cannot be a factor of $q$. Hence $r$ both is and is not a factor of $q$; absurd! So our assumption is false and the theorem is true."

This proof only seems to motivate part of the (RAA) rule, namely the case where there IS an assumption to discharge (we conclude that there are infinitely many prime numbers, discharging the assumption that "it is not true that there are infinitely many prime numbers"). However, this rule can also be used in cases where nothing is discharged (in other words, this rule contains the principle of explosion/ex falso quodlibet as a special case; see here for a related discussion). For example, the book starts out a proof of the sequent $\vdash ((\lnot(\phi\to\psi))\to\phi)$ with

$$ \begin{align} \dfrac{\phi \qquad \qquad (\neg\phi)} {\qquad \quad \dfrac{\quad \bot\quad} { \quad\psi \quad} (RAA) }(\neg E) \end{align} $$

where $\psi$ is then used further on in the proof... I don't recall ever seeing a proof in math that went something like this, where a contradiction was reached and we kept going.

So, my question in short is: what is an example of a proof that uses the principle of explosion in this way, or more generally, just how is the principle of explosion used in "normal" math?

---

Statement of (RAA) for reference: Suppose we have a derivation $$ \\\\\ D \\\\\ \bot $$ whose conclusion is $\bot$. Then there is a derivation $$ \require{cancel}(\cancel{~\lnot\phi~}) \\\\\ D \\\\\ \quad \quad \quad \dfrac{\bot}{\phi}(RAA) $$

Answer 1

The short answer to "how is the principle of explosion used in 'normal' math?" is: it isn't.

You can set up a natural deduction proof system for a first-order logic which is as adequate for normal maths (and science) as standard FOL, but lacks ex falso quodlibet. Neil Tennant has over the years shown how to do this in a sequence of papers, and then a book, Core Logic (OUP, 2017).

A core(!) result about this system is this:

if $\Gamma \vdash_\mathrm{Classical} \varphi$ then either $\Gamma \vdash_\mathrm{Core} \varphi$ or for some $\Delta \subseteq \Gamma$, $\Delta \vdash_\mathrm{Core} \bot$.

Hence, if $\Gamma$ is consistent you can still derive whatever you could derive in a standard classical system with ex falso; while if $\Gamma$ is inconsistent you can show it to be so. What you can't do, in core logic, is get from inconsistent premisses $\Gamma$ to some random irrelevant conclusion.

---

You might wonder how this can work. Don't we need ex falso to derive disjunctive syllogism using the standard or-elimination rule? Well, arguably so much the worse for the standard rule. As Tennant has put it

Suppose one is told that $A \lor B$ holds, along with certain other assumptions $X$, and one is required to prove that $C$ follows from the combined assumptions .... If one assumes $A$ and discovers that it is inconsistent with $X$, one simply stops one's investigation of that case, and turns to the case $B$. If $C$ follows in the latter case, one concludes $C$ as required. One does not go back to the conclusion of absurdity in the first case, and artificially dress it up with an application of the absurdity rule so as to make it also "yield" the conclusion $C$.

Surely that is an accurate account of how we ordinarily make deductions! In common-or-garden reasoning, drawing a conclusion from a disjunction by ruling out one disjunct surely doesn't depend on jiggery-pokery with explosion. Hence there seems to be much to be said -- if we want our natural deduction system to encode very natural basic modes of reasoning! -- for revising the disjunctive elimination rule to allow us to, so to speak, simply eliminate a disjunct that leads to absurdity. So we want to say, in summary, that if both limbs of a disjunction lead to absurdity, then ouch, we are committed to absurdity; if one limb leads to absurdity and the other to C, we can immediately, without further trickery, infer C; if both limbs lead to C, then again we can derive C. So officially the rule becomes

where if both the subproofs end in $\bot$ so does the whole proof, but if at least one subproof ends in $C$, then the whole proof ends in $C$. 

There's more to be said, and Tennant says it (at length). But the headline news is that if you use this as your or-elimination rule you can get everything you actually need by way of FOL without explosion.

---

If you check out Tennant's work, however, you might wonder whether the game is worth the candle as a practical proposal for logic reform. You might well think that adopting his Core Logic (without explosion) rather than standard logic (with explosion) would complicate logical life a bit too much for it to be worth mending our ways. We could argue the toss about that, but I might agree with you!

However that does not affect the point of principle. Tennant has certainly shown that you can do the same mathematics as before while using a deductive system for which the principle of explosion fails. Which answers the OP's orginal question.

Answer 2

The informal approach to this rule is basically a proof by cases. It's just not obvious from the formal setup.

I'm struggling to think of a "natural" example right now, so here's a slightly contrived one. Say we wanted to prove

for every $n \in \mathbb{N}$, if $n$ is even then $n^2$ is even.

Here is one way we might prove this. First, informally:

---

We're proving a claim for all $n$, so let $n$ be an arbitrary natural number.

Case 1: $n$ is odd. This isn't possible since we're assuming $n$ is even.

Case 2: $n$ is even. Then $n = 2k$ so $n^2 = 4k^2 = 2(2k^2)$ is even too

This exhausts the cases, so we're done.

---

Notice that we still technically have to consider case 1 in order to know our claim works for all naturals $n$. Most working mathematicians quickly move past this step to the interesting one, but of course when we're proving something very formally we can't do that.

Since we're working extremely formally, what do we need to do? If we're working in cases, each case should end with "$n^2$ is even", and we should exhaust all possible cases. This shows another formality which we usually ignore when proving things informally -- case $1$ ends with "this isn't possible", and moves on. Of course, it should end with "$n^2$ is even". As you might guess, the principle of explosion will let us bridge this gap!

Here is a slightly more formal version of the same proof:

---

We're proving a claim for all $n$, so let $n$ be an arbitrary natural number.

Case 1: $n$ is odd. We're assuming $n$ is even, so $n$ is both even and not even, letting us derive $\bot$. But of course $\bot$ implies everything, in particular it implies $n^2$ is even.

Case 2: $n$ is even. Then $n=2k$ so $n^2 = 4k^2 = 2(2k^2)$ is even too.

This exhausts the cases, so we're done.

---

This sort of maneuver where we ignore impossible cases is very common in working mathematics (as it should be! It's annoying and unnecessary to write these silly impossible cases all the time), but when computer formalizing these things can actually show up (since often the computer doesn't know what's obvious and unnecessary, haha), and we find ourselves explicitly invoking the principle of explosion much more frequently than mathematicians who work exclusively informally.

---

I hope this helps ^_^

Answer 3

In many formal systems you need this as a rule .. but as far as more informal logical reasoning ('normal math') goes, I think we simply stop investigating any line of investigation as soon as we reach a contradiction. Take, for example, some classic knights and knaves puzzle involving two people, A and B. One method we could use here is to exhaustively explore all 4 possible options (both are knights, both are knaves, ..), and see which one(s) work out. Those that don't work out (i.e. lead to a contradiction), we simply throw out, and typically we are left with 1 option (or, if there are multiple options left, there is something in common between them that we can then conclude).