The laugh-hospital of constructive mathematics

In Raymond Smullyan’s story there was a planet on which the concept of humor was unknown and laughter was treated as a disease. Those who laughed were sent to live in laugh-hospitals, away from normal people. As time passed ever more people contracted laughter and the laugh-hospitals grew into whole laugh-communities, until the few remaining normal people pretended to understand humor just so that they could join the rest. What if constructive models are like the laugh-hospitals? What if not understanding constructivism is like not having a sense of humor?

This is a fun talk. It’s a defense of constructive mathematics, which is what mathematics becomes when you reject the law of the excluded middle (henceforth LEM), which is the claim that “φ∨¬φ” is a tautology. Here’s a link to the paper corresponding to the talk (from which the starting quote comes).

Some highlights:

• The rejection of LEM is not the same as the claim that there are some propositions that are neither true nor false. That is, denying that φ∨¬φ is a tautology is not the same as saying that there is some proposition φ for which φ∧¬φ. This second claim can actually be proven to be false in constructive mathematics.
• Both the law of double negation (which is the claim that ¬¬φ implies φ) and the axiom of choice imply LEM. So to deny LEM, one must also deny the law of double negation and the axiom of choice.
• In constructive math, proof by negation is valid, but not proof by contradiction. Proof by negation is the argument structure “Suppose φ, (argument reaching contradiction), therefore ¬φ.” Proof by contradiction is the argument structure “Suppose ¬φ, (argument reaching contradiction), therefore φ.”
  • This might seem strange; can’t you just substitute each φ in the first argument for ¬φ to get the second argument? The reason you can’t is that the second argument involves removing a negation, while the first involves introducing one. Using proof by negation and starting with ¬φ, we get ¬¬φ, and of course to a constructivist this is not equivalent to φ.
• LEM is equivalent to the claim that all subsets of a finite set must be finite (you can prove LEM from this claim, and can prove this claim from LEM).
• In particular, in the Brouwer–Heyting–Kolmogorov interpretation of constructive mathematics one cannot prove that “all subsets of the set {0, 1} are finite”.
• φ is a classical tautology if and only if ¬¬φ is an intuitionistic tautology. (Not in this talk, but a fun one nonetheless.)

So how do we make sense of all this? Well, there are different ways of understanding propositions in intuitionistic logic. One simple one is to reinterpret the assertion that P as meaning ‘P is proven’ rather than ‘P is true’. In this interpretation, the law of the excluded middle in this interpretation is something like ‘every proposition is either provably true or provably false.’ This is the ambitious claim of Hilbert’s program that we now know to be false; for instance, Gödel’s sentence is a counterexample to the law of the excluded middle. We cannot prove that Gödel’s sentence is true, and we cannot prove that it is false. And note that Gödel’s sentence is true! Just not provably so. As for double negation, ¬¬φ means “any proof that φ entails a contradiction, would itself entail a contradiction”, and this is clearly not equivalent to φ (proving that proofs of ¬φ inevitably lead to contradiction is not the same as proving that φ). 

In some interpretations of intuitionistic logic, the interpretation of a proposition is literally tied to its current epistemic status (whether we’ve proven it one way or another yet). So in these interpretations, P=NP is a counterexample to the law of the excluded middle (not because it’s neither true nor false, nor because it’s impossible to prove, but because we don’t currently have such a proof). 

As a final note, let’s just quickly show that we can prove the law of the excluded middle from lambda calculus. We’ll formalize the law of the excluded middle as a function that takes in a proposition p and returns the function corresponding to p∨¬p. If we can show that on each possible value of the input proposition p (either T or F), the function returns T, then we have proven LEM.

I’m not totally sure about the relationship between lambda calculus and intuitionistic logic, so this apparent proof of the law of the excluded middle is curious to me.