[proofplan] We reduce the closed term $t$ to a normal form $u$ by normalization for the pure fragment, then use subject reduction to keep the judgment $\vdash u:\mathsf{Nat}$. The essential point is a canonical-forms analysis: a closed normal term of type $\mathsf{Nat}$ cannot be neutral, because the empty context supplies no variables and the pure signature supplies no extra closed constants. Therefore the normal form is built only from $\mathsf{zero}$ and finitely many applications of $\mathsf{succ}$, so it is a numeral. [/proofplan] [step:Fix the reduction relation and numeral notation] Let $\mathsf{Tm}$ denote the raw terms of the pure theory, considered modulo alpha-equivalence. Let $\to$ be the one-step definitional reduction relation generated by the beta-computation rules for the type formers of $\mathcal T$, including the computation rules for the natural-number eliminator. Let $\to^*$ denote the reflexive [transitive closure](/theorems/1493) of $\to$. Define the numeral map $\nu:\mathbb N_0\to\mathsf{Tm}$ by $\nu(0):=\mathsf{zero}$ and $\nu(n+1):=\mathsf{succ}(\nu(n))$. Thus $\nu(n)$ is the term denoted by $\mathsf{succ}^n(\mathsf{zero})$. [/step] [step:Normalize the closed natural-number term] By the normalization theorem for this pure intensional Martin-Lof [type theory](/page/Type%20Theory) fragment, applied to the derivable closed judgment $\vdash t:\mathsf{Nat}$, there exists a normal term $u\in\mathsf{Tm}$ such that \begin{align*} t \to^* u. \end{align*} Here "normal" means that no one-step definitional reduction applies to $u$. By subject reduction for the same reduction relation, the typing judgment is preserved along each step of $\to$, hence along $\to^*$. Therefore \begin{align*} \vdash u:\mathsf{Nat}. \end{align*} The normalization and subject-reduction results used here are standard metatheorems for the pure normalizing MLTT fragment under discussion; citing results not yet in the wiki: Normalization for pure intensional Martin-Lof type theory with natural numbers, and Subject reduction for intensional Martin-Lof type theory. [/step] [step:Classify closed normal terms of type $\mathsf{Nat}$] [claim:Closed normal natural-number terms are numerals] If $u$ is normal and $\vdash u:\mathsf{Nat}$, then there exists $n\in\mathbb N_0$ such that $u=\nu(n)$ as a raw normal form modulo alpha-equivalence. [/claim] [proof] We argue by induction on the normal-form grammar. A normal term is either an introduction form or a neutral form. At type $\mathsf{Nat}$, the introduction forms are exactly $\mathsf{zero}$ and $\mathsf{succ}(v)$, where $v$ is a normal term with $\vdash v:\mathsf{Nat}$. If $u=\mathsf{zero}$, then $u=\nu(0)$. If $u=\mathsf{succ}(v)$, then the typing rule for $\mathsf{succ}$ gives $\vdash v:\mathsf{Nat}$, and normality of $u$ implies normality of $v$. By the induction hypothesis, $v=\nu(n)$ for some $n\in\mathbb N_0$, so \begin{align*} u=\mathsf{succ}(\nu(n))=\nu(n+1). \end{align*} It remains to rule out the neutral case. A neutral term is generated from a variable, a primitive constant, or an eliminator-headed expression whose head is already neutral. In the empty context there is no variable from which a closed neutral term can begin. By the purity hypothesis, the signature contains no additional closed constants or postulates; the only primitive closed constants for natural numbers are constructors, and constructors are introduction forms rather than neutral heads. Finally, an eliminator-headed neutral term of natural-number type would require a neutral scrutinee or neutral head already present at a smaller stage of the grammar. Since no such closed neutral head exists at the base stage, induction on the neutral-term grammar gives that no closed neutral normal term exists. Thus the only possible closed normal forms of type $\mathsf{Nat}$ are $\mathsf{zero}$ and iterated successors of $\mathsf{zero}$, which proves the claim. [/proof] [guided] We prove the canonical-forms statement directly because it is the step where canonicity enters. The normal-form grammar separates terms into introduction forms and neutral forms. Introduction forms are constructors; neutral forms are terms that are stuck because their head is a variable, a primitive constant without a reduction rule, or an eliminator applied to a stuck head. For type $\mathsf{Nat}$, the introduction forms are precisely the two natural-number constructors. The first constructor gives the base numeral: \begin{align*} \mathsf{zero}=\nu(0). \end{align*} The second constructor has the form $\mathsf{succ}(v)$. If $\vdash \mathsf{succ}(v):\mathsf{Nat}$, then the typing rule for $\mathsf{succ}$ gives $\vdash v:\mathsf{Nat}$. Since $\mathsf{succ}(v)$ is normal, the subterm $v$ is also normal. Applying the same classification recursively to $v$, there is $n\in\mathbb N_0$ with $v=\nu(n)$. Therefore \begin{align*} \mathsf{succ}(v)=\mathsf{succ}(\nu(n))=\nu(n+1). \end{align*} The only remaining possibility is that a closed normal term $u$ of type $\mathsf{Nat}$ is neutral. This cannot occur in the pure empty-context theory. A neutral term must begin with a head that is already stuck. In an empty context, no variable can provide such a head. The hypothesis excluding extra closed constants and axioms removes the other possible source of a stuck closed head. Natural-number eliminators do not create a closed neutral term from nothing: an eliminator-headed neutral expression is neutral only when its scrutinee or head is already neutral. Induction on the neutral-term grammar therefore shows that no closed neutral normal term exists. Consequently every closed normal term of type $\mathsf{Nat}$ is generated by finitely many uses of $\mathsf{succ}$ starting from $\mathsf{zero}$. Equivalently, it is $\nu(n)=\mathsf{succ}^n(\mathsf{zero})$ for a unique $n\in\mathbb N_0$. [/guided] [/step] [step:Conclude that the original term reduces to a numeral] From normalization and subject reduction, we obtained a normal closed term $u$ with \begin{align*} t \to^* u \end{align*} and \begin{align*} \vdash u:\mathsf{Nat}. \end{align*} By the canonical-forms claim, there exists $n\in\mathbb N_0$ such that \begin{align*} u=\nu(n)=\mathsf{succ}^n(\mathsf{zero}). \end{align*} Substituting this equality of normal forms into the reduction sequence gives \begin{align*} t \to^* \mathsf{succ}^n(\mathsf{zero}). \end{align*} This is exactly the asserted canonicity property for closed terms of type $\mathsf{Nat}$ in the pure theory. [/step]