## 定義 公理的方法(axiomatic method)とは、直観的に疑いのない少数の仮定(公理, axiom)から出発し、論理的演繹の連鎖(証明)によって新たな真な命題を導く数学的真理の確立手続きである。紀元前300年ごろアレクサンドリアの数学者 Euclid が幾何学のために考案し、現代数学の基礎となっている。20世紀には Zermelo-Fraenkel with Choice(ZFC)という少数の公理と論理的推論規則だけで数学のほぼ全てを導出できることが示された。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 1 What is a Proof?]] §1.3) ## 中核概念 - **ZFCと実用上の代替**: ZFCは数学の基礎付けとしては重要だが、実用には原始的すぎる(ZFCで `2+2=4` を形式的に証明するには20000ステップ超を要する)。*Mathematics for Computer Science* はZFCの代わりに「高校数学で親しんだ既知の事実全て」を公理として採用する方針を取り、公理の精密な特定よりも「何を仮定しているか読み手に明示すること」を実務的な指針とする。(Source: ch.1 §1.4) - **推論規則(inference rule)と健全性(soundness)**: 推論規則は、証明済みの命題(前提, antecedent)から新たな命題(結論, consequent)を導く規則であり、モーダスポネンス(P と `P⟹Q` から Q を導く)が代表例。健全な推論規則とは、前提をすべて真にする真理値の割り当てが結論も必ず真にする規則をいう。健全な公理と健全な推論規則を組み合わせれば、証明された命題は必ず真になる。(Source: ch.1 §1.4.1) - **健全性の反例**: `NOT(P)⟹NOT(Q) ⊢ P⟹Q` という規則は健全ではない。P=真・Q=偽という真理値の割り当てで前提は真になるが結論は偽になるため、この規則を用いた「証明」は妥当ではない。健全性は推論規則が満たすべき最低要件として明示的に検証可能である。(Source: ch.1 §1.4.1) - **定理・補題・系の階層**: 重要な真な命題を定理(theorem)、後の証明のための準備的命題を補題(lemma)、定理からわずかな論理的段階で導かれる命題を系(corollary)と呼ぶ。この分類は理論内での役割を表す慣習的な呼称であり、厳密な定義ではない(良い補題が元の定理より重要になることもある)。(Source: ch.1 §1.3) - **Russellのパラドックスと素朴な内包の破綻**: 「自分自身を要素に含まない集合すべての集まり」W := {S | S ∉ S} を考えると、W ∈ W iff W ∉ W という矛盾が生じる(Russellのパラドックス)。これは、任意のwell-definedな性質から集合を構成できるという素朴な内包公理(Fregeが最初の集合論の公理系として採用していた)が矛盾することを示し、公理的方法そのものの脆さ——ある時代に「自明」だと思われていた公理が後に矛盾を生むことがある——を露呈させた事例である。(Source: ch.7 §7.3.1) - **ZFC公理系**: 現代数学の標準的な公理的基礎で、Extensionality(外延性)・Pairing(対)・Union(和集合)・Infinity(無限公理)・Subset(内包を既存集合の部分集合に制限する)・Power Set(冪集合)・Replacement(置換)・Foundation(基礎、∈の無限降下列の禁止)・Choice(選択公理)の9公理からなる。Russellのパラドックスは、内包の対象を「すべての集合」ではなくSubset公理により「既存の集合xの部分集合」に制限し、さらにFoundation公理によりいかなる集合も自分自身の要素になれないことを保証することで回避される(Wは「すべての集合を含む」ため集合になり得ないという形で矛盾が解消される)。(Source: ch.7 §7.3.2〜§7.3.3) - **公理系自体の限界**: ZFC公理系のもとでも、Cantorの連続体仮説(NとpowNの間の濃度を持つ集合は存在しないという予想)はZFCから独立であり、GödelとPaul Cohenにより証明も反証もできないことが示されている。さらにGödelの不完全性定理により、ZFCのような無矛盾な公理系は、その公理系自身の無矛盾性を自身の内部では証明できない。公理的方法は数学の基礎として機能するが、「正しい公理を選び切った」という保証をそれ自身の中には持てない。(Source: ch.7 §7.4) ## 横断的知見 - 第1章と第7章を突き合わせると、公理的方法という同じ枠組みが2つの異なる緊張関係の中で提示されていることが見える。第1章はZFCを「数学の基礎として重要だが実務には原始的すぎる」ものとして退け、代わりに「高校数学で親しんだ既知の事実」という非形式的な公理群を実務的な選択として採用する。一方第7章は、まさにその退けられたZFCに立ち返り、なぜ集合論という基礎だけは非形式的な扱いで済ませられないか(素朴な集合の直観がRussellのパラドックスで破綻するから)を示す。つまり本書の公理的方法へのスタンスは「実務上は非形式的な公理で十分だが、集合そのものの基礎だけは形式化されたZFCが必要」という役割分担になっている。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 1 What is a Proof?]], [[@2015__MIT__Mathematics for Computer Science - Chapter 7 Infinite Sets]]) - 第1章は「健全な公理と健全な推論規則を組み合わせれば証明された命題は必ず真になる」と述べ、公理的方法の信頼性を強調する。第7章はこれに対する重要な限定を加える: 公理の集まりが無矛盾かどうかは、その公理系の外部からしか(あるいは全く)確認できない(Gödelの不完全性定理)。第1章で暗黙に前提されている「公理さえ正しく選べば安全」という立場は、第7章によって「そもそも正しく選べたかどうかを体系内部では確認できない」という限界を明示的に付与される。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 1 What is a Proof?]] §1.3〜§1.4, [[@2015__MIT__Mathematics for Computer Science - Chapter 7 Infinite Sets]] §7.4) ## 未解決の問い - 「高校数学で親しんだ既知の事実」を公理とする非形式的な方針は、どこまで数学的な厳密性を犠牲にしているか。この非形式的な方針とZFCとの間には、本書の中で明示的な橋渡し(高校数学の各事実がZFCから実際にどう導かれるか)は示されない。 - モーダスポネンス以外に本書が明示的に採用する推論規則には何があるか(第1章では代表例が数点挙げられるにとどまる)。 - Euclidの5公理(幾何学の公理)とZFC(集合論の公理)は、歴史的・数学的にどのような関係にあるか。本書は両者を並置するが、その間の理論的な移行過程には触れていない。 - 連続体仮説がZFCから独立であるという事実(Gödel・Paul Cohen)は、公理的方法にとって何を意味するか。ZFCに新しい公理を追加して連続体仮説を決定するという立場は、Euclidの第5公準(平行線公準)を巡る非Euclid幾何学の歴史と類比的か。本書はこの問いを提起するのみで(§7.4)、答えを示さない。 ## 関連 - source: [[@2015__MIT__Mathematics for Computer Science - Chapter 1 What is a Proof?]] / [[@2015__MIT__Mathematics for Computer Science - Chapter 7 Infinite Sets]] - 概念: [[証明]] —— 公理的方法が支える証明の組み立て方(直接法・対偶法・場合分け・背理法)を扱う姉妹concept。 / [[対角線論法]](Russellのパラドックスと同型の議論構造) / [[濃度]] - 実体: [[Euclid]] / [[Georg Cantor]] / [[Bertrand Russell]] ## 出典 - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 1, Chapter 7.