System U

Short description: Inconsistent pure type systems related to Girard's paradox

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.

Background: pure type systems

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

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

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

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

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

Formal definition

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

Component	System U	System U−
Sorts $S$	$\{\ast ,◻,\mathrm{△}\}$	$\{\ast ,◻,\mathrm{△}\}$
Axioms $A$	$\{\ast :◻,◻:\mathrm{△}\}$	$\{\ast :◻,◻:\mathrm{△}\}$
Product rules $R$	$\{(\ast ,\ast ),(◻,\ast ),(◻,◻),(\mathrm{△},\ast ),(\mathrm{△},◻)\}$	$\{(\ast ,\ast ),(◻,\ast ),(◻,◻),(\mathrm{△},◻)\}$

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

Informal reading of the rules

The product rules can be read as permitted dependencies:

• $(\ast ,\ast )$: terms may depend on terms (ordinary functions).
• $(◻,\ast )$: terms may be polymorphic in types (type-parametric functions).
• $(◻,◻)$: types may depend on types (type operators / type constructors).
• $(\mathrm{△},◻)$: kinds may depend on higher-level objects (higher-order kind formation).
• The extra rule $(\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.

Inconsistency and Girard's paradox

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

$\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).

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:

$\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).

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.

Historical context

Girard's 1972 inconsistency result clarified that a sufficiently strong "type of all types" principle is incompatible with consistency. 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". Subsequent systems typically avoid this by stratifying universes (e.g. ${\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.

See also

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

Further reading

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