定理と証明

ここからが楽しいところです．ここまで，型とは型理論における集合の呼び名であり，項とは型理論における要素の呼び名でした．しかし，ここで Lean の型理論におけるもう一つの宇宙，命題の宇宙 Prop を見てみましょう．そこで起こることは，私たちの伝統的なメンタルモデルとは全く異なります．ここでは，定理のステートメントと証明が，型や項と同じようにどのようにモデル化できるかを見ていきます．

定理のステートメントと証明はどのようにモデル化されるのでしょうか？Lean の型理論には Type という宇宙だけでなく，Prop という第二の宇宙があります．Prop 型の項は命題です．ここで残念な表記の衝突があります．数学では，proposition (命題)という言葉はしばしば定理のこどもという意味で使われますが，定理は真です．（そうでなければ予想や反例と呼ばれます）したがって，数学において命題という言葉は真である文を指しますが，ここでは，論理学者と同じように命題という言葉を使います．つまり，命題とは一般的な真か偽かどちらかになる文のことであり，それが正しいか誤りかは関係ありません．

例を見るとわかりやすいでしょう．$2 + 2 = 4$ は命題なので 2 + 2 = 4 : Prop と書くことができます．しかし，$2 + 2 = 5$ も命題なので，2 + 2 = 5 : Prop と書くこともできます．何度も言いますが，命題が真である必要はありません！命題は真か偽かどちらかになる文のことです．もう少し複雑な例を見てみましょう．

「すべての自然数 $x$ について $x + 0 = x$ である」という文は命題です．Lean では，これは (∀ x : ℕ, x + 0 = x) : Prop と表せます．命題は Prop 型を持つ項です．（先ほど見てきた項が型 Type を持っていたのと同様です）RH をリーマン仮説のステートメントとします．すると RH : Prop となります．それが真か偽か，特定の数学の公理と独立であるか，決定不能であるか，等は問いません．命題とは真か偽かどちらかになる文のことです．Lean の型理論の階層のうち，Prop 宇宙に住む部分を見てみましょう．

• 宇宙 : Prop

• 具体的な型 : 2 + 2 = 4, 2 + 2 = 5, フェルマーの最終定理のステートメント，リーマン仮説のステートメント

• 具体的な項 : ??

この３層構造の Prop 階層において，項にあたるものは何でしょうか？それは証明です！