定理の要素

つまり π : ℝ というステートメントに対する私たちのメンタルモデルは，型である ℝ は「ものの集まり」であり，項である π はその集まりのメンバーである，ということです．このアナロジーを続けるなら，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 : ℝ ですが，$\pi\not=37$ です．この Prop 宇宙の特別な癖は「proof irrelevance (証明無関係)」と呼ばれます．形式的には，P : Prop に対して a : P かつ b : P ならば a = b である，と言い表せます．もちろん，ある命題が偽ならば，その命題には証明は全くありません！偽の命題は空集合のようなものです．つまり，Lean の命題のモデルは，真の命題は１つの要素を持つ集合のようなもので，偽の命題は $0$ 個の要素を持つ集合のようなものだと言っています．

f : X → Y であるとき，f は X から Y への関数であるということを思い出しましょう．ここで，$P$ と $Q$ を命題とし，$P\implies Q$ がわかっているとします．これは何を意味するでしょうか？これは $P$ ならば $Q$ であるということを意味します．$P$ が真であるとき，$Q$ も真だということです．$P$ の証明があれば，$Q$ の証明も作れるということです．$P\implies Q$ は $P$ の証明から $Q$ の証明を得る関数です．$P$ の要素を $Q$ の要素に送る関数です．P → Q 型を持つ項です．繰り返しますが，$P\implies Q$ の証明は h : P → Q という項 h です．natural number game で，私が → 記号を含意を表すのに使ったのは，このためです．

false を一般的な偽の文（$0$ 個の要素を持つ集合と考えられる）とし，true を一般的な真の文（$1$ 個の要素を持つ集合と考えられる）とします．false → false 型の項，または true → true 型の項を作ることはできるでしょうか？もちろんです．―― 恒等関数を使えばよいだけです．実際，どちらの場合も関数は一意に定まります．―― hom 集合のサイズは $1$ です．false → true 型の項を作ることはできるでしょうか？もちろん，$0$ 個の要素を持つ集合から $1$ 個の要素を持つ集合への関数はあり，この関数も一意です．では true → false 型の項を作ることはできますか？これはできません．true の証明をどこに送ればいいのでしょうか？false の証明は存在しないので，送る先がありません．したがって true → false はサイズ $0$ の集合です．これは → の標準的な真理値表に相当し，最初に分析した３つの文は真で，最後の文は偽です．