System U

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

More information Sorts ...

Component	System U	System U−
Sorts ${\displaystyle S}$	${\displaystyle \{\ast ,\ \square ,\ \triangle \}}$	${\displaystyle \{\ast ,\ \square ,\ \triangle \}}$
Axioms ${\displaystyle A}$	${\displaystyle \{\ \ast$ :\square ,\ \square :\triangle \ \}}	${\displaystyle \{\ \ast$ :\square ,\ \square :\triangle \ \}}
Product rules ${\displaystyle R}$	${\displaystyle \{(\ast ,\ast ),\ (\square ,\ast ),\ (\square ,\square ),\ (\triangle ,\ast ),\ (\triangle ,\square )\}}$	${\displaystyle \{(\ast ,\ast ),\ (\square ,\ast ),\ (\square ,\square ),\ (\triangle ,\square )\}}$

Close

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

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

${\displaystyle \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^{\square }.\ \lambda \alpha ^{k\to k}.\ \lambda \beta ^{k}.\ \alpha (\alpha \,\beta )\$ :\ \Pi k:\square .\ ((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 {Type} _{0}:\mathrm {Type} _{1}:\mathrm {Type} _{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