$\mathbb{N}$ in intensional MLTT with judgmentally commutative $+$ and $\times$

Is there a way to implement natural numbers in intensional Martin-Löf type theory so that addition and multiplication is judgmentally commutative?

• I'm glad you are asking all those questions. I recall that, a couple of years ago, when I tried to get into dependent type theories, I found it hard to find what had been tried, what had been proven. Like many active areas of research, that field lacks an up-to-date summary of the state of the art. Mar 21 '21 at 12:37
• Yes, just throw in those judgemental equalities. It's consistent. Mar 22 '21 at 7:16
• @AndrejBauer what if I don't want to change the equality checking algorithm?
– user61651
Mar 22 '21 at 7:29
• But you must change it (if you want it to be complete) because you are introducing new judgemental equalities. Mar 22 '21 at 7:30
• No I meant that I want a type $T$ with two judgmentally commutative binary operations on it such that externally we can prove there is a bijection from the set of closed terms of $T$ to the usual natural numbers respecting the operations. I don't want to introduce any new rules to type theory.
– user61651
Mar 22 '21 at 7:48

This is impossible.

1. Suppose that we have such a type $$T$$, with an implementation of addition $$\mathit{add} : T \to T \to T$$, which is judgementally commutative.
2. Because MLTT is strongly normalising, we know that we can put $$\mathit{add}$$ in $$\beta$$-normal, $$\eta$$-long form.
3. Now suppose that we have two variables $$x, y$$ of type $$T$$.
4. Now consider the terms $$\mathit{add}\,x\,y$$ and $$\mathit{add}\,y\,x$$.
5. Substituting $$x$$ and $$y$$ for the formal parameters of $$\mathit{add}$$ will not create any new $$\beta$$-reducible expressions, because $$x$$ and $$y$$ are neutral terms.
6. Now, $$\eta$$-expand the occurences of $$x$$ and $$y$$ as demanded by the definition of $$T$$.
7. Now, the resulting terms will be identical except that we've permuted the occurences of $$x$$ and $$y$$.
8. Recall that judgemental equality for $$\beta$$-normal, $$\eta$$-long terms is just $$\alpha$$-equivalence.
9. Since we assumed $$\mathit{add}\,x\,y$$ and $$\mathit{add}\,y\,x$$ were assumed to be judgementally equal, this means that the normal forms for these two terms are $$\alpha$$-equivalent.
10. Since anywhere that $$x$$ occurs in the normal form for $$\mathit{add}\,x\,y$$, a $$y$$ occurs in the corresponding position of the normal form for $$\mathit{add}\,y\,x$$, the only way that these two terms can be $$\alpha$$-equivalent is if neither $$x$$ nor $$y$$ occurs in the term.
11. This means that $$\mathit{add}\,x\,y$$ and $$\mathit{add}\,y\,x$$ do not use their arguments!
12. As a result, we can conclude that $$\mathit{add}\,1\,1$$ and $$\mathit{add}\,0\,0$$ are also judgementally equal.
13. Therefore $$T$$ cannot be the natural numbers, since $$2$$ and $$0$$ must not be judgementally equal.
• Could you explain step 9 in more detail?
– user61651
Mar 22 '21 at 14:44
• @einzwein How's that? Mar 22 '21 at 15:07
• It seems that I've given pretty much the same answer for another question. Mar 23 '21 at 10:28

CoqMT (Coq Modulo Theory) was an extension of the Coq proof assistant that allows one to parametrize a development with a decidable first-order theory T. Since equality on natural number expressions with addition and multiplication is decidable, this would be a valid application of CoqMT. Unfortunately, the implementation has not been updated in over 10 years.