命題は型，証明は項

これは，型理論の世界と集合論の世界との，そして３年前までの私の脳内世界との大きく異なる点です．何が起こっているのか理解しようとして，私は数学者が用語の濫用を行っていることに気づきました．まずそれについて考えてみましょう．ボルツァーノ＝ワイエルシュトラスの定理とは, 解析学における, 収束する部分列を持つ有界数列についてのステートメントです．数学者が「ボルツァーノ＝ワイエルシュトラスの定理」という言葉を実際にどのように使うかについて，少しお話ししましょう．数学者は，「ボルツァーノ＝ワイエルシュトラスの定理とは，収束する部分列を持つ数列に関するこのステートメントのことだ」と言うでしょう．しかし証明の途中で，証明を続けるためにこの定理を適用する必要がある場合は，「ボルツァーノ＝ワイエルシュトラスの定理によって，収束する部分列があることが推論される」と言います．何もおかしなことはないように思えます．しかし，私が指摘したいのは，「ボルツァーノ＝ワイエルシュトラスの定理」という言葉が２つの異なる意味で使われている，ということです．「ボルツァーノ＝ワイエルシュトラスの定理とは何か」という場合，かれらは定理のステートメントに言及しています．しかし，「ボルツァーノ＝ワイエルシュトラスの定理を使って」という場合，実際に使っているのはその証明です．バーチ・スウィンナートン＝ダイアー予想は，完全に整った命題であり，それが何であるかを正確に言うことができます．しかし，ある証明を完全なものにしたいのであれば，バーチ・スウィンナートン＝ダイアー予想をその証明の途中で使うことはできません．なぜなら現時点でこの予想は未解決問題だからです．ここで重要なのは，定理のステートメントと定理の証明とを明確に区別することです．数学者は「ボルツァーノ＝ワイエルシュトラスの定理」という言葉を，どちらの意味でも使うことがあります．このような非形式的な表記の濫用は初学者の混乱を招きます．なぜなら，以下では定理のステートメントと定理の証明を区別することが本当に重要だからです．この２つは全く異なるものです．

natural number game (自然数ゲーム) ¹の中で，私は数学者を相手にしていたのでこのような表記の濫用を行っていました．∀ 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$ であるという「アイデア」と何らかの形で等しいと，数学者に信じさせたわけです．しかし裏では ∀ 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 という型を持つ項）

¹ 訳注: natural number game は，ペアノの公理から始めて整数の基本的な性質を Lean で示すブラウザゲームです．ここで紹介されているのは Lean3 版ですが，Lean4 版がこちらにあります．ソースコードはこちらです．