System U#Girard's paradox

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{{cite web |first=Jean-Yves |last=Girard |title=Interprétation fonctionnelle et Élimination des coupures de l'arithmétique d'ordre supérieur |year=1972 |url=https://www.cs.cmu.edu/~kw/scans/girard72thesis.pdf }} (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{{cite book |first1=Morten Heine |last1=Sørensen |first2=Paweł |last2=Urzyczyn |title=Lectures on the Curry–Howard isomorphism |publisher=Elsevier |year=2006 |isbn=0-444-52077-5 |chapter=Pure type systems and the lambda cube|doi=10.1016/S0049-237X(06)80015-7 }}{{rp|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.

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”).
$\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 “ $\mathrm{List}$ 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{{r|SoerensenUrzyczyn2006|page=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)$ (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.

System U#Girard's paradox

Formal definition

Girard's paradox

References

Further reading