System U

In type theory and mathematical logic, System U and System U⁻ are two closely related pure type systems (PTS), i.e. typed λ-calculi specified by a finite set of sorts (universes), axioms between sorts, and rules describing which kinds of dependent function spaces (Π-types) may be formed.^[1]

System U is historically important because it is strong enough to express a form of "type-in-type"/impredicativity that leads to Girard's paradox. Girard proved System U inconsistent in 1972.^[2] A later simplification due to Hurkens shows that even the restricted variant System U⁻ suffices for a paradox; for example, the Coq/Rocq standard library explicitly presents "Hurkens's paradox … for system U⁻" as a derivation of false.^[3][4]

These inconsistency results influenced the design of later type theories and proof assistants, which typically use a hierarchy of universes rather than a single universe containing itself.^[5][6]

A pure type system is commonly presented as a triple ${\displaystyle (S,A,R)}$ consisting of:

• a set of sorts ${\displaystyle S}$ (universe levels);
• a set of axioms ${\displaystyle A}$, written ${\displaystyle s_1:s_2}$, specifying which sorts classify which other sorts; and
• a set of product rules ${\displaystyle R}$, describing when a dependent function type ${\displaystyle \mathrm{\Pi }x:A.B}$ can be formed.^[1]

Many PTSs (including System U and System U⁻) use product rules of the schematic form

if ${\displaystyle A:s_1}$ and ${\displaystyle B:s_2}$ in context ${\displaystyle x:A}$, then ${\displaystyle \mathrm{\Pi }x:A.B:s_2}$,

so the sort of the Π-type is determined by the sort of its codomain.

Following the presentation in standard references on the λ-cube and pure type systems,^[7] System U and System U⁻ are specified by the following sorts, axioms, and Π-formation rules.

Here ${\displaystyle \ast }$ is conventionally read as the sort of "types", ${\displaystyle ◻}$ as the sort of "kinds", and ${\displaystyle \mathrm{△}}$ as a higher sort above ${\displaystyle ◻}$ (often left unnamed). The axioms say that types have sort ${\displaystyle ◻}$ and kinds have sort ${\displaystyle \mathrm{△}}$.

The product rules can be read as permitted dependencies:

• ${\displaystyle (\ast ,\ast )}$: terms may depend on terms (ordinary functions).
• ${\displaystyle (◻,\ast )}$: terms may be polymorphic in types (type-parametric functions).
• ${\displaystyle (◻,◻)}$: types may depend on types (type operators / type constructors).
• ${\displaystyle (\mathrm{△},◻)}$: kinds may depend on higher-level objects (higher-order kind formation).
• The extra rule ${\displaystyle (\mathrm{△},\ast )}$ (present only in System U) additionally allows types (and hence terms) to depend on higher-level objects; System U⁻ omits this particular form of dependency.^[7]

System U (and, in fact, System U⁻ as well) is inconsistent: one can construct a term inhabiting the type

${\displaystyle \mathrm{\forall }p:\ast .p}$,

which corresponds to false and therefore implies that every type is inhabited (and, via Curry–Howard correspondence, that every proposition is provable).^[2][8][3]

Intuitively, the paradox becomes possible because the rules allow "polymorphism at the level of kinds", analogous to polymorphic terms in System F. For example, one can assign a polymorphic kind to a generic constructor such as:^[7]

${\displaystyle \lambda k^{◻}.\lambda {\alpha }^{k\to k}.\lambda {\beta }^k.\alpha (\alpha \beta ):\mathrm{\Pi }k:◻.((k\to k)\to k\to k).}$

Hurkens later gave a shorter and more modular presentation of the paradox (commonly called Hurkens's paradox); the Coq/Rocq standard library explicitly treats it as a paradox for System U⁻ (deriving false from axioms expressing U⁻-style impredicativity).^[3][4]

Girard's paradox is often described as a type-theoretic analogue of the Burali-Forti paradox: collapsing universe levels allows one to represent a "totality" that must simultaneously be inside and strictly above itself, producing a contradiction.^[8][5]

Girard's 1972 inconsistency result clarified that a sufficiently strong "type of all types" principle is incompatible with consistency.^[2][5] This observation also affected early formulations of Martin-Löf type theory: Martin-Löf notes that an earlier, strongly impredicative axiom asserting a type of all types "had to be abandoned … after it was shown to lead to a contradiction by Jean Yves Girard".^[6] Subsequent systems typically avoid this by stratifying universes (e.g. ${\displaystyle {\mathrm{T}\mathrm{y}\mathrm{p}\mathrm{e}}_0:{\mathrm{T}\mathrm{y}\mathrm{p}\mathrm{e}}_1:{\mathrm{T}\mathrm{y}\mathrm{p}\mathrm{e}}_2:\cdots }$) or by other restrictions on impredicativity.^[5]

• Girard's paradox
• Pure type system
• Lambda cube
• Universe (type theory)
• Martin-Löf type theory
• Burali-Forti paradox

• Barendregt, Henk (1992). "Lambda calculi with types". Handbook of Logic in Computer Science. 2. Oxford University Press. pp. 117–309. 
• Howe, Douglas J. (1987). The Computational Behaviour of Girard's Paradox (Technical report). Cornell University, Computer Science Technical Reports. Retrieved 2026-03-01.

0.00 (0 votes) Original source: https://en.wikipedia.org/wiki/System U. Read more