Mathematics in type thoery 日本語訳
数学とは何でしょうか？数学は基本的に４つのタイプに分類できると思います．定義，命題，証明，そしてアイデアです．
定義 (たとえば実数や
証明はある意味で数学の通貨だといえます：証明は賞で報いられます．証明の構築は芸術であり，証明の検証は科学です．このことは，Lean, Coq, Isabelle/HOL, Agda などのコンピュータ証明検証システムが，証明を構築するよりもチェックすることをはるかに得意とする理由を，とても簡単に説明しています．
そしてアイデアは，数学の純粋に芸術的な部分です．「閃き」の瞬間，問題解決を可能にする洞察力，これこそが数学のとらえどころのないアイデアなのです．
アイデアは，形式的な意味で私が最も理解していない数学の一部です．ここに２つの疑問があります：
- 群とは何ですか？
- 群をどう考えていますか？
最初のものは正確な「科学的な」質問です．群とは，ある特別な構造を持ち，ある公理を満たす集合のことです．正式な答えは Wikipediaの群についてのページにあります．群とは定義です．しかし，２つめの質問は種類の異なる質問です．群について考える方法は人によって異なります．
定義，命題，証明
アイデアとは対照的に，数学の他の部分（定義，定理/予想, 証明）は基礎的なシステムで形式化することができ，したがって精確な方法でコンピュータ上に作成・保存することができます．これは pdf ファイルのことではありません！pdf ファイルこそ，私が脱却したいものなのです！つまり，様々ある数学の基礎付け（集合論，型理論，圏論）のうち1つを理解するコンピュータプログラミング言語が設計されており，その言語で数学者が問題の定義，命題，証明を書くことができるということです．
私には，圏論でどのように数学の基礎付けを行うのかを説明する資格はありません．集合論について，ひとつだけ観察してみましょう．集合論における定義，たとえば実数や
しかし，型理論では驚くほど違います．今挙げた３つのもの ―― 定義，命題，証明 ―― はすべて同じ種類のものです！これらはすべて項です．群，証明，実数 ―― これらもすべて項です．定義と証明の統一，つまり集合と論理の統一が，型理論を実用的な基礎システムたらしめ，コンピュータに学部レベルのすべての数学を教えることを可能にしています．
宇宙，型，項
型理論では，すべてが項です．そしていくつかの項は型でもあります．すべての項が型であるわけではありませんが，すべての項は型を持っています．Lean では，コロンを使って項の型を表します．―― x : T という表記で，x が T という型の項であることを表します．たとえば，実数 π : ℝ が成り立ちます．つまり，π : ℝ と書きます．どちらも同じ数学的概念，つまり「
いま x : π は意味を持ちません．集合論では，
先ほど，すべての項は型を持つと書きました．では ℝ の型はなんでしょうか？ℝ : Type が答えです．実数全体は，Type と呼ばれる「宇宙」型の項です ―― これは「すべての集合がなすクラス」の型理論における類似物です．
数学者が定義する数学的対象の多くは，型 Type を持つか，あるいは T : Type であるような型 T を持ちます．漠然とした経験則ですが，要素を持つもの（群，環，体など）は Type 型を持ち，要素を持たないもの（T 型を持ちます．もう一つのあいまいな経験則として，大文字で書くもの（群や環など）や fancy letter（実数 ℝ や有理数 ℚ ）で書くものは Type 型を持ち，小文字で書くもの（群の要素 T 型を持つ傾向にあります．たとえば 2 : ℕ と ℕ : Type が成り立ちます．また g : G と G : Type が成り立ちます．ここには３層の階層があります ―― 一番下に項があり，その上に型があり，最上部に宇宙があります．
- 宇宙 :
Type
- 具体的な型 :
ℝ,ℕ,G(群),R(環),X(集合論者が集合と呼ぶなにか), バナッハ空間など. 形式的にはℝ : Typeなどと書きます.
- 具体的な項 :
π(型ℝの項),g(群Gの要素, つまり型Gの項),x(Xの要素, つまり型Xの項). 形式的にはg : Gなどと書きます.
この階層は，クラス（たとえばすべての集合のクラス）と集合の２つのレベルしかない集合論の階層よりも，表現力が高いです．
数学におけるコロンの標準的な使い方があります．―― 関数を書くための記法です．X と Y が集合（集合論を使っている場合）または型（型理論を使っている場合）であるとき，X から Y への関数を f : X → Y と書きます．これは実は Lean におけるコロンの使い方と一致しています．X から Y への関数の集まり X → Y であり，これは型です．（つまり X → Y : Type です．これは集合論で f : X → Y は f が X → Y 型の項であることを意味し．集合論でいう f が X から Y への関数であることを書き表すやり方です．
（これは試験に出ません）厳密に言えば，宇宙は型であり，型は項ですが，これは用語の問題です．多くの場合，ひとが型について語るとき，それは宇宙ではない型を意味し，ひとが項について語るとき，それは型ではない項を意味します．しかし常にそうとは限りません．私が初心者の頃は，これで混乱しました．
定理と証明
ここからが楽しいところです．ここまで，型とは型理論における集合の呼び名であり，項とは型理論における要素の呼び名でした．しかし，ここで Lean の型理論におけるもう一つの宇宙，命題の宇宙 Prop を見てみましょう．そこで起こることは，私たちの伝統的なメンタルモデルとは全く異なります．ここでは，定理のステートメントと証明が，型や項と同じようにどのようにモデル化できるかを見ていきます．
定理のステートメントと証明はどのようにモデル化されるのでしょうか？Lean の型理論には Type という宇宙だけでなく，Prop という第二の宇宙があります．Prop 型の項は命題です．ここで残念な表記の衝突があります．数学では，proposition (命題)という言葉はしばしば定理のこどもという意味で使われますが，定理は真です．（そうでなければ予想や反例と呼ばれます）したがって，数学において命題という言葉は真である文を指しますが，ここでは，論理学者と同じように命題という言葉を使います．つまり，命題とは一般的な真か偽かどちらかになる文のことであり，それが正しいか誤りかは関係ありません．
例を見るとわかりやすいでしょう．2 + 2 = 4 : Prop と書くことができます．しかし，2 + 2 = 5 : Prop と書くこともできます．何度も言いますが，命題が真である必要はありません！命題は真か偽かどちらかになる文のことです．もう少し複雑な例を見てみましょう．
「すべての自然数 (∀ x : ℕ, x + 0 = x) : Prop と表せます．命題は Prop 型を持つ項です．（先ほど見てきた項が型 Type を持っていたのと同様です）RH をリーマン仮説のステートメントとします．すると RH : Prop となります．それが真か偽か，特定の数学の公理と独立であるか，決定不能であるか，等は問いません．命題とは真か偽かどちらかになる文のことです．Lean の型理論の階層のうち，Prop 宇宙に住む部分を見てみましょう．
- 宇宙 :
Prop
- 具体的な型 :
2 + 2 = 4,2 + 2 = 5, フェルマーの最終定理のステートメント，リーマン仮説のステートメント
- 具体的な項 : ??
この３層構造の Prop 階層において，項にあたるものは何でしょうか？それは証明です！
命題は型，証明は項
これは，型理論の世界と集合論の世界との，そして３年前までの私の脳内世界との大きく異なる点です．何が起こっているのか理解しようとして，私は数学者が用語の濫用を行っていることに気づきました．まずそれについて考えてみましょう．ボルツァーノ＝ワイエルシュトラスの定理とは, 解析学における, 収束する部分列を持つ有界数列についてのステートメントです．数学者が「ボルツァーノ＝ワイエルシュトラスの定理」という言葉を実際にどのように使うかについて，少しお話ししましょう．数学者は，「ボルツァーノ＝ワイエルシュトラスの定理とは，収束する部分列を持つ数列に関するこのステートメントのことだ」と言うでしょう．しかし証明の途中で，証明を続けるためにこの定理を適用する必要がある場合は，「ボルツァーノ＝ワイエルシュトラスの定理によって，収束する部分列があることが推論される」と言います．何もおかしなことはないように思えます．しかし，私が指摘したいのは，「ボルツァーノ＝ワイエルシュトラスの定理」という言葉が２つの異なる意味で使われている，ということです．「ボルツァーノ＝ワイエルシュトラスの定理とは何か」という場合，かれらは定理のステートメントに言及しています．しかし，「ボルツァーノ＝ワイエルシュトラスの定理を使って」という場合，実際に使っているのはその証明です．バーチ・スウィンナートン＝ダイアー予想は，完全に整った命題であり，それが何であるかを正確に言うことができます．しかし，ある証明を完全なものにしたいのであれば，バーチ・スウィンナートン＝ダイアー予想をその証明の途中で使うことはできません．なぜなら現時点でこの予想は未解決問題だからです．ここで重要なのは，定理のステートメントと定理の証明とを明確に区別することです．数学者は「ボルツァーノ＝ワイエルシュトラスの定理」という言葉を，どちらの意味でも使うことがあります．このような非形式的な表記の濫用は初学者の混乱を招きます．なぜなら，以下では定理のステートメントと定理の証明を区別することが本当に重要だからです．この２つは全く異なるものです．
natural number game (自然数ゲーム) [1] の中で，私は数学者を相手にしていたのでこのような表記の濫用を行っていました．∀ x : ℕ, x + 0 = x という文は真であり，「これは Lean では add_zero と呼ばれる」と私は言っていました．natural number game において，私は add_zero : ∀ x : ℕ, x + 0 = x と書いていました．しかし，これが何を意味するかといえば，Lean で add_zero と呼ばれる項が ∀ x : ℕ, x + 0 = x の証明である，ということなのです！コロンは型理論的に使われています．私は natural number game では意図的にこの概念を曖昧にしました．add_zero はすべての ∀ x : ℕ, x + 0 = x は命題であり，型でもあり，add_zero はその証明であり，項でもあります．ここで重要なのは，定理のステートメントとその証明を区別することです．ステートメントは型であり，証明は項です．
- 宇宙 :
Prop
- 具体的な型 :
2 + 2 = 4,2 + 2 = 37, フェルマーの最終定理∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0
- 具体的な項 :
2 + 2 = 4の証明（2 + 2 = 4型を持つ項），フェルマーの最終定理の証明（∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0という型を持つ項）
定理の要素
つまり π : ℝ というステートメントに対する私たちのメンタルモデルは，型である ℝ は「ものの集まり」であり，項である π はその集まりのメンバーである，ということです．このアナロジーを続けるなら，2 + 2 = 4 というステートメントはある種の集まりであり，2 + 2 = 4 の証明はそのメンバーです．言い換えれば，Lean は 2 + 2 = 4 をある種の集合であるとし，2 + 2 = 4 の証明はその集合の要素であるとするようなモデルを提案しているのです．Lean では，ある命題の証明はすべて等しいという公理が組み込まれています．つまり a : 2 + 2 = 4 かつ b : 2 + 2 = 4 ならば a = b となります．これは Prop 宇宙の中だから起こることです ―― これが Lean における命題の振る舞いです．Type 宇宙の中ではこのようなことはありえません．―― π : ℝ かつ 37 : ℝ ですが，Prop 宇宙の特別な癖は「proof irrelevance (証明無関係)」と呼ばれます．形式的には，P : Prop に対して a : P かつ b : P ならば a = b である，と言い表せます．もちろん，ある命題が偽ならば，その命題には証明は全くありません！偽の命題は空集合のようなものです．つまり，Lean の命題のモデルは，真の命題は１つの要素を持つ集合のようなもので，偽の命題は
f : X → Y であるとき，f は X から Y への関数であるということを思い出しましょう．ここで，P → Q 型を持つ項です．繰り返しますが，h : P → Q という項 h です．natural number game で，私が → 記号を含意を表すのに使ったのは，このためです．
false を一般的な偽の文（true を一般的な真の文（false → false 型の項，または true → true 型の項を作ることはできるでしょうか？もちろんです．―― 恒等関数を使えばよいだけです．実際，どちらの場合も関数は一意に定まります．―― hom 集合のサイズは false → true 型の項を作ることはできるでしょうか？もちろん，true → false 型の項を作ることはできますか？これはできません．true の証明をどこに送ればいいのでしょうか？false の証明は存在しないので，送る先がありません．したがって true → false はサイズ → の標準的な真理値表に相当し，最初に分析した３つの文は真で，最後の文は偽です．
フェルマーの最終定理の証明は関数
では ∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0 の証明とはどのようなものでしょうか？この命題には矢印が含まれているので，フェルマーの最終定理のステートメントは x, y, z です．４番目の入力は証明で，命題 n > 2 ∧ x^n + y^n = z^n の証明です．そして出力は命題 x*y=0 の証明です．これは「フェルマーの最終定理の証明とは何か」という問いについてのきわめて型破りな考え方であり，証明を実際に理解しようとする際には全く役に立たないことを強調しておきましょう． ―― しかし，これは数学がどのように機能するかについての完全に一貫したメンタルモデルです．数と証明の概念を統一することで，―― つまり両方を項として考えることで，―― 証明を関数として考えることができます．Lean は関数型プログラミング言語であり，特に関数を中心に設計されています．現在 Lean や Coq や Isabelle/HOL といった型理論を使用する証明支援系が，Metamath や Mizar のような集合論を使用する証明支援系より進んでいるのは，このためだと私は確信しています．
定理を証明しましょう！関数を書きましょう！
| 宇宙 | Type |
Prop |
| 型の例 | ℝ | 2 + 2 = 5, (∀ a : ℕ, a + 0 = a) |
| 項の例 | 37, π |
add_zero, rfl
|
訳者: @aconite-ac, @Seasawher
Discussion