1.9 現実世界における優れた証明

証明を作成する目的の一つは主張の正しさを絶対的な正確性で立証することにある。途方もなく長く複雑な証明であっても、機械によって検証可能でありさえすればその目的は達成される。しかし、数学を学ぶ人の理解を助けられるのは人間に理解可能な証明だけである。数学者の多くは、数学における重要な結果はその証明が理解されるまでは本当に理解されないと考えている。このため、本講義のカリキュラムでは証明が非常に重要となる。

証明を理解可能で有用なものとするには、論理的正しさ以上のものが求められる: 優れた証明は明確でなければならない。通常、正しさと明確さは密接に関連する。よく書かれた証明は正しい証明である可能性が高い。間違いを隠すのが難しいからである。

現実世界において、証明という概念は状況によって変化する。専門的な研究ジャーナルで発表される証明は、証明に使われる用語と過去の結果を全て知っている少数の専門家だけが読めるように書かれる。逆に、6.042 (本講義) のような入門講義の最初の数週で示される証明は、職業数学者から見れば退屈で長たらしいものでしかないだろう。さらに、6.042 で「優れた証明」とみなされる証明は最初の数週とそれ以降で変化する。ただそうはいっても、優れた証明を書くための一般的なヒントを示すことはできる:

全体像を示す

優れた証明は「場合分けを用いる」「背理法で示す」といった証明全体の流れを説明する文章から始まる。

議論の流れを保つ

関係が薄い論証が散りばめられた、数学的モザイク画とでも言うべき証明を目にすることがある。これは優れた証明とは言えない。議論の各ステップは一つ前のステップを受けて議論を進めるべきであり、人間が理解しやすい順序で並んでいなければならない。

計算ではなく文章として証明を書く

積分を計算するように証明を書く学生が最初は多くいる。大量の数式が説明なしに並ぶので、読むのが非常に難しい。これは悪い証明である。優れた証明は少量の数式を含んだ文章のような見た目をしていることが多い。数式ではなく完全な文を書くべきである。

記号の濫用を避ける

証明の読者はおそらく自然言語を問題なく理解できるのに対して、奇妙な数学記号の読解にはそれほど慣れていない可能性が高い。自然言語で十分な場合は記号を避けるのが望ましい。

推敲し、単純化する

証明の読者はありがたく思うだろう。

新しい概念は注意深く導入する

新しい変数の導入、特別な記法の使用、新しい用語の定義によって議論が格段に単純化される場合がある。しかし、こうすると読者は新しい事項を覚えなければならないので、利用は必要最低限に留めるべきである。また、新しい変数・用語・記法を定義することを忘れてはいけない。いきなり使い始めないように！

長い証明では構造を意識する

長いプログラムは短い手続きからなる階層構造に分解されて書かれることが多い。長い証明でも同じことが言える。表明は簡単でも証明は複雑な事実が必要になったときは、その事実を補題として切り出すのが望ましい。また、本質的に同じ議論が何度も繰り返されているときは、それらの議論を一般化して補題にできないかどうかを考えてみるべきである。補題にできれば、以降の議論ではそれを参照するだけで済む。

「明らか」に注意する

よく知っている事実や明らかな事実が証明で必要になったときは、「証明はしないが、この事実を使う」と書けば使って構わない。しかし、あなたにとって明らかでも、読者にとっては明らかでない可能性が ── 大いに ── あることを忘れてはいけない。

特に避けてほしいのが、証明を思い付かなかった命題の正しさを読者に無理やり認めさせる目的で使う「明らかに」や「自明に」である。他人が書いた証明にそういったフレーズが含まれる場合も注意した方がいい。

証明を終える

証明を進めると、証明に必要な重要な事実が全て立証された状態になる。そこから「明らか」な結論を導くステップを読者に任せて証明をそこで終えたくなるかもしれないが、その誘惑に負けてはいけない。自分で全てのパーツをつなぎ合わせ、示したかった命題が従うことを説明するべきである。

優れた証明の作成は美しい芸術作品の作成に似ている。実際、数学者は非常に優れた証明を指して「優雅」や「美しい」といった言葉を使う。そういった賛辞を受ける証明を書くには訓練と経験が必要になるものの、正しい方向への最初の一歩として、本書では有用性の高い様々な証明技法のテンプレートを示していく。

本書には誤った証明 (bogus proof) の例も含まれる ── 証明のように見えて本当は証明でない議論である。誤った証明が論理的誤りや仮定の誤解を含んでいて、最終的な結論が偽の場合もある。一方で、真の結論を不適切な手法 (循環論法、仮定の確認忘れ、「読者への練習問題とする」など) で示している場合もある。正しくない証明の誤りを指摘する練習をすれば、証明の各ステップが以前のステップから従うことを確認するスキルが磨かれるだろう。自分の証明に含まれる誤りも見つけやすくなる。

優れた証明と優れたプログラムの類似点は構造だけではない。証明を書くために必要な厳密な思考法は、クリティカルな計算機システムを設計する上で不可欠である。アルゴリズムやプロトコルが何となくの設定で「だいたい正しく動く」とき、次に発生する問題が小さな障害か壊滅的な事故かは全く予想が付かない。誤ったプログラムが壊滅的な事故を起こした古い例として Theracセラック-25 がある。ガン患者に放射線治療を施すための装置であった Therac-25 は、ソフトウェアの競合状態が原因で膨大な量の放射線を照射し、患者を死亡させていたことが判明した。十数年前 (2004 年 8 月) にも、ユナイテッド航空とアメリカン航空が利用していた計算機システムに誤ったコマンドが一つ含まれていたことが原因で全ての飛行機 (そして全ての乗客) が飛び立てなくなる事態が発生した。

将来、あなたもしくはあなたのクラスメイトによって設計されたクリティカルな計算機システムが何らかの意味で私たち全員の首根っこを押さえることは間違いない。システムが設計者の意図通りに振る舞う事実を確実に信頼できる論理的な議論で形式的に示すスキルを、あなたが本講義で習得することを心の底から願っている！

参考文献

[14], [1], [49], [18], [22]