The principle of explosion is this:

$$ X \land \lnot X \rightarrow Y $$

And similarly, the rule of weakening/monotonicity of entailment is this:

$$ (X \rightarrow Y) \rightarrow (X \land A \rightarrow Y) $$

If in a given logic, the rule of weakening holds, you could substitute $X = P$, $Y = Q$, and $A = \lnot P$ (or $P = \lnot P$ and $A = P$) in the rule of weakening to get something that gets close assuming the law of the excluded middle holds (see line 4) - it matches the principle of explosion at least when $Q = X = \top$:

$$ (P \rightarrow Q) \rightarrow (P \land \lnot P \rightarrow Q) \tag{1} $$ $$ (\lnot P \rightarrow Q) \rightarrow (P \land \lnot P \rightarrow Q) \tag{2} $$ $$ ((P \lor \lnot P) \rightarrow Q) \rightarrow ((P \land \lnot P) \rightarrow Q) \tag{3} $$ $$ Q \rightarrow (P \land \lnot P \rightarrow Q) \tag{4} $$

Similarly, most logics I've found that reject the law of the excluded middle also reject the principle of explosion, either implicitly like minimal logic or explicitly like relevant logic. This pervasive pattern led me to question why that pattern exists in the first place - if nobody is making their logic work with it when they drop the rule of weakening, is it even possible at all (despite the broad opinionatedness)?

My question is two-fold:

  1. Does the principle of explosion depend on the rule of weakening in any case? Or in more formal terms, does proving the rule of weakening to hold also prove the principle of explosion to hold or vice versa? If not generally, then under what constraints? (The above proof sets two constraints, but I'm not fully convinced either one of them are absolute.)

  2. Are there any known non-monotonic logics where the principle of explosion does hold? (This would serve as a counterexample to my hypothesis.)

  • 6
    $\begingroup$ The best known logic that rejects excluded middle is intuitionistic logic, and it does recognize explosion. Intuitionistic linear logic rejects both excluded middle and weakening, but still retains explosion. $\endgroup$ May 22 '18 at 12:15
  • $\begingroup$ Oh, and what kind of thing is (4) even? Usually $\vdash$ wants one or more formulas on its right-hand side but does not itself produce a formula, so (4) does not look like it's a well-formed bit of symbolism at all. $\endgroup$ May 22 '18 at 12:42
  • $\begingroup$ I'm using sequent calculus syntax, but I can edit that to be a bit more traditional instead. $\endgroup$ May 22 '18 at 12:46
  • $\begingroup$ @IsiahMeadows: There is nothing like $\cdots\vdash(\cdots\vdash\cdots)$ in sequent calculus. $\endgroup$ May 22 '18 at 12:54
  • $\begingroup$ To clarify, I'm talking about predicates and logical consequence in the abstract here. Each line in 1-6 is supposed to amount to a tautology. I fixed it to be a little more traditional instead. $\endgroup$ May 22 '18 at 12:55

I find the following form of the principle of explosion more useful in proofs:

$$A\implies [\neg A \implies B]$$

I don't how much flexibility you have in choosing your axioms, but here is a proof using natural deduction (more straightforward than substitutions):

1) $A$ (assume)

2) $\neg A$ (assume)

3) $\neg B$ (assume)

4) $A \land \neg A$ (intro $\land$, 1, 2)

5) $\neg \neg B$ (discharge, 3)

6) $B$ (elim $\neg \neg$, 5)

7) $\neg A \implies B$ (discharge, 2)

8) $A\implies [\neg A \implies B]$ (discharge, 1)

See my formal proof in HTML format here.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.