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

  • 3
    $\begingroup$ 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. $\endgroup$ Commented Mar 21, 2021 at 12:37
  • $\begingroup$ Yes, just throw in those judgemental equalities. It's consistent. $\endgroup$ Commented Mar 22, 2021 at 7:16
  • $\begingroup$ @AndrejBauer what if I don't want to change the equality checking algorithm? $\endgroup$
    – user61651
    Commented Mar 22, 2021 at 7:29
  • 1
    $\begingroup$ But you must change it (if you want it to be complete) because you are introducing new judgemental equalities. $\endgroup$ Commented Mar 22, 2021 at 7:30
  • $\begingroup$ 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. $\endgroup$
    – user61651
    Commented Mar 22, 2021 at 7:48

2 Answers 2


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.
  • $\begingroup$ Could you explain step 9 in more detail? $\endgroup$
    – user61651
    Commented Mar 22, 2021 at 14:44
  • $\begingroup$ @einzwein How's that? $\endgroup$ Commented Mar 22, 2021 at 15:07
  • 1
    $\begingroup$ It seems that I've given pretty much the same answer for another question. $\endgroup$ Commented Mar 23, 2021 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.