2
$\begingroup$

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

$\endgroup$
5
  • 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 at 12:37
  • $\begingroup$ Yes, just throw in those judgemental equalities. It's consistent. $\endgroup$ Mar 22 at 7:16
  • $\begingroup$ @AndrejBauer what if I don't want to change the equality checking algorithm? $\endgroup$
    – user61651
    Mar 22 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 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 at 7:48
3
$\begingroup$

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

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.

$\endgroup$

Your Answer

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