💻 computer science

Four Paradoxes and a Proof Assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library

本論文は、coq-paradoxes ライブラリに実装された 4 つのパラドックスを分析し、それらが一貫性を維持するためにシステムが特定の構成を拒否せねばならない正確な理由を示すことによって、それらが不純性、大規模消去、および宇宙の制約に関する Rocq カーネルの必要な設計境界をどのように集合的に定義するかを明らかにする。

原著者： Bernardo Alonso

公開日 2026-05-28

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Bernardo Alonso

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

非常に厳格で非常に賢いロボット建築家「Rocq」がいると想像してください。その仕事は、安全で整合性が保証された論理構造（数学的証明）を構築することです。それは決してクラッシュせず、決して嘘をつかず、決して矛盾を生み出しません。

しかし、ロボットが正しく仕事をしていることをどうやって知ることができるのでしょうか？単にその構築過程を見守るのではなく、あなたはそのロボットを欺こうとします。一見すると機能するように見えるが、実際には建物全体を崩壊させる隠された罠を含んでいる設計図を、そのロボットに与えてみようとします。

この論文は、coq-paradoxesと呼ばれる「罠の設計図」の特別なライブラリについて述べています。そこには、ロボットの論理を破ろうとする 4 つの具体的な試みが含まれています。この論文は、これらが単なるパズルや好奇心の対象ではなく、実際にはロボットの安全性マニュアルが逆から書かれたものであると主張しています。これらは、災害を防ぐためにロボットのルールがどこで引かれているかを正確に示しています。

以下に、簡単なアナロジーを用いた 4 つの罠と、それらが私たちに教えることを解説します。

1. ブラリ＝フォルティの罠：「自分自身を含む箱」

罠：すべての本に、その内容自体を記述するラベルが貼られている図書館を想像してください。このパラドックスは、その図書館のすべての本（マスターカタログ自身も含む）をリストする「マスターカタログ」を作成しようとします。
問題： カタログが本であれば、それは自分自身をリストしなければなりません。しかし、自分自身をリストすれば、図書館のサイズが変わり、それがカタログを変え、さらに図書館を変える……これはサイズに関するルールを破る無限ループです。
教訓： ロボット（Rocq）にはユニバース階層に関するルールがあります。「同じサイズの箱の中に箱を入れることはできない」というものです。ロボットは、数学的に「内側の箱」は「外側の箱」よりも小さくなければならないと述べているため、マスターカタログの構築を拒否します。この罠は、ロボットが無限ループを防ぐために厳格なサイズ制限を正しく強制していることを証明しています。

2. ディアコネスクの罠：「魔法のコイントス」

罠：同率の選択肢から「勝者」を選ぶことができる機械（一卵性双生児のグループから代表者を選ぶような）があると想像してください。パラドックスはこう言います。「この機械を私に与えれば、実際に答えを知っていなくても、あらゆるはい/いいえの質問（『空は青いのか？』など）の答えを強制的に引き出させることができる」と。
問題： 構築的システム（推測するのではなく、答えを構築しなければならないシステム）において、同率の選択肢から勝者を選ぶ機械を持つことは、あまりにも強力すぎます。それは密かに、まだ証明できないことさえも、システムに「A が真であるか、A が偽であるかのどちらか」を受け入れさせます。
教訓： ロボットには大規模消去に関するルールがあります。「数字のグループから勝者を選ぶことはできるが、それを使って哲学的な真理を魔法のように決定することはできない」というものです。この罠は、ロボットがこの種の「魔法の選択」を許可した場合、私たちが知っていることと知らないことを区別するシステムの能力が誤って損なわれることを示しています。

3. レインズの罠：「存在しえない辞書」

罠：ありうるすべての定義が辞書内の単語となっている辞書を作成しようとすると想像してください。パラドックスは、ありうるすべての文を単一の単語にマッピングする「普遍的な辞書」を構築しようとします。
問題： これは、世界全体の地図を一枚の郵便切手に収めようとするようなものです。すべての可能な論理的命題を単一の種類のオブジェクトに圧縮しようとすれば、矛盾が生じることが数学的に証明されます（すべての可能なリストをリストできないのと同様です）。
教訓： ロボットには非予測性（定義が属する全体を参照することを許可する）に関するルールがあります。ロボットは「命題」（単純な真偽の文）についてはこれを許可しますが、それ以外の場所では明確な線引きをします。この罠は、ロボットが複雑な型に対してこの種の「普遍的な辞書」を許可した場合、システム全体が崩壊することを示しています。

4. ハルケンスの罠：「自己言及の鏡」

罠：これが最も複雑なものです。反射が反射を反射し、それが永遠に続く鏡を想像してください。パラドックスは、小さなオブジェクト（真/偽のようなブーリアン値など）を見て、それを使って大きなオブジェクト（型の完全なユニバースなど）を定義し、その大きなオブジェクトを使って再び小さなものを定義できるようなシステムを構築しようとします。
問題： これは、大きなものと小さなものを組み合わせて論理的なパラドックスを生み出す「自己言及ループ」です。蛇が自分の尾を食べるようなものですが、その尾は蛇自身の体でできています。
教訓： ロボットには集合における非予測性に関するルールがあります。「単純な真偽の文については自己言及が可能だが、それを大きく複雑な型と混ぜることはできない」というものです。この罠は、ロボットがこの混合を許可した場合、システムを整合的に保つことが不可能になることを証明しています。

全体像：なぜこれが重要なのか

この論文は、これら 4 つのファイルを「失敗した数学」として見るべきではないと主張しています。代わりに、これらをロボットの成功の証拠として見るべきです。

否定的仕様： これらのファイルを犯罪者の「指名手配書」と考えてください。犯罪者は「不整合」です。その手配書は犯罪者自身を示すのではなく、犯罪者が現れる正確な条件を示しています。
境界線： ロボット（Rocq）は砂に 3 つの目に見えない線を引いています。
1. サイズ制限： 同じサイズの箱の中に箱を入れることはできません。
2. 選択制限： 単純な選択を使って複雑な真理を強制することはできません。
3. 反射制限： 単純な自己言及を複雑な型と混ぜることはできません。

ユーザーがこれらの線のいずれかを越える構造を構築しようと試みるたびに、ロボットはそれを止めさせます。これら 4 つのファイルは、ロボットが設計された通りに、最終的に崩壊するものを構築することを拒否していることの証明です。

要約すれば、この論文はこう述べています。「私たちはこれらの 4 つの巧妙なトリックでシステムを壊そうとしました。システムは『ノー』と言いました。その『ノー』こそがシステムの中で最も重要な部分であり、それがすべてを安全に保っているのです。」

技術的サマリー：4 つのパラドックスと証明支援系

問題定義
本論文は、Rocq 証明支援系（旧 Coq）の基盤となる型理論である帰納的計算（Calculus of Inductive Constructions: CIC）の基礎的限界を扱っている。CIC の無矛盾性はよく確立されているが、無矛盾性を防ぐための具体的な設計決定、特に非予測性（impredicativity）、宇宙の制約、および大規模除去（large elimination）に関するものは、しばしば抽象的な工学的制約として扱われる。Rocq とともに配布される「coq-paradoxes」ライブラリには、Rocq カーネルによって拒否される仮定に依存する「偽（False）」の 4 つの機械化された導出（ブルアリ＝フォルティ、ディアコネスク、レイノルズ、およびフルケンス）が含まれている。中心的な問題は、これらの導出を単なる歴史的な珍事や孤立した不整合としてではなく、カーネルが健全性を維持するためにどこで線を引く必要があるかを正確に画定する「負の仕様（negative specification）」として解釈することである。

手法
本論文では、「coq-paradoxes」ライブラリ内のソースコードの精読を行い、特に以下の 4 つのファイルを分析する：BuraliForti.v、diaconescu.v、Reynolds.v、およびHurkens_Set.v。手法は以下の通りである：

共有メカニズムの分解：Logics.v を分析し、複数のパラドックスで使用される到達可能性述語（ACC）および整礎性のインフラストラクチャを理解する。
導出の追跡：各ファイルの論理的ステップを追跡し、矛盾に至る特定の仮定（例えば、関係の普遍型、選択原理、または Prop から単一の命題への単射）を特定する。
カーネル拒否との対応付け：形式化における矛盾の点を、その構築のコンパイルを防止する Rocq カーネルの特定のメカニズム（宇宙演算、除去規則、または非予測性チェック）と関連付ける。
設計決定の統合：発見事項を統合し、カーネルの振る舞いを支配する 3 つの統一された境界条件を抽出する。

主要な貢献と結果

本論文は 4 つの特定のパラドックスを分析し、特定の設計選択が変更された場合、それぞれが型理論においてどのように異なる脆弱性を露呈するかを実証する：

ブルアリ＝フォルティのパラドックス（BuraliForti.v）：
- メカニズム：関係の普遍型 $A_0$ と、関係を $A_0$ の要素に写す単射 $i_0$ を仮定する。これにより、自身に埋め込まれる「すべての順序数の順序数（ $\Omega$ ）」の構築が可能になる。
- カーネル拒否：このパラドックスは、 $A_0$ を自身でインスタンス化することに依存している。Rocq カーネルは、型が自身の像を含むことを防ぐために、厳密な宇宙の階層化（ $Type_j < Type_i$ ）を強制する。この構築は、内部型に必要な宇宙レベルが外部型と少なくとも同じ大きさでなければならないため、カーネルの累積的制約に違反し、「宇宙の不整合（Universe Inconsistency）」エラーをトリガーする。
- 結果：固定点矛盾につながる自己言及的な型定義を防ぐための宇宙階層制約の必要性を確立する。
ディアコネスクのパラドックス（diaconescu.v）：
- メカニズム：命題 $P$ によって定義される bool 上の同値関係に対して、選択公理の型付きバージョン（Tchoice）を使用する。選択関数 $f: bool \to bool$ は、 $f(\text{true})$ と $f(\text{false})$ を比較することによって $P$ を決定するために使用される。
- カーネル拒否：この議論は、Prop における存在証明から Set 内の計算的決定（関数）を抽出する。これは Prop から Set への「大規模除去」を構成する。
- 結果：Set における選択公理の許可（または Prop から Set への大規模除去）が、構成主義的システムに排中律（LEM）を強制することを示す。カーネルは、計算レイヤーへの古典論理の導入を防ぐために、大規模除去を制限する。
レイノルズのパラドックス（Reynolds.v）：
- メカニズム：システム F に集合論的モデルが存在しないというレイノルズの結果を再定式化する。Heyt（単一の命題）への Prop の単射 $I: Prop \to Heyt$ を仮定し、関手 $\Phi$ に対する前初期代数（チャーチ符号化）を構築する。ラヴェールの固定点定理を用いて否定の固定点を導き、False に至る。
- カーネル拒否：この構築は Prop の非予測性（Prop 内ですべての命題について量化すること）に依存している。しかし、このパラドックスは Prop から単一の命題への単射を必要とし、これは論理的矛盾に到達する前に、宇宙の理由によりカーネルによって拒否される。
- 結果：Prop における非予測性の役割を浮き彫りにする。Prop は非予測的であるが、カーネルはカンターの対角線論法が命題の宇宙を崩壊させることを可能にする特定の構造的単射を防止する。
フルケンスのパラドックス（Hurkens_Set.v）：
- メカニズム：ジルダールのパラドックスの簡略化であるフルケンスの適応版である。Prop と bool の間の（二重否定を介した）リトラクトを仮定し、Set の非予測性（有効化された場合）を大規模除去と組み合わせて、False に至る自己言及的な整礎関係を構築する。
- カーネル拒否：このパラドックスは、Set における非予測性と、命題的内容からブール値を抽出する大規模除去の両方を必要とする。デフォルトの Rocq カーネルは Set を予測的に保ち、Prop からの大規模除去を制限する。
- 結果：Set における非予測性と大規模除去の組み合わせが、古典論理（LEM）と矛盾することを示す。Set を予測的に保ち、除去を制限するというカーネルの決定が防衛策である。

意義と主張

本論文は、「coq-paradoxes」パッケージが Rocq カーネルの負の仕様として機能すると主張する。単に不整合を列挙するのではなく、このパッケージは失敗した例による形式証明を通じて、カーネルの健全性を提供する。

3 つの境界条件：本論文は、4 つのパラドックスをカーネルによって強制される 3 つの具体的な設計決定に統合する：
1. 宇宙階層：固定点を作成する形で型が自身について量化することを防ぐ（ブルアリ＝フォルティ）。
2. 非予測性の配置：非予測的量化を Prop（および条件付きで Set）に限定し、レイノルズおよびフルケンスの矛盾を防止する。
3. 大規模除去の規律：命題的証明から（bool や Set 内の関数などの）計算的内容を抽出することを制限し、ディアコネスクおよびフルケンスの矛盾を防止する。
メタ数学的役割：本論文は、このパッケージが、文書化しているシステム内部に書かれたユニークなメタ数学であると主張する。これは応用のための定理を証明するのではなく、特定の仮定の非充足可能性を証明する。カーネルの「拒絶」は、その場限りの修正ではなく、宇宙演算や除去規則などの均一なポリシーの結果として示される。
結論：その意義は、Rocq カーネルがこれらの構築のコンパイルを拒否することが恣意的ではなく、CIC の一貫性を維持するために必要な正確な構造的メカニズムであることを実証することにある。このパッケージは、カーネルの設計決定が「正当な理由」で行われていることを検証し、実質的にシステムの外側から内側へと境界を描き出している。