Interpretation of implication in intuitionistic logic

Question

I understand that in intuitionistic logic, a statement $A \to B$ is meant to be interpreted as "from a proof of $A$ we can construct a proof of $B$."

However, I'm confused by the following axiom:

$$\neg A \to (A\to B).$$

This seems to mean "from a proof of $\neg A$ we can construct a proof that if we were given a proof of $A$ we could construct a proof of $B$."

But why should that be true? What is the justification for including this axiom?

I guess an argument would from the principle of explosion: "if we have proven $\neg A$ then the only possible way we can also be given a proof of $A$ is if our system is inconsistent, and therefore any $B$ can be proven." But this seems somehow odd to me. I'm under the impression (perhaps wrongly?) that in classical logic the principle of explosion is a consequence of the law of the excluded middle, so if we're rejecting the LEM, why would we want to keep the principle of explosion?

I know that minimal logic exists, and from what I can tell it seems to essentially be intuitionistic logic without this axiom, so it seems to possible to reject both the LEM and the principle of explosion. I'm also aware that there are some practical proofs that work in intuitionistic logic but not in minimal logic. However my question is more on the philosophical side: for the intuitionists, what was the justification for the $\neg A \to (A\to B)$ axiom?

Answer 1

"From a proof of $A$, we can construct a proof of $B$" makes it sound like like "$A$ implies $B$ is constructively 'true' if having a proof for $A$ implies we can construct a proof for $B$". This makes it sound like the constructive notion of implication reflects the meta-logical notion of implication in some way.

In the BHK interpretation, a proof of $A\implies B$ isn't the fact that you can build a proof of $B$ given a proof of $A$, it is a function. We don't say "$A\implies B$ is true", we have some proof object that witnesses $A\implies B$. For example, a proof object representing $A\land B\implies A$ is the function $\pi_1$ defined as $\pi_1(a,b)=a$. As another aspect that I should make clear is the "proofs" talked about in the BHK semantics are not formal proofs. They are mathematical objects. You hear terms like "proof object", "evidence", "witness". The point is that the thing which the BHK interpretation refers to as a "proof" is not a fully defined thing (especially as we leverage categorical semantics). A formal proof, or derivation, on the other hand, is some typically tree-like structure involving applications of inference rules and looks something like this, say, and is fully specified.

So, via the BHK interpretation, the Principle of Explosion, i.e. $\bot\implies A$ is straightforwardly demonstrated for various more fleshed out notions of "proof". For example, using set-theoretic functions it is witnessed by the empty function. For a realizability approach and, specifically using $\mu$-recursive functions as the notion of "computable function", it is witnessed by the totally undefined (partial) ($\mu$-recursive) function. From a more pragmatic computational perspective, we might say it is witnessed by a program that is free to do just about anything because it will never be called. Often looping forever or an abort operation is used. In a categorical approach, it is witnessed by the mediating arrow of the initial object (assuming there is an initial object). Different interpretations for the notion of "proof" lead to different flavors of constructivism. If your preferred notion of "proof" can be organized into a category that lacks an initial object, you may decide to reject the Principle of Explosion.

The philosophical justification for the Principle of Explosion is then simply that in many ways of understanding the BHK notion of "proof", there simply is a proof object that corresponds to it.