# 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:352 as a pure type system with

• three sorts $\{\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:\mathrm {Bool}$ is read as “b is a boolean”) or a (dependent) function type (e.g. $f:\mathrm {Nat} \to \mathrm {Bool}$ is read as “f is a function from natural numbers to booleans”).
2. $\ast$ is the sort of all such types ($t:\ast$ is read as “t 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. $\mathrm {List} :\ast \to \ast$ is read as “List is a function from types to types”, that is, a polymorphic type). The rules restrict how we can form new kinds.
3. $\square$ is the sort of all such kinds ($k:\square$ is read as “k is a kind”). Similarly we can build related terms, according to what the rules allow.
4. $\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.

$\lambda k^{\square }\lambda \alpha ^{k\to k}\lambda \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)=\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.