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).
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.
are conventionally called “Type” and “Kind”, respectively; the sort
The two axioms describe the containment of types in kinds (
Intuitively, the sorts describe a hierarchy in the nature of the terms.
The rules govern the dependencies between the sorts:
allows values to depend on types (polymorphism),
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[2]: 353 (where k denotes a kind variable) This mechanism is sufficient to construct a term with the type
By the Curry–Howard correspondence, this is equivalent to all logical propositions being provable, which makes the system inconsistent.