System U

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.