[proofplan] Assume, toward a contradiction, that there is a closed term $t$ of type $\mathsf{Empty}$. The standard normalization theorem for pure intensional Martin-Löf [type theory](/page/Type%20Theory) reduces $t$ to a closed normal form $u$, and subject reduction transfers the typing judgment from $t$ to $u$. We then use the canonical-forms analysis for closed normal terms: a closed normal inhabitant of an inductive type must be an introduction form, while the empty type has no introduction forms, and closed neutral terms cannot occur in the empty context. This contradiction proves that no closed term of type $\mathsf{Empty}$ exists. [/proofplan] [step:Assume a closed inhabitant of the empty type and normalize it] Let $\to$ denote the one-step computation relation of $\mathcal T$, generated by the standard beta and iota computation rules for the specified type formers, and let $\to^*$ denote its reflexive [transitive closure](/theorems/1493). Suppose, for contradiction, that there exists a term $t$ such that \begin{align*} \vdash_{\mathcal T} t : \mathsf{Empty}. \end{align*} By the normalization theorem for pure intensional Martin-Löf type theory, (citing a result not yet in the wiki: Normalization for pure intensional Martin-Löf type theory), there exists a term $u$ such that $t \to^* u$ and $u$ is normal, meaning that no term $v$ satisfies $u \to v$. Since reduction does not introduce free variables, and $t$ is typed in the empty context, the term $u$ is also closed. By subject reduction, also called preservation, (citing a result not yet in the wiki: Subject reduction for pure intensional Martin-Löf type theory), the typing judgment is preserved along $t \to^* u$. Hence \begin{align*} \vdash_{\mathcal T} u : \mathsf{Empty}. \end{align*} [guided] We begin by naming the operational relation used in the argument. Let $\to$ be the one-step computation relation of $\mathcal T$, generated by the beta and iota computation rules for natural numbers, dependent products, dependent sums, identity types, and the empty type. Let $\to^*$ be the reflexive transitive closure of $\to$. Assume, for contradiction, that $\mathsf{Empty}$ has a closed inhabitant. Thus there is a term $t$ with \begin{align*} \vdash_{\mathcal T} t : \mathsf{Empty}. \end{align*} The point of normalization is to replace the arbitrary proof term $t$ by a normal one, where the syntactic shape of the term can be classified. The normalization theorem for pure intensional Martin-Löf type theory, (citing a result not yet in the wiki: Normalization for pure intensional Martin-Löf type theory), applies because $\mathcal T$ is pure and contains no additional constants, postulates, or axioms beyond the standard type formers listed in the statement. Therefore there is a term $u$ such that $t \to^* u$ and $u$ is normal. Because $t$ is typed in the empty context, it has no free variables. Reduction only contracts redexes inside a term and does not introduce new free variables, so the normal form $u$ is also closed. We now transfer the type from $t$ to $u$. Subject reduction, or preservation, says that if a typed term reduces, then its reduct has the same type in the same context. Applying subject reduction along the finite reduction sequence $t \to^* u$ gives \begin{align*} \vdash_{\mathcal T} u : \mathsf{Empty}. \end{align*} Thus the contradiction has been reduced to the existence of a closed normal term of type $\mathsf{Empty}$. [/guided] [/step] [step:Classify closed normal terms of empty type] We use the canonical-forms lemma for pure intensional Martin-Löf type theory, (citing a result not yet in the wiki: Canonical forms for closed normal terms in pure intensional Martin-Löf type theory). In the form needed here, it says that if $w$ is a closed normal term and $\vdash_{\mathcal T} w : A$ for an inductively generated type $A$, then $w$ is either an introduction form for the outer type constructor of $A$, or $w$ is neutral. For $A = \mathsf{Empty}$, the first case is impossible because the empty type has no introduction rules and no constructors. The second case is also impossible in the empty context. Indeed, every neutral term is generated from a variable by repeatedly applying eliminators, applications, or projections to already neutral heads. Since the empty context contains no variables and $\mathcal T$ has no additional closed constants, there is no closed neutral term. Applying this to the closed normal term $u$ with \begin{align*} \vdash_{\mathcal T} u : \mathsf{Empty}, \end{align*} gives a contradiction. [/step] [step:Conclude that the empty type has no closed term] The contradiction arose only from the assumption that there exists a closed term $t$ satisfying \begin{align*} \vdash_{\mathcal T} t : \mathsf{Empty}. \end{align*} Therefore no such term exists. Hence pure intensional Martin-Löf type theory with the stated type formers and no extra closed constants, postulates, or axioms is consistent in the sense that $\mathsf{Empty}$ is not inhabited in the empty context. [/step]