System F

Types are generated only by type variables, arrows, and impredicative universal quantification. Terms are variables, annotated term abstraction/application, and explicit type abstraction/application. Type and term binders are identified up to alpha-equivalence. The dynamics has exactly term beta and type beta; no primitive data, recursion, effects, subtyping, or type-level computation is present.

Type and term substitution, preservation, progress, and call-by-value safety are proved in lemma 5.6, corollary 5.12. Compatible beta reduction is strongly normalizing and confluent by theorem 5.35, theorem 5.38; hence the calculus is syntactically consistent. Checking fully annotated Church terms is decidable by proposition 5.22.

Terms are raw untyped lambda terms; universal introduction and elimination leave no syntax. Erasure from Church derivations and decoration of Curry derivations are proved in theorem 5.21. Curry typability and checking are undecidable by the exact imported result in theorem 5.23; this status does not transfer to the Church checker.

Reynolds’ obstruction is imported only for the classical full-function package of definition 9.47. The stable-element restriction and idempotent splitting are imported through the exact interface theorem 9.50; the cardinal contradiction is proved locally in theorem 5.40. It is not a syntactic inconsistency theorem. No executable artifact is used as evidence for these metatheorems.