How do we know $\neg \neg LEM$ isn't provable in MLTT?

Question

I've been trying (fruitlessly) to prove something which I now know is not provable. Take the following definitions: $$LEM \equiv \prod_{A : Type} \neg A \vee A$$ $$DNE \equiv \prod_{A : Type} \neg \neg A \to A$$ $$C(x) \equiv DNE \to x$$ I wanted to prove $\prod_{A : Type} C(A) \to \neg \neg A$. In trying to prove it the key thing to prove seemed to be $\neg \neg DNE$. I couldn't figure out how to prove this however. I thought it must be provabale however. Note that the above would be logically equivalent (implication goes both ways) to $\neg \neg DNE$ because the formula trivially implies it.

But this simple formula proved tricky. It feels like $\neg \neg DNE$ should hold because $DNE$ is consistent with MLTT. At least I had it in my mind that it already held but I couldn't seem to find a prove of it. Finally I started searching. I knew that $\neg \neg LEM$ was equivalent and found this: https://ncatlab.org/nlab/show/excluded+middle#DoubleNegatedPEM

This states that $\neg \neg LEM$ is not provable. This is the same as saying that $\neg LEM$ is consistent, at least in MLTT and other such theories. I'm certainly aware that there exist statements for which both the statement and its negation are equivalent but I hadn't realized that $LEM$ and $DNE$ were examples of this in MLTT. I'm kind of baffled that $\neg \neg \neg A \to \neg A$ holds but $\neg DNE$ is still consistent. That's a subtle point about quantifier placement that I must of missed last time I thought about this sort of thing.

Normally in logic when we want to show that something isn't provable we either show that a property that is preserved by all the inference rules (and holds for all axioms) is false for the given statement or we directly find a model for the logic and show that the given statement is false in the model. The only models I know for constructive logics are fairly complicated. For propositional logic we have Heyting algebra but the quantifier here leaves us no hope of using that. I vaguely recall that it is possible to extend these algebras to the quantifier case by doing something like taking the least upper bound or greatest lower bound of a set of instances of the algebra generated by substituting constants in the set being quantified over into the formula. I don't remember exactly how this works nor am I really clear that I could extend a result from first order constrictive logic (the logic of constructive set theory).

How do we know this? Do we have a simple enough model that would explain this? Do we just know from trying to prove it that we get stuck? After trying to prove it myself I feel intuitively that we'll always get stuck and I can explain it more or less as "you have a very limited number of ways to dig down and after digging down, you get stuck really quickly" but that's quite informal. Is there a meaty formal explanation of why this isn't provable?

Answer 1

The task here is indeed to find a model of MLTT in which $\neg LEM$ holds (and so $\neg\neg\neg LEM$ holds as well). Realizability models have this feature, for instance; see also this. Here, MLTT functions are interpreted with codes of computable recursive functions, so the usual uncomputable functions, e.g. halting oracles, cause $LEM$ to fail.

If you define $LEM$ as ranging over all types, and not just types which are propositional (i.e. have at most one inhabitant up to propositional equality), then it is also the case that $LEM$ is inconsistent with the univalence axiom of homotopy type theory, so this version of $LEM$ is also refuted by any model which can interpret the univalence axiom. Such are the simplicial set and cubical set models.

$LEM$ is also inconsistent with parametricity, so models validating parametricity also refute $LEM$. I think formally these are considerably simpler than univalent or realizability models; see for example the reflexive graph model. Intuitively, this works by noticing that MLTT does not allow inspecting the structure of types, so any function with type $\prod_{A : Type} A \rightarrow A$ must be the identity function. However, $LEM$ allows one to branch on whether two types are equal, allowing a function with the above type which is not the identity function on all types, e.g. negates Boolean inputs.