Formal definition
System U is defined as a pure type system with * three sorts ; * two axioms ; and * five rules . System U− is defined the same with the exception of the rule. The sorts and are conventionally called “Type” and “ Kind”, respectively; the sort doesn't have a specific name. The two axioms describe the containment of types in kinds () and kinds in (). Intuitively, the sorts describe a hierarchy in the ''nature'' of the terms. # All values have a ''type'', such as a base type (''e.g.'' is read as “ is a boolean”) or a (dependent) function type (''e.g.'' is read as “ is a function from natural numbers to booleans”). # is the sort of all such types ( is read as “ is a type”). From we can build more terms, such as which is the ''kind'' of unary type-level operators (''e.g.'' is read as “ is a function from types to types”, that is, a polymorphic type). The rules restrict how we can form new kinds. # is the sort of all such kinds ( is read as “ is a kind”). Similarly we can build related terms, according to what the rules allow. # is the sort of all such terms. The rules govern the dependencies between the sorts: says that values may depend on values ( functions), allows values to depend on types ( polymorphism), 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) :. This mechanism is sufficient to construct a term with the type (equivalent to the type ), 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 inReferences
Further reading
* * * {{cite conference , first=Antonius J. C. , last=Hurkens , title=A simplification of Girard's paradox , conference=Second International Conference on Typed Lambda Calculi and Applications (TLCA '95) , pages=266–278 , location=Edinburgh , url=https://link.springer.com/chapter/10.1007/BFb0014058 , date=1995 , conference-url=https://link.springer.com/book/10.1007/BFb0014040 , doi=10.1007/BFb0014058 , editor1-first=Mariangiola , editor1-last=Dezani-Ciancaglini , editor2-first=Gordon , editor2-last=Plotkin , url-access=subscription Lambda calculus Proof theory Type theory