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 { ∗ , ◻ , △ } {\displaystyle \{\ast ,\square ,\triangle \}} ; two axioms { ∗ : ◻ , ◻ : △ } {\displaystyle \{\ast :\square ,\square :\triangle \}} ; and five rules { ( ∗ , ∗ ) , ( ◻ , ∗ ) , ( ◻ , ◻ ) , ( △ , ∗ ) , ( △ , ◻ ) } {\displaystyle \{(\ast ,\ast ),(\square ,\ast ),(\square ,\square ),(\triangle ,\ast ),(\triangle ,\square )\}} . System U− is defined the same with the exception of the ( △ , ∗ ) {\displaystyle (\triangle ,\ast )} rule. The sorts ∗ {\displaystyle \ast } and ◻ {\displaystyle \square } are conventionally called “type” and “kind”, respectively; the sort △ {\displaystyle \triangle } doesn't have a specific name. The two axioms describe the containment of types in kinds ( ∗ : ◻ {\displaystyle \ast :\square } ) and kinds in △ {\displaystyle \triangle } ( ◻ : △ {\displaystyle \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 : B o o l {\displaystyle b:\mathrm {Bool} } is read as “ b {\displaystyle b} is a boolean”) or a (dependent) function type (e.g. f : N a t → B o o l {\displaystyle f:\mathrm {Nat} \to \mathrm {Bool} } is read as “ f {\displaystyle f} is a function from natural numbers to booleans”).
∗ {\displaystyle \ast } is the sort of all such types ( t : ∗ {\displaystyle t:\ast } is read as “ t {\displaystyle t} is a type”). From ∗ {\displaystyle \ast } we can build more terms, such as ∗ → ∗ {\displaystyle \ast \to \ast } which is the kind of unary type-level operators (e.g. L i s t : ∗ → ∗ {\displaystyle \mathrm {List} :\ast \to \ast } is read as “ L i s t {\displaystyle \mathrm {List} } is a function from types to types”, that is, a polymorphic type). The rules restrict how we can form new kinds.
◻ {\displaystyle \square } is the sort of all such kinds ( k : ◻ {\displaystyle k:\square } is read as “ k {\displaystyle k} is a kind”). Similarly we can build related terms, according to what the rules allow.
△ {\displaystyle \triangle } is the sort of all such terms. The rules govern the dependencies between the sorts: ( ∗ , ∗ ) {\displaystyle (\ast ,\ast )} says that values may depend on values (functions), ( ◻ , ∗ ) {\displaystyle (\square ,\ast )} allows values to depend on types (polymorphism), ( ◻ , ◻ ) {\displaystyle (\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)
λ k ◻ λ α k → k λ β k . α ( α β ) : Π k : ◻ . ( ( k → k ) → k → k ) {\displaystyle \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 ( ∀ p : ∗ , p ) {\displaystyle (\forall p:\ast ,p)} (equivalent to the type ⊥ {\displaystyle \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 the Burali-Forti paradox in set theory.
References
Further reading Barendregt, Henk (1992). "Lambda calculi with types". In S. Abramsky; D. Gabbay; T. Maibaum (eds.). Handbook of Logic in Computer Science. Oxford Science Publications. pp. 117–309. Hurkens, Antonius J. C. (1995). Dezani-Ciancaglini, Mariangiola; Plotkin, Gordon (eds.). A simplification of Girard's paradox. Second International Conference on Typed Lambda Calculi and Applications (TLCA '95). Edinburgh. pp. 266–278. doi:10.1007/BFb0014058.