System U

Template:Short description 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).

System U was proved inconsistent by Jean-Yves Girard in 1972 (and the question of consistency of System U⁻ was formulated). 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 definedTemplate:Rp as a pure type system with

• three sorts $\{\ast ,◻,\mathrm{△}\}$;
• two axioms $\{\ast :◻,◻:\mathrm{△}\}$; and
• five rules $\{(\ast ,\ast ),(◻,\ast ),(◻,◻),(\mathrm{△},\ast ),(\mathrm{△},◻)\}$.

System U⁻ is defined the same with the exception of the $(\mathrm{△},\ast )$ rule.

The sorts $\ast$ and $◻$ are conventionally called “type” and “kind”, respectively; the sort $\mathrm{△}$ doesn't have a specific name. The two axioms describe the containment of types in kinds ($\ast :◻$) and kinds in $\mathrm{△}$ ($◻:\mathrm{△}$). 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{B}\mathrm{o}\mathrm{o}\mathrm{l}$ is read as “$b$ is a boolean”) or a (dependent) function type (e.g. $f:\mathrm{N}\mathrm{a}\mathrm{t}\to \mathrm{B}\mathrm{o}\mathrm{o}\mathrm{l}$ 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{L}\mathrm{i}\mathrm{s}\mathrm{t}:\ast \to \ast$ is read as “$\mathrm{L}\mathrm{i}\mathrm{s}\mathrm{t}$ is a function from types to types”, that is, a polymorphic type). The rules restrict how we can form new kinds.
3. $◻$ is the sort of all such kinds ($k:◻$ is read as “$k$ is a kind”). Similarly we can build related terms, according to what the rules allow.
4. $\mathrm{△}$ 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), $(◻,\ast )$ 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 beTemplate:R (where k denotes a kind variable)

$\lambda k^{◻}\lambda {\alpha }^{k\to k}\lambda {\beta }^k.\alpha (\alpha \beta ):\mathrm{\Pi }k:◻.((k\to k)\to k\to k)$.

This mechanism is sufficient to construct a term with the type $(\mathrm{\forall }p:\ast ,p)$ (equivalent to the type $\mathrm{\perp }$), 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 the Burali-Forti paradox in set theory.

Further reading

• Template:Cite book
• Template:Cite conference