To install click the Add extension button. That's it.

The source code for the WIKI 2 extension is being checked by specialists of the Mozilla Foundation, Google, and Apple. You could also do it yourself at any point in time. 4,5
Kelly Slayton
Congratulations on this excellent venture… what a great idea!
Alexander Grigorievskiy
I use WIKI 2 every day and almost forgot how the original Wikipedia looks like.
Live Statistics
English Articles
Improved in 24 Hours
Languages
Recent
Show all languages
What we do. Every page goes through several hundred of perfecting techniques; in live mode. Quite the same Wikipedia. Just better.
.
Leo
Newton
Brights
Milds # 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. 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.

• 1/3
Views:
2 969
21 569
1 488
• System U aujourd'hui
• FreedomRail Closet Organization System Install - Glenbrook U
• E36 BMW 328is UUC System U Exhaust

## Formal definition

System U is defined: 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.

1. 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”).
2. $\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 “List is a function from types to types”, that is, a polymorphic type). The rules restrict how we can form new kinds.
3. $\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.
4. $\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.

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