6
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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.) $\endgroup$ – chi Apr 21 at 0:06
8
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Very helpful answer! Thanks. This gives several helpful models to think about. $\endgroup$ – Jake Apr 23 at 4:33
  • $\begingroup$ I'll have to dig into the specifics of realizability but it seems clear how this would work for Heyting Arithmetic where quantification can only occur over natural numbers. It would be helpful to see realizability models in the context of system F where I think everything I'm concerned with here would still apply but certainly for the calculus of constructions case. I'll read both the paper on realizability models and reflexive graph models. Handling quantification over types seems quite tricky. $\endgroup$ – Jake Apr 23 at 4:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.