## 定義 証明(proof)とは、公理(axiom)と既に証明された命題から、論理的な演繹(deduction)を積み重ねて対象の命題を導く手続きである。証明済みの命題は文脈での役割に応じて定理(theorem, 重要な真な命題)・補題(lemma, 後の証明のための準備的命題)・系(corollary, 定理からわずかな論理的段階で導かれる命題)と呼び分けられるが、この呼び分けは厳密な定義ではない。命題(proposition, 真か偽かのいずれかであるコミュニケーション)や述語(predicate, 変数の値に依存して真偽が定まる命題)は証明の対象となる文の基本単位であり、無限集合に関する主張は有限個の要素の確認だけでは証明できない(Euler予想が218年間反例なしに信じられ、n=61^7年後に反例が見つかった例が典型)。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 1 What is a Proof?]] §1.1, §1.3) ## 中核概念 - **証明の4つの定型パターン**: 含意「PならばQ」の証明(直接法: Pを仮定してQを導く/対偶法: `NOT(Q)⟹NOT(P)` を示す)、「P iff Q」の証明(両側含意を示す/同値変形の連鎖を構成する)、場合分けによる証明(考えうる全ケースを尽くしたことを示す必要がある)、背理法(Pの否定を仮定し矛盾を導く)の4種が基本パターンとして提示される。(Source: ch.1 §1.5–§1.8) - **良い証明の実践的基準**: 論理的な正しさに加えて明確さ(clarity)が要求される。方針の明示・線形な流れ・記号だけでなく完全な文で書く「エッセイとしての証明」・過度な記号使用の回避・推敲・長い証明を補題に分割する構造化・「明らか」の濫用への警戒・証明を最後まで書き切ることが実践的な指針として挙げられる。(Source: ch.1 §1.9) - **偽の証明(bogus proof)への警戒**: 誤った結論に至る証明だけでなく、正しい結論に循環論法や未正当化な飛躍で到達する証明も「偽の証明」であり、これを見抜く訓練が証明を書く力を養う。(Source: ch.1 §1.9) - **工学的動機**: 証明の厳密さはプログラム・システムの正当性(correctness)を保証する実務(CPUチップの正当性証明など)に直結し、厳密さの欠如は Therac-25 や航空会社システム障害のような致命的な結果を招きうる。(Source: ch.1 §1.1, §1.9) ## 横断的知見 - 第2章が導入する [[整列原理]] は、本ページの4パターン(直接法・対偶法・場合分け・背理法)のどれか一つに単純には収まらない証明技法である。形式としては背理法(反例の集合が空でないと仮定して矛盾を導く)だが、そこに「反例集合の最小元を取る」という整列原理固有の一手が加わっている。第1章時点の4分類は「対偶・背理法は直接法が難しいときの代替」という緩い指針にとどまっており、整列原理の最小反例法はその枠組みを具体化・拡張する特殊形として位置づけられる。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 1 What is a Proof?]], [[@2015__MIT__Mathematics for Computer Science - Chapter 2 The Well Ordering Principle]]) ## 未解決の問い - 直接法・対偶法・背理法・場合分けという4パターンの使い分けは、どのような判断基準で選ばれるべきか(本章は「対偶・背理法は直接法が難しいときの代替」という緩い指針しか与えていない)。第5章(帰納法)で整列原理・通常の帰納法・強帰納法が相互翻訳可能とされる予定だが、証明パターンの分類にどう影響するかは ingest 後に検討する。 - 「良い証明」の基準(§1.9)は数学以外の分野(計算機科学の形式手法・査読プロセス)にどこまで一般化できるか。 - Therac-25 や航空会社システム障害の事例は、厳密な証明の欠如が直接の原因なのか、それとも検証プロセス全体の欠如を象徴する逸話なのか。一次資料での裏付けは未確認。 ## 関連 - source: [[@2015__MIT__Mathematics for Computer Science - Chapter 1 What is a Proof?]] - 概念: [[公理的方法]] —— 証明が依拠する公理と推論規則の枠組みを扱う姉妹concept。本conceptは証明の「組み立て方」、あちらは証明の「土台」を扱う。 - 実体: [[Euclid]] ## 出典 - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 1.