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

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?

• I don't have a formal argument, but I think the intuition is that there should be a model where there is some $f:\mathbb N \to\mathbb N$ such that $(\forall n. fn=0) \lor \lnot(\forall n. fn=0)$ does not hold. That property is undecidable, so we can't prove nor refute it. In other words, undecidable properties should prove $\lnot LEM$ consistent. (I don't know enough about models of MLTT to be really sure, though. Mine is only a hunch.) – chi Apr 21 '19 at 0:06

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.