U系统

在数理逻辑中，U系统和U-系统是纯类型系统，即具有任意数量的排序、公理和规则（或排序之间的依赖关系）的类型化λ计算的特殊形式。它们都被Jean-YvesGirard在1972年证明是不一致的。这一结果导致人们认识到，马丁-洛夫1971年的原始类型理论是不一致的，因为它允许与吉拉德悖论所利用的类型中的类型行为相同。

系统U被定义为一个纯类型系统，具有{displaystyleb:mathrm{Bool}）。}被解读为"b是一个布尔值"）或一个（依赖）函数类型（例如{displaystyleast}是所有这些类型的排序。是所有这些类型的排序(t:∗{displaystylet:ast}是所有此类类型的排序。被理解为"t是一个类型"）。从{displaystyleast}中，我们可以建立更多的术语，如我们可以建立更多的术语，比如说{displaystylemathrm{List}:asttoast}被理解为"List是一个函数。被理解为"List是一个从类型到类型的函数"，也就是一个多态类型）。这些规则限制了我们如何形成新的类型。{displaystyle{square}是所有这些类型的排序。{displaystylek:square}是所有此类种类的排序。被理解为"k是一个种类"）。同样地，我们可以根据规则所允许的情况来建立相关术语。

{displaystyletriangle}是所有此类术语的排序。{displaystyle(square,ast)}说数值可以依赖于数值（函数）。允许值依赖于类型（多态性）。(◻,◻){displaystyle(square,square)}允许数值依赖于类型（多态性）。允许类型依附于类型（类型操作符），等等。

系统U和U-的定义允许将多态类型分配给泛型构造器，类似于经典多态λ计算中术语的多态类型，比如系统F。这种泛型构造器的一个例子是353(其中k表示种类变量)这意味着每个类型都是有人居住的。根据库里-霍华德的对应关系，这相当于所有的逻辑命题都是可以证明的，这使得系统不一致。吉拉德悖论是集合论中罗素悖论的类型论类似物。