在數理邏輯中，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表示種類變量)這意味著每個類型都是有人居住的。根據庫里-霍華德的對應關系，這相當于所有的邏輯命題都是可以證明的，這使得系統不一致。吉拉德悖論是集合論中羅素悖論的類型論類似物。