System U

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

In type theory and mathematical logic, '''System U''' and '''System U{{sup|−}}''' 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.<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. 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.<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 and therefore implies that every type is inhabited (and, via Curry–Howard 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. 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 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: 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: 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" />

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