4
$\begingroup$

In laying down the equality rules in Martin-Löf type theory, e.g., for the type $\mathsf{N}$ of natural numbers, there seems to be an implicit assumption that any natural number is either $0$ or $S(a)$ for some $a\in\mathsf{N}$; in other words, only the so-called 'canonical' elements of the type $\mathsf{N}$ are given rules for their equality. Of course, we do know, from our background understanding of natural numbers and their inductive construction (as the smallest set such that ...) that they are either $0$ or $S(a)$ for some $a$, but I wonder how this is granted by the rules of Martin-Löf type theory. The introduction rules only say that $0\in \mathsf{N}$ and that if $a\in \mathsf{N}$ then $S(a)\in \mathsf{N}$, but I don't see how this guarantees there's no other element in $\mathsf{N}$.

Is the assumption that any natural number is of one of its two canonical forms only implicitly assumed or is there a way we can derive it from the deductive rules that characterize $\mathsf{N}$? Is the fact that we're not laying down any other rule for introduction itself a way of carrying the idea? (A similar question applies to other types.)

$\endgroup$
4
  • 1
    $\begingroup$ In type theory, it is usually understood—not just for the natural-number type—that any terms constructed using the construction rules, and only terms so constructed, belong to the type. $\endgroup$
    – LSpice
    Jan 10 at 17:24
  • 5
    $\begingroup$ @LSpice: Nope, there is no such assumption in type theory. Do you have a reference? $\endgroup$ Jan 10 at 20:49
  • 2
    $\begingroup$ @AndrejBauer, no reference other than what I have mentioned in a comment below: informal notes that say "terms constructed in this way are of type $\mathsf N$", and less informal notes that say "terms constructed in this way are of type $\mathsf N$, and no other terms are of this type." I did not mean to make a statement about the formal theory, just the sort of thing that one might encounter (or at least, I did) in introductory notes. (That's why I referred, obtusely, to an understanding (often elided in notes) rather than an assumption.) $\endgroup$
    – LSpice
    Jan 10 at 21:25
  • 4
    $\begingroup$ Yes, if you read old books on logic, then they do indeed describe inductive construtions as saying "things constructed this was an no other way". Such statements do not survive scrutiny and are just handwaving explanations. They may serve a pedagogical purpose, but they also do a good deal of harm, as the present discussion confirms. $\endgroup$ Jan 10 at 21:28

4 Answers 4

8
$\begingroup$

There is no such implicit assumption at all. You are missing one rule for natural numbers, namely the induction principle. The rules for natural numbers are: $$\frac{}{\vdash \mathbb{N} \; \mathsf{type}} \qquad \frac{}{\vdash 0 : \mathbb{N}} \qquad \frac{\vdash t : \mathbb{N}}{\vdash \mathsf{S}(t) : \mathbb{N}} \\[4ex] \frac{n {:} \mathbb{N} \vdash P(n) \;\mathsf{type} \quad \vdash t : P(0) \quad n {:} \mathbb{N}, y {:} P(n) \vdash f : P(\mathsf{S}(n)) \quad \vdash e : \mathbb{N}}{\vdash \mathsf{rec}(t, (n \, y . f), e) : P(e)} $$ The last rule is the induction principle, stated type theoretically. The technical details are not too important, but briefly, $t$ is the base case and $f$ is the induction step. There are also further equations governing $\mathsf{rec}$, but they are not important for this discussion.

There is no mysterious, implicit, cultural, meta-level or other kind of hidden anything. The above rules are all there is to say about $\mathbb{N}$.

Now, using the induction principle we can derive an inhabitant of the type \begin{equation} \textstyle\prod (n : \mathbb{N}) \,.\, \left(\mathsf{Id}(n, 0) + \sum (m : \mathbb{N}) \,.\, \mathsf{Id}(n, \mathsf{S}(m)\right) \tag{1} \end{equation} This type says "every natural number is either 0 or a successor". I will leave this as an exercise, it's not hard.

A word of warning: sometimes people think of types as collections of terms (expressions), especially when their background is programming and computer science. From a mathematical point this is a bad idea, or at least as bad as thinking that a function is a symbolic expression (historically, this was the accepted understanding, and is quite natural for pre-college students), or that a surface is made of set-theoretic expressions denoting its points.

Anyhow, when people do think of type theory as a purely syntactic entity, then they might prove a meta-theorem that says something like "every closed term of type $\mathbb{N}$ is judgementally equal to one of the form $S(S(\cdots S(0)))$". Such theorems have their place and are important, but they do not say that every element of $\mathbb{N}$ is either 0 or a successor. Expressions are not the inhabitants of a type, they are just representations of some of the inhabitants. Depending on a model, there may be others.

In your question you state that we "know" that every natural number is zero or a successor because we construct $\mathbb{N}$ as "the smallest set such ..." True, taking such a smallest set is a method of ensuring that the induction principle will be validated - and the induction principle then implies the statement "every number is $0$ or a successor".

But taking "the smallest set such ..." is not a method of insuring that the set will only contain elements of the form $S(S(...S(0)))$! For if you carry out the construction in a non-standard model of set theory, you will get non-standard natural numbers which are not denoted by any expression of the form $S(S(...S(0)))$. And in a Boolean topos such as $\mathsf{Set}^2$, the construction will produce what we would view as $\mathbb{N} \times \mathbb{N}$. It is still true inside the model that "every number is zero or a successor" – and that corresponds precisely to the fact that inside type theory (1) is inhabited.

I am not sure all of this is making things clearer, but I hope it at least points to some possible misunderstandings.

$\endgroup$
4
  • 1
    $\begingroup$ In the last rule, the one for rec, I think $ny$ is a typo. $\endgroup$ Jan 10 at 21:27
  • 1
    $\begingroup$ Oh no, that's a binder. It binds $n$ and $y$ simulatneously, so they do not roam freely when they shouldn't. We lack good standard notation for such things. $\endgroup$ Jan 10 at 21:30
  • 1
    $\begingroup$ Oh, so the dot after $ny$ functions like a $\lambda$ or rather a pair of $\lambda$'s, but understood in a dependent-type sense where the type of $y$ depends on $n$. Since some people still use dots for simple grouping, I"d encourage you to invent another notation. (By the way, I'm not a fan of $\lambda$ either, since most mathematicians would not write $\lambda x t$ but rather $x\mapsto t$.) $\endgroup$ Jan 10 at 21:38
  • $\begingroup$ I already invented another notation, and implemented it in an experimental proof assistant that support abstraction as a primitive operation, it's $\{n\}\{y\} f$. I am not sure it's any good though, it uses up $\{$ and $\}$. $\endgroup$ Jan 10 at 22:03
10
$\begingroup$

Adding a little to other good answers, especially Andrej’s: Nothing in this discussion is specific to Martin-Löf type theory. All these phenomena show up in other foundational systems, like ZFC or PA — and perhaps looking at them there may clarify them, for some readers.

In ZFC, for instance, you can of course prove “Every element of $\mathbb{N}$ is either zero or a successor” — this follows directly from induction for $\mathbb{N}$, and is often mentioned as part of the intuitive motivation for induction. But consider the number $\chi_{CH}$, defined to be 1 if the continuum hypothesis holds, and 0 if CH fails. Since CH is independent of ZFC, we know ZFC can’t prove either that $\chi_{CH} = 1$, or $\chi_{CH} = 0$. There’s no contradiction here, but it shows we have to distinguish between:

  1. ZFC proves “every element of $\mathbb{N}$ is either zero or a successor”;

  2. for every ZFC-definable element of $\mathbb{N}$, either ZFC proves it is 0, or ZFC proves it is a successor.

We’ve seen that for ZFC, (1) holds, quite easily and (2) fails, quite non-trivially. Similarly, with type theory, we can distinguish:

  1. MLTT proves “every element of $\mathbb{N}$ is either zero or a successor”;

  2. for every MLTT-term of type $\mathbb{N}$, either it is [provably or judgementally] equal to 0, or to a successor.

There are two differences in the phrasing: MLTT has a much richer term language, so we can say “term” instead of “definable element”; and MLTT has several different notions roughly corresponding to provable-equality in ZFC, each giving a different variant of (2). But again, (1) and the variants of (2) are very different: (1) holds, quite easily (again directly provable from the induction principle of $\mathbb{N}$); while (2) may hold or fail depending which variant of it and which variant of MLTT you consider, but in any case it is a quite non-trivial property, and very distinct from (1).

$\endgroup$
0
2
$\begingroup$

First, we should pin down that we're talking about closed terms with natural number type, that is, terms without free variables. A free variable with type $\mathsf{N}$ is clearly not of the form $0$ or $S(n)$.

A type theory has the canonicity property if all closed terms with type $\mathsf{N}$ can be computed to a numeral, i.e. a finite successor of $0$.

This property is not an assumption. It is a provable property for most commonly used type theories, which follows from the specification of the theory. It is not enough though to only look at the rules for natural numbers, we have to consider all rules of a type theory simultaneously, because (intuitively) it is possible to construct numbers from various other types. For example, if we add the law of excluded middle as an axiom, that makes canonicity fail, since it introduces non-constructive definitions which cannot be computed to numerals.

Canonicity proofs are moderately complex for interesting type theories. The easiest way is to do "proof-relevant logical predicates", or "Artin gluing". Sterling - Algebraic Type Theory and Universe Hierarchies is a fairly accessible and detailed exposition. In a nutshell, we construct the following by induction on the syntax of a theory:

  • For each typing context, a family of sets indexed by parallel substitutions targeting the context (a "proof-relevant predicate").
  • For each type in a context, a family of sets indexed by terms of the type.
  • For each parallel substitution, a function which witnesses that the substitution preserves predicates.
  • For each term, again a function witnessing preservation of predicates.

Concretely for the $\mathsf{N}$ type, we may pick the predicate which says that a given term is a numeral. Then, from the above induction, and also from the fact that the predicate corresponding to the empty context is trivially true, we get that every closed term with type $\mathsf{N}$ must be a numeral.

$\endgroup$
1
  • $\begingroup$ I think one thing that may confuse @qk11—it certainly confused me—is that, while a suitably rigorous presentation will surely allow one to prove canonicity, there is a tendency in informal presentations to say something like "$N$ is of type $\mathsf N$ if $N = 0$ or $N = S(n)$ for some $n$ of type $\mathsf N$", from which alone it is not possible to prove that there are no other terms of type $\mathsf N$. $\endgroup$
    – LSpice
    Jan 10 at 20:39
2
$\begingroup$

Your question can be understood in different ways. András has answered one way, here is another way.

It is a consequence of the $\mathbb{N}$-elimination rule that, to define any function $f:\mathbb{N}\to A$, it is enough to define it for $0$, and for $s(a)$, where $a$ is an arbitrary inhabitant of $\mathbb{N}$. So we can say: "to define $f(x)$, we can suppose that $x$ is either $0$ or $s(a)$".

The classical recursion principle is also a consequence of the $\mathbb{N}$-elimination rule: to prove a property for all $x:\mathbb{N}$, it is enough to prove it for $0$ and for $s(a)$, where $a$ is an arbitrary inhabitant of $\mathbb{N}$.

Using this principle you can prove the property: $\Pi_{x:\mathbb{N}} (x=0) + (\Sigma_{a:\mathbb{N}} (x=s(a)))$.

$\endgroup$
4
  • 1
    $\begingroup$ Just to connect with my answer, the "$\mathbb{N}$-elimination rule" is what is also know as "induction principle for $\mathbb{N}$". $\endgroup$ Jan 10 at 21:30
  • $\begingroup$ @AndrejBauer's answer. $\endgroup$
    – LSpice
    Jan 10 at 21:30
  • 1
    $\begingroup$ It's a bit like path induction for identity types, where it suffices to prove things for refl. That doesn't say every term is refl! $\endgroup$ Jan 10 at 21:46
  • 1
    $\begingroup$ @LSpice : fixed, thanks ! $\endgroup$
    – L. Garde
    Jan 12 at 21:11

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.