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.

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. 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.

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.