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).

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 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 $(\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.
# All values have a ''type'', such as a base type (''e.g.'' $b : \mathrm$ is read as “$b$ is a boolean”) or a (dependent) function type (''e.g.'' $f : \mathrm \to \mathrm$ is read as “$f$ is a function from natural numbers to booleans”).
# $\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 : \ast \to \ast$ is read as “$\mathrm$ is a function from types to types”, that is, a polymorphic type). The rules restrict how we can form new kinds.
# $\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.
# $\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.

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 be (where ''k'' denotes a kind variable)

:$\lambda k^\square \lambda\alpha^ \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)$ (equivalent to the type $\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.

Girard's paradox is the type-theoretic analogue of Russell's paradox in set theory.

References

Further reading

*
*
* {{cite conference , first=Antonius J. C. , last=Hurkens , title=A simplification of Girard's paradox , conference=Second International Conference on Typed Lambda Calculi and Applications (TLCA '95) , pages=266–278 , location=Edinburgh , url=https://link.springer.com/chapter/10.1007/BFb0014058 , date=1995 , conference-url=https://link.springer.com/book/10.1007/BFb0014040 , doi=10.1007/BFb0014058 , editor1-first=Mariangiola , editor1-last=Dezani-Ciancaglini , editor2-first=Gordon , editor2-last=Plotkin , url-access=subscription

Lambda calculus
Proof theory
Type theory