# System U

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/System_U
> Markdown URL: https://mediated.wiki/source/System_U.md
> Source: https://en.wikipedia.org/wiki/System_U
> Source revision: 1355359735
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

{{short description|Inconsistent pure type systems related to Girard's paradox}}

In [type theory](/source/type_theory) and [mathematical logic](/source/mathematical_logic), '''System U''' and '''System U{{sup|−}}''' are two closely related [pure type system](/source/pure_type_system)s (PTS), i.e. typed [λ-calculi](/source/lambda_calculus) specified by a finite set of ''sorts'' (universes), axioms between sorts, and rules describing which kinds of dependent function spaces (Π-types) may be formed.<ref name="Barendregt1991">{{cite journal |last=Barendregt |first=Henk |title=Introduction to generalized type systems |journal=Journal of Functional Programming |volume=1 |issue=2 |date=April 1991 |pages=125–154 |doi=10.1017/S0956796800020025|hdl=2066/17240 |hdl-access=free }}</ref>

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](/source/Girard's_paradox). Girard proved System U inconsistent in 1972.<ref name="Girard1972">{{cite thesis |last=Girard |first=Jean-Yves |title=Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur |type=Thèse de doctorat d'État |institution=Université Paris VII |year=1972 |url=https://www.cs.cmu.edu/~kw/scans/girard72thesis.pdf}}</ref> A later simplification due to Hurkens shows that even the restricted variant System U{{sup|−}} suffices for a paradox; for example, the Coq/Rocq standard library explicitly presents "Hurkens's paradox … for system U{{sup|−}}" as a derivation of [false](/source/False_(logic)).<ref name="Hurkens1995">{{cite conference |last=Hurkens |first=Antonius J. C. |title=A simplification of Girard's paradox |book-title=Typed Lambda Calculi and Applications (TLCA '95) |editor-last1=Dezani-Ciancaglini |editor-first1=Mariangiola |editor-last2=Plotkin |editor-first2=Gordon |series=Lecture Notes in Computer Science |volume=902 |publisher=Springer |year=1995 |pages=266–278 |doi=10.1007/BFb0014058}}</ref><ref name="CoqHurkensUminus">{{cite web |title=Library Coq.Logic.Hurkens |website=Rocq/Coq Standard Library documentation |url=https://rocq-prover.org/doc/V8.19.2/stdlib/Coq.Logic.Hurkens.html |access-date=2026-03-01}}</ref>

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.<ref name="SEPTypeTheory">{{cite web |title=Type Theory (Spring 2025 Edition) |website=Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/spr2025/entries/type-theory/ |access-date=2026-03-01}}</ref><ref name="ML1972Rocq">{{cite web |title=An Intuitionistic Theory of Types |author=Per Martin-Löf |website=Rocq Papers |year=1972 |url=https://rocq-prover.org/papers/an-intuitionistic-theory-of-types |access-date=2026-03-01}}</ref>

== Background: pure type systems ==
A pure type system is commonly presented as a triple <math>(S,A,R)</math> consisting of:
* a set of ''sorts'' <math>S</math> (universe levels);
* a set of ''axioms'' <math>A</math>, written <math>s_1 : s_2</math>, specifying which sorts classify which other sorts; and
* a set of ''product rules'' <math>R</math>, describing when a dependent function type <math>\Pi x:A.\,B</math> can be formed.<ref name="Barendregt1991" />

Many PTSs (including System U and System U{{sup|−}}) use product rules of the schematic form
: if <math>A:s_1</math> and <math>B:s_2</math> in context <math>x:A</math>, then <math>\Pi x:A.\,B : s_2</math>,
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,<ref name="SoerensenUrzyczyn2006">{{cite book |last1=Sørensen |first1=Morten Heine |last2=Urzyczyn |first2=Paweł |title=Lectures on the Curry–Howard Isomorphism |publisher=Elsevier |year=2006 |isbn=978-0-444-52077-7 |doi=10.1016/S0049-237X(06)80015-7}}</ref> System U and System U{{sup|−}} are specified by the following sorts, axioms, and Π-formation rules.

{| class="wikitable" style="text-align:left;"
! Component !! System U !! System U{{sup|−}}
|-
| Sorts <math>S</math>
| <math>\{\ast,\ \square,\ \triangle\}</math>
| <math>\{\ast,\ \square,\ \triangle\}</math>
|-
| Axioms <math>A</math>
| <math>\{\ \ast:\square,\ \square:\triangle\ \}</math>
| <math>\{\ \ast:\square,\ \square:\triangle\ \}</math>
|-
| Product rules <math>R</math>
| <math>\{(\ast,\ast),\ (\square,\ast),\ (\square,\square),\ (\triangle,\ast),\ (\triangle,\square)\}</math>
| <math>\{(\ast,\ast),\ (\square,\ast),\ (\square,\square),\ (\triangle,\square)\}</math>
|}

Here <math>\ast</math> is conventionally read as the sort of "types", <math>\square</math> as the sort of "kinds", and <math>\triangle</math> as a higher sort above <math>\square</math> (often left unnamed). The axioms say that types have sort <math>\square</math> and kinds have sort <math>\triangle</math>.

=== Informal reading of the rules ===
The product rules can be read as permitted dependencies:
* <math>(\ast,\ast)</math>: terms may depend on terms (ordinary functions).
* <math>(\square,\ast)</math>: terms may be polymorphic in types (type-parametric functions).
* <math>(\square,\square)</math>: types may depend on types (type operators / type constructors).
* <math>(\triangle,\square)</math>: kinds may depend on higher-level objects (higher-order kind formation).
* The extra rule <math>(\triangle,\ast)</math> (present only in System U) additionally allows types (and hence terms) to depend on higher-level objects; System U{{sup|−}} omits this particular form of dependency.<ref name="SoerensenUrzyczyn2006" />

== Inconsistency and Girard's paradox ==
System U (and, in fact, System U{{sup|−}} as well) is inconsistent: one can construct a term inhabiting the type
:<math>\forall p:\ast.\,p</math>,
which corresponds to [false](/source/bottom_type) and therefore implies that every type is inhabited (and, via [Curry–Howard correspondence](/source/Curry%E2%80%93Howard_correspondence), that every proposition is provable).<ref name="Girard1972" /><ref name="Coquand1986">{{cite conference |last=Coquand |first=Thierry |title=An Analysis of Girard's Paradox |book-title=Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986) |publisher=IEEE Computer Society Press |location=Cambridge, MA, USA |date=June 1986 |pages=227–236 |url=https://lics.siglog.org/1986/Coquand-AnAnalysisofGirards.html |access-date=2026-03-01}}</ref><ref name="Hurkens1995" />

Intuitively, the paradox becomes possible because the rules allow "polymorphism at the level of kinds", analogous to polymorphic terms in [System F](/source/System_F). For example, one can assign a polymorphic kind to a generic constructor such as:<ref name="SoerensenUrzyczyn2006" />
:<math>\lambda k^{\square}.\ \lambda \alpha^{k\to k}.\ \lambda \beta^{k}.\ \alpha(\alpha\,\beta)\ :\ \Pi k:\square.\ ((k\to k)\to k\to k).</math>
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{{sup|−}} (deriving [false](/source/false) from axioms expressing U{{sup|−}}-style impredicativity).<ref name="Hurkens1995" /><ref name="CoqHurkensUminus" />

Girard's paradox is often described as a type-theoretic analogue of the [Burali-Forti paradox](/source/Burali-Forti_paradox): collapsing universe levels allows one to represent a "totality" that must simultaneously be inside and strictly above itself, producing a contradiction.<ref name="Coquand1986" /><ref name="SEPTypeTheory" />

== Historical context ==
Girard's 1972 inconsistency result clarified that a sufficiently strong "type of all types" principle is incompatible with consistency.<ref name="Girard1972" /><ref name="SEPTypeTheory" /> This observation also affected early formulations of [Martin-Löf type theory](/source/Martin-L%C3%B6f_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".<ref name="ML1972Rocq" /> Subsequent systems typically avoid this by stratifying universes (e.g. <math>\mathrm{Type}_0 : \mathrm{Type}_1 : \mathrm{Type}_2 : \cdots</math>) or by other restrictions on impredicativity.<ref name="SEPTypeTheory" />

== See also ==
* [Girard's paradox](/source/Girard's_paradox)
* [Pure type system](/source/Pure_type_system)
* [Lambda cube](/source/Lambda_cube)
* [Universe (type theory)](/source/Universe_(type_theory))
* [Martin-Löf type theory](/source/Martin-L%C3%B6f_type_theory)
* [Burali-Forti paradox](/source/Burali-Forti_paradox)

== References ==
{{reflist}}

== Further reading ==
* {{cite book |last=Barendregt |first=Henk |chapter=Lambda calculi with types |editor-last1=Abramsky |editor-first1=Samson |editor-last2=Gabbay |editor-first2=Dov M. |editor-last3=Maibaum |editor-first3=Thomas S. E. |title=Handbook of Logic in Computer Science |volume=2 |publisher=Oxford University Press |year=1992 |pages=117–309}}
* {{cite tech report |last=Howe |first=Douglas J. |title=The Computational Behaviour of Girard's Paradox |institution=Cornell University, Computer Science Technical Reports |year=1987 |url=https://ecommons.cornell.edu/items/53ab9742-5d85-468e-a200-08475caa6d94 |access-date=2026-03-01}}

Category:Lambda calculus
Category:Proof theory
Category:Type theory

---
Adapted from the Wikipedia article [System U](https://en.wikipedia.org/wiki/System_U) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/System_U?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.