System U Explained

In mathematical logic, System U and System U⁻ are pure type systems, i.e. special forms of a typed lambda calculus with an arbitrary number of sorts, axioms and rules (or dependencies between the sorts). System U was proved inconsistent by Jean-Yves Girard in 1972^[1] (and the question of consistency ofSystem U⁻ was formulated).This result led to the realization that Martin-Löf's original 1971 type theory was inconsistent as it allowed the same "Type in Type" behaviour that Girard's paradox exploits.

Formal definition

System U is defined^[2] as a pure type system with

\{\ast, \square, \triangle\} ;

• two axioms

\{\ast:\square, \square:\triangle\} ; and

• five rules

\{(\ast,\ast), (\square,\ast), (\square,\square), (\triangle,\ast), (\triangle,\square)\} .

System U⁻ is defined the same with the exception of the

(\triangle, \ast) rule.

The sorts

\ast and \square are conventionally called “Type” and “Kind”, respectively; the sort \triangle doesn't have a specific name. The two axioms describe the containment of types in kinds (\ast:\square ) and kinds in \triangle (\square:\triangle ). Intuitively, the sorts describe a hierarchy in the nature of the terms.

1. All values have a type, such as a base type (e.g.

b : Bool is read as “ is a boolean”) or a (dependent) function type (e.g. f : Nat \to Bool is read as “ is a function from natural numbers to booleans”).\ast is the sort of all such types (t : \ast is read as “ is a type”). From \ast we can build more terms, such as \ast \to \ast which is the kind of unary type-level operators (e.g. List : \ast \to \ast is read as “ is a function from types to types”, that is, a polymorphic type). The rules restrict how we can form new kinds.\square is the sort of all such kinds (k : \square is read as “ is a kind”). Similarly we can build related terms, according to what the rules allow.\triangle is the sort of all such terms.

The rules govern the dependencies between the sorts:

(\ast,\ast) says that values may depend on values (functions), (\square,\ast) allows values to depend on types (polymorphism), (\square,\square) allows types to depend on types (type operators), and so on.

Girard's paradox

The definitions of System U and U⁻ allow the assignment of polymorphic kinds to generic constructors in analogy to polymorphic types of terms in classical polymorphic lambda calculi, such as System F. An example of such a generic constructor might be (where k denotes a kind variable)

λ k ^{\square} λ \alpha ^{k} λ \beta ^{k.} \alpha (\alpha \beta) : \Pi k : \square.((k \to k) \to k \to k) .

This mechanism is sufficient to construct a term with the type

(\forall p:\ast, p) (equivalent to the type \bot ), which implies that every type is inhabited. By the Curry–Howard correspondence, this is equivalent to all logical propositions being provable, which makes the system inconsistent.

Girard's paradox is the type-theoretic analogue of Russell's paradox in set theory.

Further reading

• Book: Barendregt, Henk . S. Abramsky . D. Gabbay . T. Maibaum . Henk Barendregt . Lambda calculi with types . Handbook of Logic in Computer Science . 117–309 . . 1992 . ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps .
• Book: Coquand, Thierry . Thierry Coquand . An analysis of Girard's paradox . Logic in Computer Science . 227–236 . IEEE Computer Society Press . 1986 .
• Antonius J. C. . Hurkens . A simplification of Girard's paradox . Second International Conference on Typed Lambda Calculi and Applications (TLCA '95) . 266–278 . Edinburgh . 1995 . https://link.springer.com/book/10.1007/BFb0014040 . 10.1007/BFb0014058 . Mariangiola . Dezani-Ciancaglini . Gordon . Plotkin .

Notes and References

1. Web site: Jean-Yves . Girard . Interprétation fonctionnelle et Élimination des coupures de l'arithmétique d'ordre supérieur . 1972 .
2. Book: Morten Heine . Sørensen . Paweł . Urzyczyn . Lectures on the Curry–Howard isomorphism . Elsevier . 2006 . 0-444-52077-5 . Pure type systems and the lambda cube. 10.1016/S0049-237X(06)80015-7 .