Properties of the System

The core system

The theorems below concern the core system: the rules of Figure 3.1, with the universes of Chapter 13 and without the constants of Part II. This is a Pure Type System in the sense of Barendregt: the Calculus of Constructions [Coquand 1988] with a hierarchy of predicative universes above its impredicative $\Sort{0}$, close to Luo's Extended Calculus of Constructions [Luo 1990]. The first three properties hold for every functional Pure Type System [Barendregt 1992]. Strong normalization is much harder in the presence of impredicativity and needs Girard's method of reducibility candidates [Girard 1972; Coquand 1988; Luo 1990]. The end of the chapter says what changes with inductive types.

Four properties

A term has, up to conversion, one type. $\Infer$ depends on this: there is a single answer for it to compute, and $\Check$ can compare against it without worrying that some other derivation would have produced a different, non-convertible type.

The type of a well-typed term is itself a type (or is a universe, which has a type by T-Sort but need not be written as one). So the result of $\Infer$ can always be fed back into $\InferSort$, and contexts built by the algorithm stay well formed.

Computation preserves types. This is what justifies T-Conv and the whole strategy of deciding equality by normalization: reducing a term never takes it out of its type, so comparing normal forms compares the right things.

Every well-typed term reaches a normal form, whatever order reductions are performed in. This is the deep one. $\Whnf$, $\Normalize$, and therefore $\IsDefEq$ and $\Infer$ terminate on well-typed input because of it, and the next section shows that consistency rests on it too.

The four properties support the two guarantees in a definite pattern, drawn below: the arrows read "is needed for".

Together these give the two guarantees we want from a kernel.

• Decidability. Algorithm 5.1 terminates on every input, so whether a proof is correct can always be determined.
• Consistency. No closed term proves False.

Consistency

The argument has two halves, and their shape is visible without the details.

Reduce to normal forms. By strong normalization, such a term $t$ would have a normal form $n$, and by subject reduction, $n$ would have the same type. So it suffices to show that no normal closed term has type $\tPi{P}{\Sort{0}}{P}$. This step is where all the difficulty lies, because it uses Theorem 14.4.

Analyse normal forms. A normal term is a universe, a $\Pi$, a $\lambda$, or a variable applied to some arguments (a neutral term). A closed normal term whose type is a $\Pi$ must be a $\lambda$: it cannot be neutral, since no variable is in scope, and universes and $\Pi$-types have a universe as their type, not a $\Pi$. So $n = \tLam{P}{\Sort{0}}{s}$ with $P : \Sort{0} \vdash s : P$ and $s$ normal. Now ask what $s$ can be. A universe, a $\Pi$, or a $\lambda$ would have a universe or a $\Pi$ as its type, not the variable $P$. A neutral term would have to start with a variable in scope, and the only one is $P$ itself, whose type is $\Sort{0}$: it is not $P$, so $s$ cannot be $P$; and it is not a function type, so $P$ cannot be applied to anything. Every case is impossible.

Appendix D carries this out carefully, including the standard facts about typing and conversion (generation, confluence, substitution) that the case analysis silently uses.

With inductive types

The iota-rules of Part II do not overlap with each other or with beta, so reduction remains confluent. Subject reduction, strong normalization, and consistency are known for the Calculus of Inductive Constructions [Werner 1994], of which our system with inductive types is a small fragment. The short consistency argument above no longer suffices by itself, because normal forms now include stuck recursor applications such as $\NatRec{0}\;M\;z\;s\;n$ with $n$ a variable; consistency follows from strong normalization by a more careful analysis of normal forms, in which a neutral term may also be headed by a constant.

Each of the acceptance conditions of Chapter 8 corresponds to a way this analysis could fail: without positivity, iota-reduction can loop and strong normalization is lost; without the universe condition, a type could contain its own universe and the paradox of Chapter 13 returns; without the elimination restriction on propositions, proof irrelevance (which Lean assumes) would be refuted.

Lean's full theory, with definitional proof irrelevance, universe polymorphism, quotient types, and general nested and mutual inductive types, has subtler metatheory; Carneiro's thesis [Carneiro 2019] is the reference. The central structure, strong normalization plus an analysis of normal forms, is the same.

Exercises