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). They were both proved inconsistent by Jean-Yves Girard in 1972. 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 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”).