snippetModerate
How do we know $\neg \neg LEM$ isn't provable in MLTT?
Viewed 0 times
lemknowmlttnegprovablehowisn
Problem
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 vag
$$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 vag
Solution
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.
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.
Context
StackExchange Computer Science Q#107286, answer score: 10
Revisions (0)
No revisions yet.