New Foundationsの無矛盾性 ― Leanで検証された難解な数学証明
(leanprover-community.github.io)- 1937年にQuineが提案した集合論 New Foundations の無矛盾性証明のうち、難しい部分がLeanで検証されており、核心となる定理は
ConNF/Model/Result.leanにまとめられている - アプローチは、New Foundationsと Tangled Type Theory（TTT） の無矛盾性が同値であるという結果を利用し、Lean内でTTTモデルを形式的に構成するもの
- TTTモデルは、低い型の要素によって集合が一意に決まらなければならない 外延性 のため、構成の難度が高くなる
- モデル構成には基底型、t-set、許容可能な置換、小さなsupport、preferred extensionが使われ、型のサイズを μ で制御するにはfreedom of action theoremが必要になる
- Leanカーネルは形式化された証明を検査するが、形式文が意図した英語の意味と一致するかまでは保証しないため、結果の解釈には翻訳の確認が必要
Leanで完成したNew Foundationsの無矛盾性検証
- 1937年にQuineは集合論 New Foundations を提案し、Randall Holmesは2010年からその無矛盾性証明を持っていると主張してきた
- このプロジェクトは、Holmesの証明の難しい部分を対話型定理証明器 Lean で検証し、New Foundationsの無矛盾性を示すことに焦点を当てている
- 証明は完了しており、定理文は
ConNF/Model/Result.leanで確認できる - 関連資料もあわせて提供されている
ローカルでコードを実行する
- ローカル実行は、elanをインストールしてリポジトリをクローンしたあと、リポジトリのルートで次のコマンドを実行すればよい
lake exe cache get
- その後、コードはVisual Studio Codeのようなエディタで確認でき、コマンドラインでは
lake buildで直接コンパイルできる
New FoundationsとTTTのつながり
- New Foundationsは Tangled Type Theory（TTT） が無矛盾であるとき、かつそのときに限り、無矛盾であることが知られている
- 関連する結果は Holmesのtheorem 1 にある
- プロジェクトではLeanでTTTモデルを形式的に構成し、それにより紙上の結論としてNew Foundationsの無矛盾性、すなわち Con(NF) を得る
- 作業はHolmesの複数の証明文書を基に進められたが、Leanの型理論に合わせるため、多くの変更と追加が必要だった
Lean検証の基盤と解釈上の注意点
- プロジェクトはLeanで書かれたコミュニティ数学ライブラリ mathlib に依存している
- mathlibのおかげで、基数や群のようなよく知られた結果をプロジェクト内で再証明せずに利用できる
- mathlibとこのプロジェクトの定義・定理は、Leanの trusted kernel が検査する
- Leanカーネルは、構成された証明が実際に正しいかを計算的に検証する
- ただしLeanは、形式文が意図された英語の等価物と一致しているかまでは確認できない
- コードから結論を引き出す際には、英語の記述と形式文の間の 翻訳 を注意深く見る必要がある
Tangled Type Theoryの構造と難点
- TTTは等号
=と包含関係∈を持つ 多ソート集合論 である - ソート（sort）は極限順序数λで添字付けされ、λの要素は型指数と呼ばれる
- 式の形成条件は型によって制限される
x = yはxとyの型が同じときに整形式となるx ∈ yはxの型がyの型より低いときに整形式となる
- 核心的な難点はTTTの 外延性 公理から生じる
- 型αの集合は、任意の型β < αの要素によって一意に決まらなければならない
- 例えば型αの2つの集合が異なるなら、すべてのβ < αについて、互いに異なる型βの要素を持たなければならない
- この要求条件により、TTTモデルの構成は単純な集合論モデルの構成より難しくなる
モデル構成の主な段階
-
基底型の構成
- λを極限順序数、κ > λを正則順序数、μ > κを共終数が少なくともκである強極限基数とする
- サイズがκより小さい集合を small と呼ぶ
- すべてのモデル型の下にある補助型であるレベル-1の base type をまず構成する
- この型の要素はatomsと呼ばれるが、ZFUやNFUの意味でのatomではない
- atomはμ個あり、サイズκの litters に分割される
-
t-setと許容可能な置換
- 各型レベルαでTTTモデルの要素となるコレクションを作り、これを t-set と呼ぶ
- 同時に、t-setに作用する置換群である allowable permutations を構成する
- 包含関係はallowable permutationsの作用の下で保存される
- 各t-setはallowable permutationsの作用に対する support を持つように定められる
- supportはaddressesと呼ばれる対象の小さな集合である
- あるallowable permutationがsupportのすべての要素を固定すれば、そのt-setも固定する
-
preferred extensionで外延性を合わせる
- 各レベルαのt-setは、β < αである何らかの型の preferred extension を持つ
- t-setの要素から、どのextensionを好むかを復元でき、他の低い型のextensionはそのβ-extensionから導かれる
- この構造がTTTの外延性公理を満たすために使われる
-
型サイズの制御
- 各型αは、すべてのβ < αの型のサイズが正確にμであるという仮定などがあって初めて構成できる
- レベルαのt-setコレクションのサイズが少なくともμであることは容易に証明できるため、高々μ個であることを示す必要がある
- そのために、allowable permutationsの作用の下で、tanglesの本質的に異なる記述が多くないことを示す
- この段階には、allowable permutationsを構成できるようにする技術的補題である freedom of action theorem が必要になる
- この節の主な結果は ConNF.mk_tSet にある
-
帰納の仕上げと公理の確認
- 上記の過程を再帰的に実行し、すべての型レベルαでtanglesの型を生成する
- 集合論では簡単な段階だが、必要な複数の帰納仮定が互いに絡み合っているため、型理論では多くの作業が必要になる
- その後、構成物がTTTのモデルであることを確認するため、この理論の 有限公理化 を満たすかを検査する
- プロジェクトはHailperinによるNF comprehension schemeの有限公理化をTTTの有限公理化へ変換して使用している
- 結果ファイルは results file にある
- この選択は任意であり、すでに構築されたインフラを使えば、他の有限公理化も容易に証明できる
1件のコメント
Hacker News のコメント
Lean による証明が間違っているリスクは非常に小さいと思う。
ただし Lean のバグとは無関係に、ソフトウェア検証でも数学でもよく知られたリスクがある。結論を正確に読んで、実際に必要な命題が証明されているか確認しなければならない。
Wilshaw の最終結論を注意深く読んだが、実際に証明すべきものを証明していると判断した。
論文も似た点を述べている。mathlib とこのプロジェクトのすべての定義と定理は Lean の信頼カーネルによって検査され、私たちが構成した証明が実際に正しいことを計算的に検証している。
しかし Lean は、定義や定理の命題が意図した英語表現と一致しているかどうかまでは確認できないため、このプロジェクトのコードから結論を引き出す際には、英語との翻訳に注意する必要がある。
私が言っている問題は、ライブラリに関する懸念ともつながっている。定義済みの概念を使う場合、その定義が正しいか、つまり本当に必要なことが証明されているかを確信しなければならない。
Wilshaw の形式化はライブラリを使ってはいるが、この反論には弱くない。証明されているのは、ある定義済み概念が一階論理式の特定のまとまりを満たすということであり、そのような式を満たす述語が存在すれば NF は無矛盾である。
もう一つのリスクは Lean 自体のバグである。定理証明器で前例がないことでもない 1。
偶然踏むのは難しいかもしれないが、3 のように不特定多数の人がステップを埋めていく大規模な共同作業はますます大きくなっている。誰かが発見したバグで一つのステップを埋めて妨害するような状況は、懸念に値するものになり得る。
基礎論の観点では、この証明が NF と Lean カーネルの間の等無矛盾性についての証明である点も重要である。Lean カーネル自体は人間がレビューしている。
機械化された定理証明器は、人間や他の外部システムを通じて注入された正しさの水準を保存する仕組みである。
私の勘違いでなければ、これは何年も曖昧な状態に残っていた難しい証明の位置づけを、証明支援器で整理した初の事例に見える。
Coq の四色定理のように、信頼されていないソフトウェアが大きな計算要素を担った既存の証明を検証したプロジェクトはあったが、より広い数学コミュニティにおいて結果の認識論的地位そのものが不確かだったケースは、今回が初めてのように思う。
Liquid Tensor Experiment も思い浮かぶ。
https://www.nature.com/articles/d41586-021-01627-2
https://leanprover-community.github.io/blog/posts/lte-final/
ケプラー予想と似た状況である（https://en.m.wikipedia.org/wiki/Kepler_conjecture）。
証明はすでに知られていたが、形式化されるまでは正しいかどうか確信できなかった。
次は abc 予想の番になりそうだ。
2012 年に証明されたと主張され、400 ページを超える論文がオンラインにあるが、その証明を受け入れている人は多くないようだ。
「New Foundations」集合論の形式化が、他の形式化と比べて何が特別または新しいのか、ざっくり説明してもらえるだろうか。
あるいは数学の学部生や工学系の専門家が読める説明リンクでもよい。
核心は普遍集合の存在だと思う。私の用途であるプログラミング言語の型システムでは、このような普遍集合が非常に有用である。
既存システムの累積宇宙や type-in-type のような各種の回避策には満足できない。その代わり、型シグネチャが階層化されているかだけを確認したうえで、型に数値的な段階があるという事実を忘れることができる。
基本的には、部分集合を選ぶのに使う述語が非常に軽量な型システムに従うことを要求する。「x は自分自身の要素ではない」というのは、合理的な型システムでは型付けのうまくいく問いではなく、とりわけ NF の「階層化可能性」の要求も満たさないため、自分自身を含まないすべての集合からなる集合、すなわちラッセルのパラドックスの集合を作ることはできない。
「階層化可能」の定義もそれほど複雑ではない。一方で ZF には、かなり場当たり的に見える公理／公理図式が八つある。
Coq と Lean の根本的な違いは何か、同じ種類の論理の上で動いているのかが気になって、この投稿を見つけた 1。
その議論はほとんど理解できなかったし、どちらも実際には使っていない。関連して、さらに説明できることや他の証明支援器との比較があれば聞きたい。
1 https://proofassistants.stackexchange.com/questions/153/what...
違いはあり、この議論も読む価値がある 1。
1 https://github.com/coq/coq/issues/10871
Lean の支持者たちは、少し表現が大げさなように思う。Lean は、しばしば暗に示されるような、より優れた証明方法ではなく、代替的な証明方式である。
Lean を学ぼうとすればすぐ分かるが、それ自体にバグがあり得るプログラミング言語でありシステムであり、他の人間が書いた複数のライブラリスタックに大きく依存している。そのライブラリには選択が入り込んでおり、抜けやバグもあり得る。
だから「Lean がその証明は良いと言った」というような表現には異論がある。より正確で誠実な言い方は、書かれた証明を人間の数学者たちが検証し、その証明を人間が Lean に翻訳して、そこでも検証した、ということだと思う。Lean が唯一の黄金の検証を提供するという言い方は、必ずしも正確ではないか、少なくともそうだという説明を見たことがない。副題の「ランドール・ホームズの証明のデジタル化」が最も正確な表現に思える。
Lean のような強力なシステムにおける機械検証済み証明は、人間だけが検証した証明よりはるかに優れていると思う。人間は驚くべき存在だが、退屈もするし、細部を見落とすこともある。
これは単なる理論上の主張ではない。人々はユークリッドの『原論』を2000年以上読んだ後で、ようやく欠けていた公理に気づいた。適切に動作する機械証明検証システムなら即座に露呈したはずの基本的なミスである。
出版された数学の証明も、後になって誤りだと判明することは多い。数学がますます精緻になるにつれ、人間がすべての段階を正しく検証することはますます難しくなっている。機械はまだ証明の生成では人間ほど優れていないが、検証に関しては比類がない。
Lean と「競合」するシステムもあるので、Lean が「唯一の真の道」だとは言わない。例えば Metamath も好きだ。ただし、これらのシステム間の「競争」には引用符が必要だ。それぞれ長所と短所が異なり、複数のシステムを好んだり、使ったり、貢献したりする人も多い。いずれも、人間には非現実的な厳密さで定理を検証できる。
バグがあり得るとしても、信頼すべきなのはカーネルだけだと理解している。
「他の人間が書いた複数のライブラリスタック」が mathlib を指しているなら、その言い方は正しくないように思う。mathlib のコードも結局、カーネルが処理するコードへコンパイルされるからだ。
ウェブサイトの論文ドラフト 0 もこの点を補強している。Lean は大きなプロジェクトだが、受理された証明が正しいことを保証するにはカーネルだけを信頼すればよい。タクティックが誤った証明項を出力したとしても、カーネルは証明を受理する前にその誤りを発見する機会を持つ。
違いは、Lean ではカーネルだけを信頼すればよいという点にある。それ以外はその上に構成されている。カーネルが健全なら、他のすべても健全である。
これは通常のプログラミング言語とは大きく異なる。通常の言語では、いつでもバグが入り得る。また、どんな補題にも誤りが含まれ得る数学とも大きく異なる。
定理証明器の素晴らしい点は、カーネルが正しいという前提の下では、誤った証明はコンパイルすらされないことだ。
証明に関しては、従来のソフトウェアのように実行時にだけ発生するバグはない。そもそも実行時というものがないからだ。
Lean を「普通の」プログラミング言語として使うこともでき、その場合は実行時バグのリスクがあるが、ここで問題にしているのはそういうことではない。
定理証明器を誤解している。これは「すべての抽象化は漏れる」というレベルの話ではない。ライブラリを信頼する必要はなく、カーネルだけを信頼すればよい。
カーネルを信頼することも些細なことではないが、非形式的な証明に比べれば大きな飛躍だ。非形式的な証明では、実際には「ライブラリ」、つまり文化や他人の知識を信頼しなければならない。公理まで実際に煮詰めていく実用的な方法がないからだ。
ZFC は死に、NF 万歳なのか？
集合を主に他のものを説明する共通言語として使うアマチュア数学者としては、これがより広い数学分野にどんな含意を持つのかよく分からない。特に、NF の有用性が既存の ZFC とその変種と同程度ならなおさらだ。
機械証明において NF が ZFC と同じくらい人気を得ると予想されているのだろうか。普遍集合の存在はより直感的に感じられるので、少なくともこの証明のおかげで形式化への個人的な関心は再び湧いてきた。
素朴なアマチュアの視点では、すべての ZFC モデルを NF モデルに拡張できるので、相対的一貫性の結果は NF を少なくとも ZFC と同じくらい有用にしてくれるように思える。
しかし、次のいずれかでない限り、NF が大きく有用になることはなさそうだ。
NF が矛盾していることを証明する。すると ZFC も矛盾している。夜空の星々が一つずつ消え始める ;)
ZFC が矛盾していることを証明する。すると NF が無矛盾である可能性はまだ残る。幸運を祈るしかない。
もちろん、真のクラスについて語れるとか、階層化された式でラッセルのパラドックスを回避できるといった、NF のより実用的な「生活の質」上の利点を見落としている可能性は大いにある。
NF を独立した基礎体系として推そうという意図はまったくない。NF はかなり特異な体系だ。
それでも誰かがそれを推したいなら、この一貫性の結果は、少なくとも ZFC で矛盾に到達する危険より大きくはない、という意味では使えると言ってくれる。
これは本当に気に入った。
最終的には協調的な証明と「バグ修正」につながり、数学が GitHub 上のコードに近いプロセスになるのではないかと気になる。
mathlib プロジェクトを追いかける自由時間があればいいのに。本当にすごい。
ものすごく緩い形でも参加する方法はある？
Natural numbers game から始められる。
https://adam.math.hhu.de/#/g/leanprover-community/NNG4
この分野の人間ではないけれど、十分に強いすべての体系は自分自身の無矛盾性を示せないという Gödel の定理があったのでは？
ただし、体系 X は自分自身の無矛盾性を証明できないが、より強い体系 Y は X の無矛盾性を証明できる。そして、さらに強い別の体系が Y の無矛盾性を証明することもできる。こうして、各体系がより弱い体系の無矛盾性を証明する連鎖ができる
これはその体系が絶対的に無矛盾であることを証明するものではない。Y が矛盾していれば、X が無矛盾であることも、X が矛盾していることも証明できてしまうからだ。それでも価値はある。いずれにせよ、私たちが Y を使う理由の一つは、その中で矛盾を知らないという点にあるからだ。形式体系はしばしば微妙な形で矛盾していることがあるので、「別の体系が無矛盾であるという仮定の下で無矛盾」は「無矛盾性の証明がまったくない」よりはずっと良い
矛盾した体系でも自分自身の無矛盾性を証明できる。したがって、ある体系が自ら無矛盾であるという証明を持っていても、実際に無矛盾かどうかは依然として分からない
作成者の一人が参加している Reddit の議論も見る価値がある 0
https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...