New Foundations の無矛盾性 ― Lean を用いて証明された難解な数学的証明

Here is a summary of the key points from the given article, organized using Markdown:

New Foundations 集合論の無矛盾性証明

• 1937年に Quine が提案した "New Foundations(NF)" 集合論の無矛盾性を、Randall Holmes が 2010年以降証明したと主張してきた
• このリポジトリでは、対話型定理証明器 Lean を使って Holmes の証明の難しい部分を検証することで、NF が実際に矛盾を持たないことを証明している
• 証明は現在完了しており、定理の命題は ConNF/Model/Result.lean で見つけられる

目標

• NF は Tangled Type Theory(TTT) が無矛盾であるとき、そしてそのときに限って無矛盾であることが知られている
• Lean で TTT のモデルを形式的に構成することで NF が無矛盾であることを証明する
• Holmes の複数の版の証明をもとにしているが、Lean の型理論と両立するように多くの変更と追加が行われている
• このプロジェクトは、Lean で書かれたコミュニティ数学ライブラリである mathlib に依存しており、濃度や群などに関する馴染みのある結果を自分で直接証明せずに利用できる
• Lean の信頼できるカーネルによって mathlib とこのプロジェクトのすべての定義と定理は検証されているが、Lean は定義や定理の説明が意図された英語の説明と一致するかどうかを確認できないため、このプロジェクトのコードから結論を導く際には英語との対応に注意する必要がある

もつれた型理論(TTT)

• TTT は、等価関係 = と属する関係 ∈ を持つ多ソート集合論である
• ソートは極限順序数 λ によって添字付けされ、λ の要素を型指数と呼ぶ
• x = y という式は x と y が同じ型のときに整形式であり、x ∈ y という式は x が y より小さい任意の型を持つときに整形式である
• TTT の公理の一つは、型 α の集合が β < α である任意の β 型の要素によって一意に決定されるという外延性である
• 例えば、型 α の二つの集合が異なるなら、任意の β < α に対してそれらは異なる β 型要素を持つことになり、この性質が TTT モデルの構築を難しくしている

戦略

• モデル構築には、おおよそ次の戦略を用いる:

  • 基本型の構成

    • λ を極限順序数、κ > λ を正則順序数、μ > κ を少なくとも κ の余終性を持つ強極限基数とする
    • κ より小さい集合を小さいと呼ぶ
    • レベル -1 において基本型という補助的な型を構成し、これは最終的にモデルの一部となるすべての型の下に位置する
    • この型の要素を原子と呼び（ZFU や NFU の意味での原子ではない）、μ 個の原子があり、κ サイズの litter に分割される

  • 各型の構成

    • 各型レベル α で、TTT の意図されたモデルのためのモデル要素の集まりを生成し、これをときに t-集合と呼ぶ
    • 許容置換と呼ばれる置換群を生成し、これらが t-集合に作用する
    • 属する関係は、許容置換の作用の下で保存される
    • 各 t-集合は、許容置換の作用の下で支えを持つように定められ、これはアドレスと呼ばれる小さな対象の集合であり、許容置換が支えのすべての要素を固定するときには常に、その t-集合も固定する
    • レベル α の各 t-集合には、β < α 型の優先的な拡張が与えられ、t-集合の要素からどの拡張が優先されているかを復元できる
    • こうした t-集合の他の下位型での拡張は β-拡張から推論でき、これによって TTT の外延性公理を満たせる

  • 各型の大きさの制御

    • 各型 α は、すべての型 β < α の大きさがちょうど μ であるという仮定（他の仮定に加えて）の下でのみ構成できる
    • レベル α における t-集合の集まりが少なくとも μ の濃度を持つことは容易に証明できるため、この集合の要素が高々 μ 個であることを示す必要がある
    • これは、許容置換の作用の下でのもつれに対する本質的に異なる記述がそれほど多くないことを示すことで可能になる
    • そのためには、許容置換を構成できるようにする技術的補題である作用の自由定理が必要となる
    • この節の主要な結果はここにある

  • 帰納法の仕上げ

    • 上の過程を再帰的に実行して、すべての型レベル α でもつれた型を生成できる
    • これは集合論では容易な段階だが、必要なさまざまな帰納法の仮定が相互に絡み合っているため、型理論では多くの作業を要する
    • その後、この構成が実際に TTT のモデルを生成すること、あるいは理論の有限公理化を満たすことを確認する
    • 私たちは NF の包括公理図式に対する Hailperin の有限公理化を TTT の有限公理化へ変換することを選び、その内容を結果ファイルで示している
    • しかし、この選択は任意であり、すでに整備された基盤を使って他の有限公理化も容易に証明できる

GN⁺ の意見

• この証明は、これまで非常に抽象的なレベルでしか知られていなかった NF 集合論の無矛盾性を形式的に証明したという点で非常に意義深い結果である。これは純粋数学的に重要であるだけでなく、証明支援ツールの発展と自動定理証明の実質的な前進を示す事例でもある
• Lean を用いた形式化作業は証明の正確さと完全性を保証する一方で、数学者にとって馴染みの薄い言語で書かれているため理解しにくい場合がある。証明の核心的なアイデアを自然言語で明確に説明する作業も並行して必要だろう
• TTT の奇妙な外延性公理がなぜ必要なのか、他の集合論とどのような関係にあるのかなど、背景理論についての直観的な説明もやや不足している。形式的証明だけでなく、哲学的・歴史的文脈に関する議論が補われれば、NF 理論への理解はさらに深まるだろう
• 構築されたモデルが標準的な ZFC 集合論のモデルとどのような関係にあるのか、NF の無矛盾性が他の公理系の無矛盾性とどのように結びつくのかといった今後の追加研究テーマも興味深い
• このような複雑な証明を Lean で形式化した事例は、他の数学分野における証明自動化の模範にもなりうる。従来は証明過程がよく知られていない定理を対象に同様の試みが進めば、数学界に大きな波及効果をもたらすことが期待される

[GN⁺]

Hacker Newsのコメント

• Leanを使った証明が誤っているリスクは非常に低い。しかしLeanのバグとは無関係に、ソフトウェア検証や数学で知られている問題として、結論を注意深く読み、実際に証明された内容と一致しているかを確認する必要がある。
• 今回の事例は、難解な証明の状態を解決するために証明支援系を用いた最初の事例のように見える。以前にも、信頼できないソフトウェアで処理された大規模な計算要素を含む既存の証明を検証したプロジェクトはあったが、今回は結果の認識論的地位が数学界で不確かだった最初の事例である。
• CoqとLeanの根本的な違い、および同種の論理の上で動作しているのかどうかについて疑問が提起されている。関連する議論では、理解しづらい内容も言及されている。
• Leanの支持者は、Leanが優れた証明方法であるという点を強調しすぎる傾向がある。Leanはあくまで別の証明手法にすぎず、プログラミング言語およびシステムとして独自のバグを持ち、他人が書いたさまざまなライブラリのスタックに大きく依存している。
• Leanが証明は良いものだと言った、という表現よりも、書かれた証明が人間の数学者によって検証され、その証明がLeanに変換され、そこで再び検証された、と表現するほうがより正確で誠実だろう。Leanが唯一の黄金の検証を提供するという説明は正確ではないし、そのように述べる説明も見たことがない。
• 「New Foundations」の集合論の定式化が、他の定式化と比べて何が特別または新しいのかについて、数学科の学部生や工学系の専門家が読める形で大まかな説明を求めている。
• このようなアプローチが最終的に協調的な証明や「バグ修正」につながり、数学をGitHub上のコードに似たプロセスにしていくのかと疑問を呈している。
• ゲーデルの定理によれば、十分に強力なあらゆる体系は自分自身の無矛盾性を示せないとされるが、これについて質問している。
• mathlibプロジェクトを追い続けたいが時間がない。非常に受動的な形で参加する方法があるのか気にしている。