システムU

型理論と数理論理学において、システム Uとシステム U ⁻は密接に関連した 2 つの純粋型システム(PTS) であり、すなわち、有限個のソート(ユニバース)、ソート間の公理、およびどのような種類の依存関数空間 (Π-型) を形成できるかを記述する規則によって指定される型付きλ 計算である。^{[ 1 ]}

システム U は、ジラールのパラドックスにつながる「型内型」/非述語性を表現するのに十分な強さを持っているため、歴史的に重要です。ジラールは 1972 年にシステム U が矛盾していることを証明しました。^{[ 2 ]}後に Hurkens によって簡略化された結果、制限された変種であるシステム U ⁻でさえパラドックスを生じさせるのに十分であることが示されました。たとえば、Coq/Rocq標準ライブラリは、 falseの導出として「システム U ⁻の Hurkens のパラドックス」を明示的に示しています。^{[ 3 ] [ 4 ]}

これらの矛盾の結果は、後の型理論や証明支援システムの設計に影響を与え、それらは通常、単一の宇宙がそれ自身を含むのではなく、宇宙の階層を使用する。 ^{[ 5 ] [ 6 ]}

純粋な型システムは、一般的にトリプルとして表現されます。${\displaystyle (S,A,R)}$構成：

• ある種のセット${\displaystyle S}$（宇宙レベル）
• 一連の公理${\displaystyle A}$書かれた$s_1:s_2$どの分類が他のどの分類を分類するかを指定すること。
• 一連の製品ルール${\displaystyle R}$依存関数型がいつになるかを説明する${\displaystyle \Pi x:A.\,B}$形成することができる。^{[ 1 ]}

多くのPTS（System UおよびSystem U ⁻を含む）は、概略形式の積ルールを使用する。

もし${\displaystyle A:s_{1}}$そして${\displaystyle B:s_{2}}$文脈において${\displaystyle x:A}$、 それから${\displaystyle \Pi x:A.\,B:s_{2}}$、

したがって、Π型のソートは、そのコドメインのソートによって決定されます。

λキューブと純粋型システムに関する標準的な参考文献の発表に続いて、^{[ 7 ]}システム U とシステム U ⁻は、次のソート、公理、および Π 形成規則によって指定されます。

ここ${\displaystyle \ast }$は慣習的に「タイプ」の一種として読まれ、${\displaystyle \square }$「種類」として、そして${\displaystyle \triangle }$上位の種別として${\displaystyle \square }$（多くの場合、名前は付けられない）。公理によれば、型にはソートがある。${\displaystyle \square }$種類は${\displaystyle \triangle }$。

システム U (そして実際にはシステム U ⁻も) は矛盾している:

${\displaystyle \forall p:\ast .\,p}$、

これは偽に対応し、したがってすべての型が占有されている（そして、カリー・ハワード対応により、すべての命題が証明可能である）ことを意味する。^{[ 2 ] [ 8 ] [ 3 ]}

直感的に言えば、このパラドックスは、 System Fの多相項に類似した「種類のレベルでの多相性」をルールが許容するため可能になります。たとえば、次のような汎用コンストラクタに多相の種類を割り当てることができます。^{[ 7 ]}

${\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).}

ハーケンスは後にこのパラドックスをより短くモジュール化した形で提示した（一般にハーケンスのパラドックスと呼ばれる）。Coq/Rocq標準ライブラリはこれをシステム^U−のパラドックスとして明示的に扱っている（^U−スタイルの非述語性を表す公理から偽を導出する）。^{[ 3 ] [ 4 ]}

ジラールのパラドックスは、しばしばブラリ＝フォルティのパラドックスのタイプ理論的な類似物として説明される。宇宙レベルを縮退させることで、同時にその内部にあり、かつ厳密にその上に位置する「全体性」を表現することが可能になり、矛盾が生じる。^{[ 8 ] [ 5 ]}

ジラールの1972年の矛盾結果により、十分に強い「すべてのタイプのタイプ」原理は一貫性と両立しないことが明確になった。^{[ 2 ] [ 5 ]}この観察は、マルティン＝レーフ型理論の初期の定式化にも影響を与えた。マルティン＝レーフは、すべてのタイプのタイプを主張する初期の強い非述語的公理が「ジャン＝イヴ・ジラールによって矛盾につながることが示された後、放棄せざるを得なかった」と述べている。^{[ 6 ]}後続のシステムは通常、宇宙を階層化することによってこれを回避している（例：${\displaystyle \mathrm {タイプ} _{0}:\mathrm {タイプ} _{1}:\mathrm {タイプ} _{2}:\cdots }$）または非予測性に対するその他の制約によって。^{[ 5 ]}

• ジラールのパラドックス
• 純粋型システム
• ラムダキューブ
• 宇宙（型理論）
• マルティン＝レーフ型理論
• ブラリ＝フォルティのパラドックス

• Barendregt, Henk (1992). "型付きラムダ計算". Abramsky, Samson; Gabbay, Dov M.; Maibaum, Thomas SE (編) 『コンピュータサイエンスにおける論理学ハンドブック』第 2巻、Oxford University Press、pp. 117–309。 
• Howe, Douglas J. (1987).ジラールのパラドックスの計算上の挙動（技術報告書）。コーネル大学、コンピュータサイエンス技術報告書。2026年3月1日取得。