Supriya Ghosh (Editor)

System U

Updated on
Edit
Like
Comment
Share on FacebookTweet on TwitterShare on LinkedInShare on Reddit

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

Contents

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 ( △ , ∗ ) 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 : B o o l is read as “b is a boolean”) or a (dependent) function type (e.g. f : N a t → B o o l 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. L i s t : ∗ → ∗ 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 ) = ⊥ , 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

    System U Wikipedia
    (Text) CC BY-SA