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?

  • 1
    $\begingroup$ IMO the arguments exposed in the linked post are good ones. The principle encodes the meaning of inconsistency in classical and intuitionistic logic: an inconsistency trivialize the full system. $\endgroup$ Commented Jun 28, 2023 at 17:35
  • $\begingroup$ Possibly helpful: How or why does intutionistic logic proof negations from within the theory, constructively?. My answer there discusses a semantics of $\bot$ in which $\bot$ is “the type of a program that doesn't return a value, perhaps because it threw a fatal exception that terminated the computation, or because it went into an infinite loop and never completed.” It doesn't address $\bot\to A$ specifically though. $\endgroup$
    – MJD
    Commented Jun 28, 2023 at 18:03
  • $\begingroup$ @MauroALLEGRANZA “an inconsistency trivialize[s] the whole system” is just a meta-statement of the principle in question. $\endgroup$
    – PW_246
    Commented Jun 28, 2023 at 18:17
  • $\begingroup$ I just remembered that I asked something very similar a few years back: Can the principle of explosion be removed from constructive logic?. I think the answers here are deeper, but the other thread might also be interesting. $\endgroup$
    – MJD
    Commented Jun 29, 2023 at 15:35
  • 1
    $\begingroup$ Yeah, this is tricky since intuitionistic logic isn't designed from model-theoretic semantics unlike classical logic. What about an empirical argument as follows: a non-terminating program (which corresponds to a proof of $\bot$) in programming languages that uses some variant of typed lambda calculus (such as Haskell/ML etc.) has the type of $\forall A: Type. A$, which is explosive? $\endgroup$
    – Poscat
    Commented Mar 8 at 0:54

3 Answers 3


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.

  • 2
    $\begingroup$ Either way, thanks for your answer. This one is the closest to making perfect sense. $\endgroup$
    – PW_246
    Commented Jun 29, 2023 at 0:01
  • 2
    $\begingroup$ +1 - very very interesting; much more than the (IMO convoluted) MLTT's "foundations", I've found illuminating the "practical" PAML example regarding the procedure to produce from the inconsistency $0=1$ all arithmetical formulas. This is exactly what "explosion" means! $\endgroup$ Commented Jun 29, 2023 at 7:37
  • 2
    $\begingroup$ My appreciation (for what is worth...) of your argument relies also on the support it gives to the "basic insight" of ancient logicians. In the language of Aristotle's logic, a "basic" contradiction is "to assert that an object A is B and at the same time not-B". See Met, Bk Gamma, 1007b 18-21: "Further, if all contradictory propositions were true at the same time in respect to the same thing, then clearly everything will be one. For a trireme, a wall, and a man would then be the same." This is exactly what your "procedure" shows.... $\endgroup$ Commented Jun 29, 2023 at 7:54
  • 3
    $\begingroup$ @PW_246: You don't need to interpret $\bot$ as $0=1$ everywhere - although you can interpret it as $0=1$ in type theory, or in Heyting arithmetic. Other choices are available in other theories, e.g. $\forall x. \forall y. x\in y$ works in all common set theories formulated in FOL without equality. In fact, any theory over a finite language (even propositional) contains an explicit explosive formula. $\endgroup$
    – Z. A. K.
    Commented Jun 29, 2023 at 11:39
  • 1
    $\begingroup$ @MauroALLEGRANZA: Thanks so much. I've added some signposting, to make sure that people will find the section about FOL and HA even if they do not go through the type theory section first. $\endgroup$
    – Z. A. K.
    Commented Jun 29, 2023 at 11:43

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.

  • $\begingroup$ I found this answer enlightening. Thanks very much. $\endgroup$
    – MJD
    Commented Jun 29, 2023 at 14:00
  • $\begingroup$ This is convincing, but I don’t see how one could possibly construct an empty disjunction using the formation rules for wffs in any logic. As far as I know, a disjunction is of two wffs, and “nothing” isn’t a wff. Still, I’m seeing where you’re coming from. $\endgroup$
    – PW_246
    Commented Jun 29, 2023 at 15:12
  • 5
    $\begingroup$ @PW_246: Absolutely, it depends on what primitives you put into the logic. If the only disjunction you include is binary, then indeed, you can’t construct the empty one from that. My point is that it’s also natural to give rules for general finitary disjunction directly, and when you do that, you see that the rules for false arise as the nullary case of the scheme. You certainly still have the choice of which cases of the scheme to put into your logic. $\endgroup$ Commented Jun 29, 2023 at 15:21
  • $\begingroup$ This is a very convincing argument, but the question becomes how to justify encoding negation as $ \rightarrow \bot$ $\endgroup$
    – Poscat
    Commented Mar 7 at 5:15

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

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

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

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$.

  • 3
    $\begingroup$ I’ll be honest, this notation makes almost no sense to me. $\endgroup$
    – PW_246
    Commented Jun 28, 2023 at 18:26

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .