証明難しい
数学書(初心者向け)を読んでいると度々証明に出くわす。
ごく基本的で直感的には「いやいやそりゃそうでしょ」っていう規則も証明して、 それを積み上げながら「え、そうなるの」っていう不思議な規則が証明されたりする。 このプロセスは精緻で地道で、けれど発見があった時の興奮が刺激的だ。
でも難しい。
自分でやるのはなかなか骨の折れる作業だ。
小さな証明ですらトライしては打ち負かされて悲嘆にくれている。 群という代数的構造に近づきたいのに、その群論が前提とするごくごく初歩的な定理の証明で躓いている。
これではいけない。このままでは群論はあまりに遠い。ましてや圏論なんてずっと先のことだ。
何が問題か
まずは躓くパターンを自覚しなければならない。
途方に暮れるという感覚
証明するべき命題が与えられる。
詰まる時は決まって「証明の道筋が見えない」ということだ。 何を示せばこの定理が真であると言えるのか、それに気づかない。
だから手持ちの等式を変形して、なんの収穫も得られず途方に暮れる。 これが問題なわけだ。
問題の解決に向けて
命題を整理する
難しくて大きな仕事の依頼が来た時は、それを分解する。WBSを作ったりするのはそのアプローチの一つだ。 この考え方を応用できないだろうか。
例題を解きながら思考の過程を整理しようと思う。
集合
\( A \subseteq B \land B \subseteq C \Rightarrow A \subseteq C \)
を証明してみる。集合の包含関係についての三段論法だ。
問題の分解
結論である
\( A \subseteq C \)
を分解できるか？
まずここが最初の壁。 ポイントとなるのは言い換えだ。ある性質が「つまりどういうことか?」を書き下すことで問題を捉える。 ここでは集合の元と集合の関係で記述してみる。
Aに含まれる要素xがすべてCに含まれている。
\( \forall x (x \in A \rightarrow x \in C) \)
こんな風に含意で書き換えることができる。
はて、これを証明するプロセスはどんな感じになるか。整理してみよう。
プログラムのように考えると、\( P \rightarrow Q \) はあたかも関数のように考えることができる。 Haskellならこういう型を持つだろう。
proof :: P -> Q
証明はこの関数の実装を与えるような作業だ。
つまり与えられたPという仮定に他の関数(定理・公理)を適用してQという結論を生じることを示す。
そう考えてみる。
これを証明の手続きで表現するのであれば、仮定を変形しながら結論を導く作業が証明の道筋となる。
証明
仮定を要素との関係で表してみる。それを変形しながら結論へと辿り着けるか確認してみよう。
\( \forall x (x \in A \rightarrow x \in B) \land (x \in B \rightarrow x \in C) \)
この仮定の式と結論の式を見比べてみる。
\( \forall x (x \in A \rightarrow x \in C) \)
Bについての命題と論理積\(\land\)が消去できれば結論に辿り着けそうだ。
含意の関係を消去する方法は解らないが、論理積と論理和なら消去の規則が使えるかもしれない。
含意を論理和に変形してみる。 まずは仮定の論理積の左側。
\( \forall x (x \in A \rightarrow x \in B) \)
これを論理和に変形する。
\( \forall x (\lnot (x \in A) \lor x \in B) \)
この時点で
\( \forall x (\lnot (x \in A) \lor x \in B) \land (x \in B \rightarrow x \in C)\)
そしてこのあと式を変形し続けて泥沼にはまっていく……。
けっきょく仮定から結論は導けなかった。悔しいながらも解答を見てみる。
解答
\( A \subseteq B \land B \subseteq C \)
= 部分集合の定義(ここは気づけた)
\( \forall x ((x \in A \rightarrow x \in B) \land (x \in B \rightarrow x \in C)) \)
= 仮言三段論法 ★
\( \forall x (x \in A \rightarrow x \in C) \)
= 部分集合の定義(これを使って論理含意から関係へと戻すべきなのも気づいていた)
\( A \subseteq C \)
★のところがブレイクスルーだった。直感的には分かることだが自分はそれを正しい定理として導入できなかった。 何故なら仮言三段論法という定理を知らなかったからだ。 それが直感的に正しいからといって自分で定理として導入することはできない。 だから使えなかった。
本当はこの三段論法（論理含意の推移律）を補題として証明すべきだったのかもしれない。
まとめ
解ったのは証明の作り方。
- 仮定から出発する
- 既知の定理を使って仮定を変形する
- 結論の式を導く
またこれを達成するためにいくらか結論の式をあれこれ変えてみて、 自分が解きやすい形にするのも、最初の段階で試してみる価値があると解った。