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$ Mar 21 '21 at 12:37
  • $\begingroup$ Yes, just throw in those judgemental equalities. It's consistent. $\endgroup$ Mar 22 '21 at 7:16
  • $\begingroup$ @AndrejBauer what if I don't want to change the equality checking algorithm? $\endgroup$
    – user61651
    Mar 22 '21 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$ Mar 22 '21 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
    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.
  • $\begingroup$ Could you explain step 9 in more detail? $\endgroup$
    – user61651
    Mar 22 '21 at 14:44
  • $\begingroup$ @einzwein How's that? $\endgroup$ Mar 22 '21 at 15:07
  • 1
    $\begingroup$ It seems that I've given pretty much the same answer for another question. $\endgroup$ 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.


Your Answer

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