There's normally a tight connection between programming and proving: this is known as "Propositions as Types." I found one aspect of the correspondence troubling, went down a rabbit hole, and came back less troubled.
Our most popular logical systems all include exfalso, a.k.a. The Principle of Explosion which is the principle that a contradiction implies anything at all. That is, forall B, if false then B.Which seems really surprising on the face of it: where did B come from?! I'll share my exploration of this question and an attempt at an answer.
Warning: There's nothing practical in this post.
Exfalso is easily derived in classical logic, the logic we're taught in school if we learn any logic at all. In classical logic, A -> B means (not A) or B. In classical logic, this is true by definition because if false then B means (not false) or B, which is just true regardless of what B is.
What was unclear to me was where exfalso comes from in the logic that corresponds to computation* (intuitionistic logic). It's almost a secret that exfalso is assumed in intuitionistic logic, without proof. But both intuitionists and our programming languages seem to quietly believe exfalso:
// exfalso in TypeScript is a function
// from a contradiction to anything at all
function exfalso<T>(contradiction: never): T {
return contradiction;
}
*Note: I'm exaggerating a bit in calling intuitionistic logic the logic of computation. It's closest to how most of our programming languages seem to work most of the time. See Linear Logic: The resource interpretation and "A Formulae-as-Types Notion of Control for aspects of computation that other logics model better._
Background on Intuitionistic Logic and Programming
From a programmer's point of view, classical logic works for booleans, but otherwise rarely has much to do with our craft. That's because classical logic assumes something we cannot compute: the law of excluded middle (or an equivalent axiom), which is forall A, A or not A (each thing we can say is either true or false).
To show why assuming the Law of Excluded Middle doesn't accurately describe computation, consider this TypeScript function:
function foo(thing: Thing): number | string {
...
}
The type signature says that this function will return either a number OR a string. But at runtime there is no such thing as an instance of number | string that is not specifically a number or a string. In both programming and intuitionistic logic, in order to construct an instance of "number or string" we must have a number or have a string.
The correspondence with computation makes intuitionistic logic really attractive (at least to me), and this logic underlies some of our most cutting-edge programming languages (Coq, Agda, Idris).
Next I'll share where exfalso comes from in intuitionistic logic, the relationship to programming, and why everything is probably OK.
Exfalso in Intuitionistic Logic and Programming
If intuitionistic logic is the logic of what is programmable, then it's pretty strange that it says that in certain situations we can get any value we like for free (exfalso).
It wasn't obvious to me from Wikipedia or The Stanford Encyclopedia of Philosophy, but exfalso is assumed by intuitionistic logic. This is in contrast to classical logic, where exfalso is derivable. So it seems intuitionists (who assume very little) intentionally committed to this surprising principle.
To try to figure out why, I looked at what early intuitionists had to say about exfalso. Note that intuitionism came before computers, so the inventors of intuitionism did not think about it as the logic of computation, but had similar interpretations:
- The logic where one judges what is constructable (Brouwer)
- The logic where one finds a method of fulfilling/realizing an intention (Heyting)
- The logic where one finds a method of solving a task (Kolmogorov)
Source: "Intuitionistic Type Theory" (Martin-Löf, 1980)
Brouwer basically said nothing about exfalso, but relied on it implicitly.
Heyting subtly qualified his view of implication to include the commitment to exfalso, selling this qualification as "adding precision":
As a matter of fact [exfalso] adds to the precision of the definition of implication. You remember that P → Q can be asserted if and only if we possess a construction which, joined to the construction of P would prove Q. Now suppose that ⊢ ¬P, that is, we have deduced a contradiction from the supposition that that P were carried out. Then, in a sense, this can be considered as a construction, which, joined to a proof of P (which cannot exist) leads to a proof of Q. I shall interpret then implication in this wider sense. (from "Intuitionism, an Introduction", Heyting)
Kolmogorov, to my ears at least, is clearer on the topic of exfalso:
As far as [exfalso] is concerned, as soon as [not A] is solved, the solution of A is impossible, and the problem of "A -> B" has no content. ... the proof that a problem is without content will always be considered as its solution.
Kolmogorov is not saying that a contradiction implies anything. Instead, he's saying that we can safely pretend it does. Morally, this feels like a significant difference to me: exfalso is imagination run wild, but saying we don't have any particular obligations in impossible situations sounds reasonable. However, in formal systems as well as programming, I have a tough time seeing what the difference would be between pretending exfalso and believing exfalso.
Take the following TypeScript example, noting that in programming contradiction can be thought of as unreachable code:
function example(bool: boolean): string {
switch (bool) {
case false:
return "false";
case true:
return "true";
default:
// unreachable
return bool;
}
}
Check out the default case. If bool is of type boolean, why does TS let us treat it as having type string?
To see what's going on, try putting your mouse over bool in the last return statement in the TypeScript playground. TypeScript reports that bool is of type never on that line. never is TypeScript's name for "contradiction." Even though booleans are not numbers, you can return bool in the default case because the type checker knows that the default case is unreachable.
To me, the choice made by TS and other programming languages here helps clarify intuitionistic logic. It's not like when a contradiction is reached a genie appears, ready to grant any wish. Instead, we have no particular obligation with regard to our return types in unreachable parts of our programs. I think this gibes with what Kolmogorov was talking about when he said "the problem has no content" in cases of contradiction. "unreachable code" ~= "problem with no content."
The Heyting and Kolmogorov quotes and interpretation of them are from van Dalen's "Kolmogorov and Brouwer on constructive implication and the Ex Falso Rule"
Top comments (2)
Enjoyed reading. Good work!
Thanks!