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: 352  as a pure type system with

System U− is defined the same with the exception of the (△,∗) rule.

The sorts ∗ and ◻ are conventionally called “type” and “kind”, respectively; the sort △ doesn't have a specific name. The two axioms describe the containment of types in kinds (∗:◻) and kinds in △ (◻:△). 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:Bool is read as “b is a boolean”) or a (dependent) function type (e.g. f:Nat→Bool is read as “f is a function from natural numbers to booleans”).
  2. ∗ is the sort of all such types (t:∗ is read as “t is a type”). From ∗ we can build more terms, such as ∗→∗ which is the kind of unary type-level operators (e.g. List:∗→∗ is read as “List 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. △ is the sort of all such terms.

The rules govern the dependencies between the sorts: (∗,∗) says that values may depend on values (functions), (◻,∗) 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 be: 353  (where k denotes a kind variable)

λk◻λαk→kλβk.α(αβ):Πk:◻.((k→k)→k→k).

This mechanism is sufficient to construct a term with the type (∀p:∗,p) (equivalent to the type ⊥), 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.

References

  1. ↑ Girard, Jean-Yves (1972). "Interprétation fonctionnelle et Élimination des coupures de l'arithmétique d'ordre supérieur" (PDF).
  2. 1 2 Sørensen, Morten Heine; Urzyczyn, Paweł (2006). "Pure type systems and the lambda cube". Lectures on the Curry–Howard isomorphism. Elsevier. doi:10.1016/S0049-237X(06)80015-7. ISBN 0-444-52077-5.
  3. ↑ Coquand, Thierry (1986). "An analysis of Girard's paradox". Logic in Computer Science. IEEE Computer Society Press. pp. 227–236.

Further reading