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.[1] 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.
System U is defined[2]:352 as a pure type system with
System U− is defined the same with the exception of the [math]\displaystyle{ (\triangle, \ast) }[/math] rule.
The sorts [math]\displaystyle{ \ast }[/math] and [math]\displaystyle{ \square }[/math] are conventionally called “Type” and “Kind”, respectively; the sort [math]\displaystyle{ \triangle }[/math] doesn't have a specific name. The two axioms describe the containment of types in kinds ([math]\displaystyle{ \ast:\square }[/math]) and kinds in [math]\displaystyle{ \triangle }[/math] ([math]\displaystyle{ \square:\triangle }[/math]). Intuitively, the sorts describe a hierarchy in the nature of the terms.
The rules govern the dependencies between the sorts: [math]\displaystyle{ (\ast,\ast) }[/math] says that values may depend on values (functions), [math]\displaystyle{ (\square,\ast) }[/math] allows values to depend on types (polymorphism), [math]\displaystyle{ (\square,\square) }[/math] allows types to depend on types (type operators), and so on.
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 [math]\displaystyle{ (\forall p:\ast, p) }[/math] (equivalent to the type [math]\displaystyle{ \bot }[/math]), 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 Russell's paradox in set theory.
![]() | Original source: https://en.wikipedia.org/wiki/System U.
Read more |