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.^[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.

Formal definition

System U is defined^[2]: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 types and kinds, 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$). The rules govern the dependencies between the sorts: $(\ast,\ast)$ says that terms may depend on terms (functions), $(\square,\ast)$ allows terms 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^[2]:353 (where k denotes a kind variable)

$\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.

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

References

1. Girard, Jean-Yves (1972), Interprétation fonctionnelle et Élimination des coupure de l'arithmétique d'ordre supérieur
2. Sørensen, Morten Heine; Urzyczyn, Paweł (2006). "Pure type systems and the lambda cube". Lectures on the Curry–Howard isomorphism. Elsevier. ISBN 0-444-52077-5.

Further reading

• Barendregt, Henk (1992). "Lambda calculi with types". In S. Abramsky, D. Gabbay and T. Maibaum. Handbook of Logic in Computer Science. Oxford Science Publications. pp. 117–309.
• Coquand, Thierry (1986). "An analysis of Girard's paradox". Logic in Computer Science. IEEE Computer Society Press. pp. 227–236.