Hurkens のパラドックス

設定

この付録を通して、カーネルの宇宙は単一の宇宙 $\mathsf{Type}$ に置き換え、T-Sort と T-Pi の代わりに次の二つの規則を使う。

それ以外はすべて変わらず、T-Lam、T-App、T-Conv、代入、$\beta$ 簡約はそのままである。目標は次を満たす閉じた項 $t_{\mathrm{H}}$ である。

このような項は、$t_{\mathrm{H}}\;C : C$ なので、あらゆる命題 $C$ を証明する。

この構成は Girard によるもので、集合論の Burali-Forti のパラドックスを $\mathsf{Type} : \mathsf{Type}$ をもつ型理論に移植したものである [Girard 1972]。以下に示す項は Hurkens による簡略版 [Hurkens 1995] で、1 ページに収まり、$\Pi$、$\lambda$、適用以外は何も使わない。

型理論における冪集合

関数 $p : S \to \mathsf{Type}$ は $S$ 上の述語、言い換えれば $S$ の部分集合と読み、$p\;x$ に証明がある要素 $x$ がその元である。そのような述語すべての型が $S$ の冪集合（power set）である。

これを 2 回適用した $\wp\wp S = (S \to \mathsf{Type}) \to \mathsf{Type}$ は、$S$ の部分集合の族の型である。

集合論では、Cantor の定理により $\wp S$ は常に $S$ より真に大きいので、どんな集合も自分の冪集合の複製を含まず、二重冪集合ならなおさらである。パラドックスは、これに反して $\wp\wp U$ の複製を含む型 $U$ の上に組み立てられる。すなわち、$U$ の部分集合の族を $U$ の一つの要素に詰め込む関数 $\tau : \wp\wp U \to U$ と、それを再び取り出す関数 $\sigma : U \to \wp\wp U$ がある。型

は、$\mathsf{Type}$ 全体にわたって量化することでこれを実現する。$\mathsf{Type}$ にわたって量化しながら $U$ 自身が $\mathsf{Type}$ の元であることこそ、$\mathsf{Type} : \mathsf{Type}$ が許し、第 13 章 の階層が禁じるものである。

項

以下の略記はその場で展開され、カーネルが見るのは $\Pi$、$\lambda$、変数、適用だけである。$\varphi \to \bot$ を $\neg\varphi$ と書く。

これらの略記を使うと、型 $\bot$ をもつ項は次のようになる。

形は適用であり、$h_0$ を束縛する $\lambda$ が、（最後の行で）$h_0$ の期待する型の引数に適用されている。内部では $h_0$ が二つの引数、$\Delta$ と $\Delta$ についての証明に適用され、その結果がさらにもう一つの引数に適用される。すべて以下で説明する。

項の仕組み

詰め込みと取り出し。 二つの関数 $\tau : \wp\wp U \to U$ と $\sigma : U \to \wp\wp U$ は、この議論に必要な程度には互いに逆である。定義を展開して $\beta$ 簡約すると、任意の $t : \wp\wp U$ と $p : \wp U$ について次が得られる。

この等式は公理ではなく計算であり、$t_{\mathrm{H}}$ のいくつかの箇所で T-Conv を通してカーネルに使われる。

$U$ 上の順序。 $\sigma\;x\;p$ を「述語 $p$ は $x$ より下のすべてについて成り立つ」と読むと、$U$ に順序のようなものが入り、述語と要素について二つのことが言える。

• 述語 $p : \wp U$ が帰納的であるとは、$x$ より下のすべてについて成り立つなら $x$ についても成り立つこと、すなわち $\tPi{x}{U}{\sigma\;x\;p \to p\;x}$ である。
• 要素 $x : U$ が整礎（well-founded）であるとは、すべての帰納的述語が $x$ について成り立つこと、すなわち $\tPi{p}{\wp U}{(\tPi{x}{U}{\sigma\;x\;p \to p\;x}) \to p\;x}$ である。

要素 $\Omega$ は、すべての帰納的述語からなる族を詰め込んだもので、「すべての整礎な要素の集まり」の役を演じるように作られている。Burali-Forti のパラドックスでは、これはすべての順序数の集合にあたり、それ自身が順序数であり、したがって自分自身の元であり、したがってすべての順序数が整礎であるにもかかわらず整礎でない。

三つの材料。 $t_{\mathrm{H}}$ を下から上へ読む。

1. 最後の行 $\tLam{p}{\wp U}{\tLam{h_1}{\cdots}{h_1\;\Omega\;(\tLam{x}{U}{h_1\;(\tau\;(\sigma\;x))})}}$ は、$\Omega$ が整礎であることを証明する。その型は $\tPi{p}{\wp U}{(\tPi{x}{U}{\sigma\;x\;p \to p\;x}) \to p\;\Omega}$ で、これは $h_0$ の型なので、$h_0$ は「$\Omega$ は整礎である」を表す。
2. 述語 $\Delta\;y$ は「$y$ は自分自身より下にない」と言っている（厳密には $\tau\;(\sigma\;y)$ について述べているが、上の等式によりこれは $y$ と同じように振る舞う）。$h_0$ の第二引数、$\tLam{x}{U}{\tLam{h_2}{\cdots}{\cdots}}$ で始まる長い $\lambda$ は、$\Delta$ が帰納的であることを証明するので、$h_0\;\Delta\;(\cdots) : \Delta\;\Omega$、つまり $\Omega$ は自分自身より下にない。
3. 残りの引数 $\tLam{p}{\wp U}{h_0\;(\tLam{y}{U}{p\;(\tau\;(\sigma\;y))})}$ は、$\Omega$ が自分自身より下にあることを、$\Omega$ の整礎性を詰め込みの等式で変換した述語に適用することで証明する。

$\Delta\;\Omega$ は「$\Omega$ は自分自身より下にある」の否定なので、ステップ 2 の結果をステップ 3 の結果に適用すると型 $\bot$ の項が得られる。

Type : Type が使われる場所

$t_{\mathrm{H}}$ の型付けの各ステップは、一つを除いてすべて普通のものである。$\sigma = \tLam{s}{U}{s\;U\;\tau}$ では、変数 $s : U$ が型 $U$ 自身に適用され、$s$ の型は $\tPi{X}{\mathsf{Type}}{\cdots}$ で始まるので、T-App は $U : \mathsf{Type}$ を要求する。ところが $U$ は $\mathsf{Type}$ にわたって量化する $\Pi$ 型であり、宇宙の階層をもつ体系では、そのような型は量化対象の宇宙より一つ上のレベルに属する。

第 13 章 の T-Pi 規則のもとでは、$U$ はよくても $\Sort{(u+1)}$ に属し、決して $\Sort{u}$ には属さない。したがって $s\;U$ には型が付かず、$\sigma$ は書けず、構成全体がこの一つの適用で崩れる。$U$ の本体は $(\wp\wp X \to X) \to \wp\wp X$ で、その結果 $\wp\wp X$ は宇宙への関数型であって命題ではないため、$\mathrm{imax}$ は $U$ を $\Sort{0}$ に置かず、$\Sort{0}$ の非述語性が扉を開け直すこともない。Coquand は、最下層に非述語的な宇宙が一つあるだけなら整合的であることを示した [Coquand 1988] が、Hurkens の項は、非述語的なレベルが二つあればもう多すぎることを示している [Hurkens 1995]。

カーネルで再現する

カーネルがこの項を受理し、また拒否する様子を自分で確かめられる。変更すべき規則は T-Sort だけで、これは src/typecheck.rs の infer にある Term::Sort(u) の場合分けで実装されている。

// T-Sort、出荷時の形: どの宇宙も一つ上の宇宙に属する。
Term::Sort(u) => Ok(Term::Sort(u.checked_add(1).ok_or("universe overflow")?)),

右辺を Ok(Term::Sort(*u)) に置き換えて $\Sort{0} : \Sort{0}$ とし、全体を通して $\Sort{0}$ を $\mathsf{Type}$ として使う。ほかに変更は要らず、すべての型が $\Sort{0}$ にあれば、$\mathrm{imax}$ 付きの T-Pi 規則はすでにあらゆる $\Pi$ 型に $\Sort{0}$ を割り当てており、これがこの付録の第二の規則にほかならない。この 1 行の変更で、infer は $t_{\mathrm{H}}$ に対してちょうど $\tPi{p}{\Sort{0}}{p}$ を返す。変更前のカーネルは、上で予告したとおり、$\sigma$ の中の適用 $s\;U$ で型の不一致を報告してこの項を拒否する。

正規形が存在しない理由

第 14 章 は、型 $\tPi{P}{\Sort{0}}{P}$ をもつ正規な閉じた項が存在しないことを示して、本来の体系の整合性を証明する。その証明のうち正規項の形を分析する部分は強正規化を使わず、$\mathsf{Type} : \mathsf{Type}$ のもとでもそのまま通る。したがって、もし $t_{\mathrm{H}}$ に正規形があれば、それは型 $\bot$ をもつ閉じた正規項になるが、そのようなものは存在しえない。型保存性も成り立つので、簡約によって型 $\bot$ から逃れることもできない。残る可能性はただ一つ、$t_{\mathrm{H}}$ が永遠に簡約され続けることであり、強正規化が破れ、それとともに型検査器の停止性も失われる。Girard のパラドックスは論理上の欠陥であるだけでなく計算上の欠陥でもあり、第 13 章 の宇宙の設計が、論理と同じくらいアルゴリズムにとっても重要である理由はここにある。