Why is the Principle of Explosion considered constructive?

Question

I read over this post Why is the principle of explosion accepted in constructive mathematics? and still have some thoughts/questions.

One of the answers mentions that a formula is constructively valid when there is a witness for that formula. So, when we say there is a witness for the formula $\bot \to A$, we mean that there is a function from the set of witnesses for $\bot$ to the set of witnesses for $A$. This seems to be circular at the meta-level; in order to justify “if $x$ is a member of the empty set, then $\varphi(x)$,” one needs the Principle of Explosion. A similar charge of circularity can be made against using Disjunctive Syllogism as a justification for the constructiveness of Explosion.

Ultimately, I’m not a skeptic about Explosion, but I don’t exactly see how it is constructively valid. I know that Proof of Negation is constructively valid since it amounts to a version of conditional proof. If explosion is just an assumption of Intuitionistic Logic, that makes sense, but it seems a bit arbitrary to say that constructive proof definitely includes explosion. It seems like one could just assume the Law of the Excluded Middle as an axiom, and then everything in Classical Logic would be “constructively” provable, assuming LEM were considered constructive, as is the case with Explosion.

Is there a reason beyond pure logic that Intuitionistic logic is considered the stepping-stone into constructive logic, as opposed to something like Minimal Logic?

Answer 1

NB I start by talking about type theory in this first section, but the second section contains comments about usual first-order logic and Heyting arithmetic that also make sense on their own.

When we ask about the constructivity of certain moves, Per Martin-Löf's type theory provides a fairly comprehensive philosophical framework and a useful starting point, in the sense that almost all stakeholders accept it as constructive.

And we can formulate MLTT in such a way that explosion occurs as a proper theorem, not an axiom.

In type theory, as in most foundational systems, the statement $0=1$ is naturally explosive, in the sense that you can prove anything using $0=1$ without ever invoking any rule akin to explosion ($\bot$-elimination). How?

Let us start with MLTT and let $\mathcal{U}$ denote the type of small types (we won't need a cumulative universe hierarchy). Consider the modified type theory MLTT' obtained by removing the built-in empty type from MLTT. I.e. we only have dependent sum and product types $\Sigma,\Pi$, equality types $=$ on all sets, the type of natural numbers $\mathbb{N}$, and (if you wish) the singleton type $\top$, with their usual introduction and elimination rules. We define all other types using these primitives.

I will now show that the statement $0=1$ is naturally explosive in the modified type theory MLTT', i.e. that $0 = 1 \rightarrow P$ for any proposition/type $P$.

1. Assume $0 = 1$ and take your favorite proposition $P : \mathcal{U}$.

2. We can use the induction principle on the natural numbers (the elimination rule for $\mathbb{N}$) to construct a function $f: \mathbb{N} \rightarrow \mathcal{U}$ so that $f(0)$ reduces to $\top$, but $f(n+1)$ reduces to $P$ for all $n:\mathbb{N}$.

3. We can prove the congruence rule, $a = b \rightarrow f(a) = f(b)$ by applying the usual introduction and elimination rules of equality. Applying the congruence rule to the equality $0 = 1$, we get $f(0) = f(1)$, which reduces to $\top = P$.

4. Moreover, if $\top = P$, then $\top \rightarrow P$ holds. Why? Because we can obtain $\top = P \rightarrow (\top \rightarrow \top) \rightarrow (\top \rightarrow P)$ from the elimination rule for equality, and you can prove $\top \rightarrow \top$ itself trivially.

5. So if $0 = 1$, then $\top \rightarrow P$. But $\top$ holds, so by modus ponens (the elimination rule for dependent product), we immediately get $P$. Therefore, we have shown that $0 = 1 \rightarrow P$ as claimed.

At this point, we're done. We can just introduce $\bot$ as an abbreviation for $0=1$, and define negation $\neg P$ as $P \rightarrow \bot$ as we'd normally do, and go on with our lives. We regard explosion as constructive because we all agree on the constructivity of MLTT (at least when formulated without $\bot$, and hence without explosion), and we can explicitly define $\bot$ as $0=1$ and prove it explosive inside this constructive theory.

---

Of course, one could worry about the anachronistic character of the story above, in that intuitionistic logicians accepted explosion decades before Martin-Löf formulated his type theory in 1971.

But a similar phenomenon occurs even in foundational theories formulated in ordinary first-order intuitionistic logic: e.g. $0=1$ is explosive in Peano Arithmetic in Minimal Logic (PAML, the first-order Peano axioms stated in minimal logic -- not to be confused with minimal arithmetic, which most people use as a synonym Robinson's Q).

For example, if you want to prove using $0=1$ that every number is even in PAML, you can just multiply both sides of the inconsistent equality by $2$ to get $0=2$, apply transitivity to get $1=2$, then replace $1$ with $2$ in $\forall x. 1\cdot x=x$ to conclude $\forall x. 2\cdot x=x$, and then a fortiori $\forall x. \exists y. 2y = x$. You can do this systematically, by induction on the structure of the target formula $P$ to prove that $0=1 \rightarrow P$ for any proposition $P$ in the language of PAML.

---

This all relies on one key insight. The rules of the connectives determine their meaning. And $\bot$ does not have any other rules apart from its elimination rule (ex falso). Without rules, it does not, and cannot, have intrinsic meaning: it simply denotes "some formula". This happens in minimal logic: in minimal logic you can prove $A \rightarrow \bot$ precisely if you can prove $A^{[\bot/B]} \rightarrow B$ for any formula $B$, where $[\bot/B]$ denotes replacing all occurrences of the symbol $\bot$ with the formula $B$. In minimal logic, $\bot$ really just denotes some arbitrary formula.

When we add an elimination rule for $\bot$, we declare: we don't want this symbol to stand for any arbitrary formula. Instead, we want it to stand for some explosive formula. We don't really care which one, they're all logically equivalent anyway. But we're not adding anything new: we already know that explosive formulas exist, e.g. $\bot$ could stand for $0=1$.

And that is why we consider explosion constructive.

---

I had a conversation on this exact topic with four other constructive mathematicians at CM:FP '23 earlier today. I'm quite amused to see the question come up here a few hours after that. It must be on everyone's minds.

Answer 2

There are other excellent answers, but here is another piece of the story I find helpful: the comparison with disjunction.

First think about just disjunction for a moment, $A_1 \vee A_2$. It expresses the idea that “(at least) one of $A_1$ and $A_2$ holds”. And its elimination principle is just “proof by cases”, with two cases: to show $A_1 \vee A_2$ implies some statement $B$, it suffices to show that $A_1$ implies $B$ and $A_2$ implies $B$. This is very widely accepted as a good constructive principle; it has been supported by plenty of both philosophical arguments and precise mathematical results (e.g. normalisation and other good computational behaviour for logical systems incorporating this kind of disjunction).

But that was just binary disjunction: you can generalise to disjunctions of any number of statements, $\vee_n(A_1,\ldots,A_n)$ (equivalent to the statement usually built out binary disjunctions, as $A_1 \vee \ldots \vee A_n$). Everything we said about the binary case transfers straightforwardly to this. It expresses the idea that “at least one of the statements $A_1$, …, $A_n$ holds”. Its elimination principle is proof by cases, with $n$ cases: to show the disjunction implies $B$, it suffices to show that $A_1$ implies $B$, $A_2$ implies $B$, and so on up to $A_n$. The arguments for constructivity of binary disjunction all carry over happily enough to this general $n$-ary version. (Indeed, most of the above arguments make sense for any family of statements, $\{ A_i \mid i \in I \}$, not just finite families — keeping syntax finite of course requires restricting to the finite case, but almost all other parts of the arguments are completely generic in the set $I$.)

Now take the special case $n = 0$ — “nullary disjunction”. This gives a proposition $\bigvee_0$ expressing the concept “at least one of the statements [no statements at all] holds” — which will never be true, but is perfectly meaningful as a special case of the general notion. And its elimination rule should be proof-by-cases, with 0 cases: to show $\vee_0$ implies some statement $B$, you need to show… nothing at all! So this special case, nullary disjunction, recovers precisely the usual rules for $\bot$; and all the constructive justifications for general $n$-ary proof-by-cases become, as a special case, justifications for the principle of explosion.

I like this story for two different reasons. Specifically, it shows that the standard rules for $\bot$ are not just an isolated ad hoc idea needing separate motivation, but tie together into a family with the rules for $\vee$, and give a perhaps-enlightening reading for the meaning of $\bot$. More generally, it fits with the story in Z.A.K.’s answer: lots of general constructively-valid principles provide ways to build some “explosive” statement. So to reject the meta-theoretic justifications for explosion, it’s not enough to just drop the rules for $\bot$ or $\emptyset$ themselves in the meta-theory: you have to actively restrict lots of other principles, so that they only apply in non-empty/non-vacuous cases. This isn’t unreasonable or infeasible, but it puts some of the burden of justification on explaining these added restrictions — they require motivation just as much as adding a rule for falsehood or empty set does.

Answer 3

I'll give an example of how in the proof assistant Coq, which implements an intuitionistic logic, it is possible to explicitly construct a function from an empty type to any other type.

First, let me give a couple other examples to give an idea of the syntax that will be involved. The cartesian product type is defined as something like:

Inductive prod (X Y : Type) : Type :=
| pair (x : X) (y : Y) : prod X Y.

Now, to write a function using a value of such a type, you use a match expression such as:

Definition first {X Y : Type} (p : prod X Y) : X :=
match p return X with
| pair x y => x
end.

Similarly, a "disjoint union" type is defined as something like:

Inductive sum (X Y : Type) : Type :=
| left (x : X) : sum X Y
| right (y : Y) : sum X Y.

This represents what in many programming languages would be called a "tagged union". For an example of a match expression on such a value:

Definition case {X Y Z : Type} (s : sum X Y) (f : X -> Z) (g : Y -> Z) : Z :=
match s return Z with
| left x => f x
| right y => g y
end.

In parallel with these examples, we can construct an empty type which has no constructors, and therefore no possible way to create an element of that type:

Inductive Empty_type : Type :=
.

And for a match expression using this type:

Definition error (X : Type) (e : Empty_type) : X :=
match e return X with
end.

This follows the pattern of the first two examples, where an Inductive type with $n$ constructors requires $n$ branches in the match expression.

In terms of program execution, the error function can never actually be called, since it is impossible to construct any argument e to the function. Therefore, any branch of a program which has a call to the error function must be unreachable. Nevertheless, the error function can end up being useful in filling in those branches of the program, in such a way that the overall program still type-checks.

Coq also uses the Curry-Howard correspondence for logic, where a proposition is treated as a type, whose elements are proofs of the proposition. Under this correspondence, the prod type corresponds to conjunction of propositions $P \land Q$; the sum type corresponds to disjunction of propositions $P \lor Q$; and the Empty_type type corresponds to the false proposition $\bot$. And then the first function corresponds to a proof that $P \land Q \rightarrow P$ is a tautology; the case function corresponds to a proof of $P \lor Q \rightarrow [(P \rightarrow R) \rightarrow [(Q \rightarrow R) \rightarrow R]]$; and the error function corresponds to a proof of $\bot \rightarrow P$.