A Naive Encoding of Russell's Paradox in Type Theory

技術的要約：型理論におけるラッセルのパラドックスの素朴なエンコーディング

問題提起
「型の中の型」（$U : U$）システムの不整合性は、ジラールのパラドックス（ブラーリ＝フォルティのパラドックスの型論的アナロジー）を通じて確立されているが、ラッセルのパラドックスを型理論へ直接エンコードする手法はそれほど一般的ではない。コカンドによるW型を用いた、パラドックス的な集合に対応する木を構成する手法などの既存のアプローチは、帰納的型に依存している。本論文は、帰納的型に頼ることなく、単一の宇宙、シグマ型、および同一性型のみを用いて、ラッセルのパラドックスを直接エンコードする手法を提案することで、この空白を埋めるものである。

手法
構成は、$U : U$ を満たす単一の宇宙 $U$ を持つ型理論内で行われる。手法は以下のステップに従う：

1. 集合の宇宙 ($V$) の定義:
   著者は、「すべての集合の集合」（より正確には、すべての型の部分集合）を表す型 $V$ を、依存和（シグマ型）として定義する：
   $$V := \sum_{A:U} (A \to U)$$
   ここで、$V$ の元は、型 $A$ と述語 $P$ のペア $(A, P)$ である。このようなペアを $\{x : A \mid P(x)\}$ と表記する。

2. 所属 ($\in$) の定義:
   パラドックスを扱うためには、所属関係 $(\in_A) : A \to V \to U$ が必要である。所属関係の左辺（$A$）と、右辺の集合の基礎となる型（$B$）が異なる場合があるため、強制変換（coercion）メカニズムが必要となる。

   • 強制変換: 著者は、型 $A$ と $B$ の間の移動を、型 $A$ と $B$ の同一性の証明 $h : \text{Id}_U(A, B)$ を用いた依存パターンマッチングによって定義される coe を用いて定義する。
   • 同一性の証明: 強制変換の振る舞いに関する coe-eq の定義は、同一性証明の一意性 (UIP)（公理Kと同値）に依存している。本文では、外延型型理論（extensional type theory）では明示的な強制変換の定義なしに直接輸送が可能であるが、ここで用いられる内延型（intensional）のアプローチでは、輸送が期待通りに動作することを保証するために UIP が厳密に必要であると述べている。
   • 所属の定義: 所属関係は次のように定義される：
     $$a \in_A \{x : B \mid P(x)\} := \sum_{h: \text{Id}_U(A, B)} P(\text{coe}(h, a))$$
     これにより、集合が所属関係の両側に現れることが可能となり、これがパラドックスの前提条件となる。

3. パラドックス的な集合 ($R$) の構成:
   ラッセルの集合は次のように定義される：
   $$R := \{x : V \mid x \notin x\}$$
   ここで $x \notin x$ は $x \in x \to \bot$ として定義される。

4. 矛盾の導出:

   • 補題 1 ($R \notin R$): $R \in R$ と仮定すると（これはパス $h$ と証明 $p$ を含むシグマ型へと展開される）、証明は coe-eq（UIPに依存）を用いて $p$ の型を書き換える。この書き換えにより、仮定が $R$ の定義との矛盾へと変形され、$R \notin R$ が証明される。
   • 補題 2 ($R \in R$): 補題1の結果を用いて、反射的なパスと $R \notin R$ の証明をペアリングすることにより、$R \in R$ 型の項を構成する。
   • 結果: $R \in R$ と $R \notin R$ の両方の証明が同時に存在することは、矛盾 ($\bot$) を導き出し、システムの不整合性を実証する。

主要な貢献

• 直接的なエンコーディング: 本論文は、$\Pi$-型、$\Sigma$-型、および同一性型を用いて、ラッセルのパラドックスを直接形式化できることを提供し、コカンドの木によるパラドックスのような帰納的型を用いたエンコーディングを回避している。
• 構造的分析: 著者は、様々なパラドックス（ジラール、フルケンス、コカンドの木によるパラドックス）を統一する一般的な構造（$V$、intro、match、および $\beta$-等価性）を特定している。本論文は、intro が集合抽象として定義され、match が所属として定義されるとき、ラッセルのパラドックスがこの構造に適合することを示している。
• 簡略化: 他のパラドックスでよく見られる複雑な $P_2 U$（宇宙の部分集合）の構造を避けることで、構成がより直感的で理解しやすいものとなっている。

結果と限界
構成は、型の中の型システムにおいて矛盾を導出することに成功している。しかし、論文は決定的な依存関係について明記している：この証明は UIP（公理K） に依存している。したがって、この特定のエンコーディングは、UIPが拒絶されるホモトピー型理論（HoTT）では形式化できない。この構成は、宇宙チェックを無効にした状態で Agda および Rocq プローバで検証されている。

意義
本論文は、UIPが仮定されるならば、標準的な構成を用いて型理論におけるラッセルのパラドックスを素朴にエンコードすることが可能であることを主張している。これは、帰納的型に基づいたパラドックスに対する代替案を提示しており、不整合性が $U:U$、シグマ型、および強い同一性の原理（UIP）の組み合わせから生じることを強調している。本研究は、ラッセルのパラドックスと他の型論的な不整合性との構造的な類似性を明らかにし、それらが宇宙の導入規則と除去規則の統一的な視点を通じて捉えられることを示している。