Pure type systems and the lambda cube

A PTS is fixed by sorts $S$, axioms $\mathcal{A}\subseteq C\times S$, and product triples $\mathcal{R}\subseteq S^3$. Its only term constructors are constants, variables, application, annotated abstraction, and dependent product. The lambda-cube instances use $S=\{\ast ,◻\}$, the axiom $\ast :◻$, the ordinary triple $(\ast ,\ast ,\ast )$, and a subset of the three optional triples listed in subappendix A.59.

Conversion is compatible beta-equivalence on pseudo-terms. The system has no primitive eta-rule, inductive family, identity eliminator, universe hierarchy, large elimination, store, effect, or observation rule.

Context validity, free-variable containment, weakening, substitution, generation, correctness of types, untyped beta-confluence, product compatibility, and subject reduction are proved in chapter 22. Beta-equivalence is proved compatible with substitution in both arguments.

Barendregt’s Lemma 5.2.21 gives type uniqueness for functional specifications, and Corollary 5.2.18 gives decidable checking under the finite, effective, and normalization hypotheses made explicit in the chapter. Theorem 5.3.33 gives strong normalization for exactly the eight lambda-cube vertices. The one-sort system $\ast :\ast$ instead inherits Girard’s paradox through Definition 5.5.1 and Corollary 5.5.4: every type is inhabited and some typable terms have no normal form.

Setzer’s ordinal ${\psi }_{{\mathrm{\Omega }}_1}({\mathrm{\Omega }}_{I+\omega })$ belongs to the exact Martin–Löf system with one universe and W-types described in his paper. It is not a theorem about an arbitrary PTS or about the Calculus of Constructions, and no earlier book result depends on the ordinal analysis.

The Kappa companion checks four finite beta-normal cube-classification cases and one application accepted after a single visible type-redex development. It proves none of the structural, normalization, inconsistency, or decision theorems above.