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

## Contents

* 1 Background: pure type systems
* 2 Formal definition
* 2.1 Informal reading of the rules
* 3 Inconsistency and Girard's paradox
* 4 Historical context
* 5 See also
* 6 References
* 7 Further reading

## 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 s1:s2, specifying which sorts classify which other sorts; and
* a set of product rules R, describing when a dependent function type Πx:A.B can be formed.[1]

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

if A:s1 and B:s2 in context x:A, then Πx:A.B:s2,

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,[7] System U and System U− are specified by the following sorts, axioms, and Π-formation rules.

Component | System U | System U−

|
|

Sorts S | {∗, ◻, △} | {∗, ◻, △}
Axioms A | { ∗:◻, ◻:△ } | { ∗:◻, ◻:△ }
Product rules R | {(∗,∗), (◻,∗), (◻,◻), (△,∗), (△,◻)} | {(∗,∗), (◻,∗), (◻,◻), (△,◻)}

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

### Informal reading of the rules

The product rules can be read as permitted dependencies:

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

## Inconsistency and Girard's paradox

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

∀p:∗.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]

λk◻. λαk->k. λβk. α(αβ) : Πk:◻. ((k->k)->k->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]

## Historical context

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. Type0:Type1:Type2:⋯) or by other restrictions on impredicativity.[5]

## See also

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

## References

1. ↑ 1.0 1.1 Barendregt, Henk (April 1991). "Introduction to generalized type systems". Journal of Functional Programming 1 (2): 125–154. doi:10.1017/S0956796800020025.
2. ↑ 2.0 2.1 2.2 Girard, Jean-Yves (1972). Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur (PDF) (Thèse de doctorat d'État). Université Paris VII.
3. ↑ 3.0 3.1 3.2 Hurkens, Antonius J. C. (1995). "A simplification of Girard's paradox". 902. Springer. pp. 266–278. doi:10.1007/BFb0014058.
4. ↑ 4.0 4.1 "Library Coq.Logic.Hurkens". https://rocq-prover.org/doc/V8.19.2/stdlib/Coq.Logic.Hurkens.html.
5. ↑ 5.0 5.1 5.2 5.3 Zalta, Edward N., ed. "Type Theory (Spring 2025 Edition)". https://plato.stanford.edu/archives/spr2025/entries/type-theory/.
6. ↑ 6.0 6.1 Per Martin-Löf (1972). "An Intuitionistic Theory of Types". https://rocq-prover.org/papers/an-intuitionistic-theory-of-types.
7. ↑ 7.0 7.1 7.2 Sørensen, Morten Heine; Urzyczyn, Paweł (2006). Lectures on the Curry–Howard Isomorphism. Elsevier. doi:10.1016/S0049-237X(06)80015-7. ISBN 978-0-444-52077-7.
8. ↑ 8.0 8.1 Coquand, Thierry (June 1986). "An Analysis of Girard's Paradox". Cambridge, MA, USA: IEEE Computer Society Press. pp. 227–236. https://lics.siglog.org/1986/Coquand-AnAnalysisofGirards.html. Retrieved 2026-03-01.

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

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/System U. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=System_U&oldid=4297173"