Why is the principle of explosion accepted in constructive mathematics?

Question

I think something is wrong with the principle of explosion, because according to it, if I know $P\wedge \lnot P$, I can deduce $Q$ though I don't know anything about $Q$.

Is it really constructive to decide whether $Q$ is true by only seeing $P$ unrelated to $Q$? If $P\wedge \lnot P$ holds, how do I construct a reason for $Q$ ?

Answer 1

As correctly pointed out by @DanielV, the principle of explosion (aka ex falso quodlibet) just says that $(P \land \lnot P) \to Q$ holds for any formula $Q$ (possibly unrelated to $P$). It does not mean that $Q$ holds, but only that if $P \land \lnot P$ held then $Q$ (which could be anything) would hold; as in a consistent system $P \land \lnot P$ never holds, from the principle of explosion we cannot infer whether $Q$ holds or not.

So, the principle of explosion does not contradict constructivity, this is the reason why it is accepted in a constructive setting such as intuitionistic logic. The principle of explosion just says that if a theory contains a single inconsistency, such a theory is trivial—that is, it can prove everything. Therefore, according to the principle of explosion, there is only one inconsistent theory: the trivial theory that has every sentence as a theorem.

An informal justification of the principle of explosion is the following: if $P$ and its negation $\lnot P$ are both assumed, then $P$ holds, from which it follows that at least one of the claims $P$ and some other (arbitrary) claim $Q$ holds. However, as we know that either $P$ or $Q$ holds, and also that $P$ does not hold (that is, $\lnot P$ holds) we can conclude that $Q$ holds. This argument is constructive, in that it is valid in classical logic as well as in intuitionistic logic.

---

There are logics that reject the principle of explosion: paraconsistent logics and in particular minimal logic. Such logics make it possible to distinguish between inconsistent theories and to reason with them. The idea is that it ought to be possible to reason with inconsistent information in a controlled and discriminating way, which is precluded by the principle of explosion.

For more information, see here, here and here.

Answer 2

In the BHK interpretation of constructive logic, a proposition is "true" when you provide a witness for it. You get different notions of constructive logic by defining "witness" in different ways. For example, you could say a witness is a Turing machine that will compute the relevant evidence. For our purposes, let's say for each proposition we assign a set of witnesses. We don't do this arbitrarily though. For an proposition variable, we may assign a set of witnesses arbitrarily, but, in particular, for $A\to B$, we assign as the set of witnesses the function space between the set of witnesses of $A$ and the set of witnesses of $B$. All this is to say, that for this example, a witness of an implication is a (set-theoretic) function from a set of witnesses of $A$ to a set of witnesses for $B$. We also assign the empty set of witnesses to $\bot$, the nullary connective for falsity corresponding to a contradiction¹.

For the particular notion of "witness" just described, the principle of explosion is "true" constructively because it is witnessed. In particular, it is witnessed by the empty function. For most of the other common choices for the notion of "witness", there is some analogue of the empty function. One take on generalizing the BHK interpretation, in the case of Intuitionistic Propositional Logic (IPL), is saying that we have a Heyting category of witnesses and the BHK interpretation is a Heyting functor from the (thin) syntactic Heyting category describing IPL to that Heyting category of witnesses. Heyting categories have initial objects which represent $\bot$ and the unique arrow from an initial object to any other object is the generalization of the empty function. Whenever our category of witnesses has an initial object (that's well-behaved in a certain sense and we also have some other "structural" stuff), then we can interpret the $\bot$ connective. Having the $\bot$ connective means having the principle of explosion in the form $\bot\vdash\varphi$ for all $\varphi$.

Of course, we could just drop $\bot$ and weaken the requirement that the category of witnesses be Heyting and that we have a Heyting functor to not include the initial object stuff. That's a completely reasonable thing to do and will lead to a paraconsistent logic such as minimal logic. It's not so much "do we support the principle of explosion" as "do we have (something equivalent to) the $\bot$ connective". However, dropping $\bot$ means we need a different story for negation, $\neg$, or dropping we need to drop negation entirely. For intuitionistic logics, negation is usually defined as $\neg\varphi\equiv\varphi\to\bot$.

¹ I strongly recommend providing $\bot$ as a primitive connective (for logics where contradictions make sense). Always talking about $P\land\neg P$ is tedious and kind of hacky. Why do I need to arbitrarily choose some irrelevant proposition $P$ just to talk about a fundamental concept like contradiction?

Answer 3

Here's one way to look at it. Suppose we're working in a natural deduction system with a $\lor$-elimination rule that goes $$ \frac{\Gamma\vdash P\lor Q \qquad \Gamma, P\vdash R \qquad \Gamma, Q\vdash R}{\Gamma\vdash R} $$ This allows us to prove things by case analysis once we have proved a $\lor$ that tells us we have to be in one of the cases.

Now, what is the fundamental thing knowing $\neg P$ tells us? Arguably it is that in the above rule we won't need to carry out the $\Gamma, P\vdash R$ part of the proof because $P$ cannot actually happen.

We could achieve that by having a bunch of specialized $\lor$-elimination rules such as $$ \frac{\Gamma\vdash P\lor Q \qquad \Gamma, P\vdash A \qquad \Gamma\vdash\neg A \qquad \Gamma, Q\vdash R}{\Gamma\vdash R} $$ but it is simpler to wrap all the variants up in a single rule that says:

If you find yourself in a branch of a proof where two contradictory things appear to hold, it means that proof branch was not actually necessary, and you're allowed to cancel it completely by pretending you've already proved whatever you were aiming for in that branch.

That's basically what the principle of explosion does.

It is constructively acceptable because intuitively there are only two ways it's ever possible to use it:

1. Either your initial assumptions in the proof are impossible to satisfy. Then we don't really care if we conclude nonsense. What we do care is that if our assumptions hold then the conclusion will also hold. Otherwise we're happy with garbage-in, garbage-out.

2. Or you have introduced an additional temporary assumption somewhere in the proof tree which creates the contradiction. For example, the $\Gamma,P\vdash R$ premise in our $\lor$-elimination rule does that. Then we can justify the use of explosion by arguing that the branch that the explosion happened in was not actually necessary because the conditions it would be relevant in cannot happen.

3. If the additional assumption came from an introduction rule such as $\to$-introduction, the argument that "this branch is not needed" is not as immediately convincing. However, in that case we can argue that we're still "constructively safe", because then our conclusion of that introduction rule is something that involves $\to$. And the only way we can use that result is by using it in modus ponens (aka $\to$-elimination). At that time someone will be claiming they can prove the antecedent of the $\to$, but we know that is not actually realistic because the assumption leads to a contradiction! So this tells us that the proof branch where the modus ponens is found will itself be an unneeded branch, so constructively we don't need to worry about shenanigans there. It will never be executed.

   The story for $\neg$-introduction is similar to that for $\to$-introduction; then the principle of explosion itself is the relevant elimination rule.