3
$\begingroup$

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?

$\endgroup$
11
  • 1
    $\begingroup$ The Principle of Explosion is argued from the Principle of Bivalence: $\neg(A\wedge \neg A)$, rather than the Principle of Excluded Middle: $A\vee\neg A$. $\endgroup$ – Graham Kemp Mar 18 '18 at 7:16
  • $\begingroup$ @GrahamKemp Perhaps part of the confusion is that those are classically equivalent. $\endgroup$ – spaceisdarkgreen Mar 18 '18 at 7:18
  • $\begingroup$ Indeed, but not intuitionistically. @spaceisdarkgreen $\endgroup$ – Graham Kemp Mar 18 '18 at 7:20
  • $\begingroup$ Right, they're equivalent in classical logic but not in intuitionistic logic, that's all true and helpful. So what I said, "in classical logic the principle of explosion is a consequence of the law of the excluded middle", is correct. But the question is about the justification for the axioms of intuitionistic logic. The non-equivalence of these things under the new axioms might be a piece of the puzzle, but seems not to lead me directly to its answer. $\endgroup$ – Nathaniel Mar 18 '18 at 7:36
  • 1
    $\begingroup$ @Nathaniel And on the philosophical end, just cause within minimal logic, LEM does imply explosion wouldn't mean that LEM is the philosophical justification for explosion. There could be separate justifications, with the one for explosion being intuitionistic and the one for LEM classical. But then I think this is basically what you're after. My non-authoritative two cents on this is that it boils down to the fact that intuitionism basically accepts vacuous truth. Thus $\bot \to A$ which says "If I have a proof of something that I have no proof of, then I have a proof of A" is true. $\endgroup$ – spaceisdarkgreen Mar 18 '18 at 8:16
3
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ Thanks, this is quite interesting. Do you know if this was the historical motivation for intuitionistic logic, or if it came later? $\endgroup$ – Nathaniel Mar 18 '18 at 8:37
  • $\begingroup$ Brouwer is generally viewed as the founder of Intuitionism. I haven't read Brouwer's work directly, but from what I've read about it, his view was one of "mental constructions". That is, "mental constructions" would be what he meant by "proof" in the BHK interpretation hence "Intuitionism". Brouwer did not explicitly articulate the BHK interpretation (at least not initially). His student Heyting did and independently Kolmogorov. My impression is few of the modern users of Intuitionistic logic are Brouwer-style Intuitionists philosophically. $\endgroup$ – Derek Elkins left SE Mar 18 '18 at 8:53

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.