Why in Martin-Löf type theory any natural number is assumed to be either $0$ or $S(a)$ for some $a\in\mathsf{N}$?

Question

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.)

Answer 1

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.

Answer 2

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).

Answer 3

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.

Answer 4

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)))$.