「証明とは何か」を形式的に
納得の説明から、検査できる導出へ
入門（高校〜大学1年レベル）
このページの目標
日常語の「証明」を、公理と推論規則からなる導出として形式的に定義し直す。証明の正しさが式の意味を考えずに記号の形だけで機械的に検査できること、その意義を理解する。
1. 日常の証明と形式的な証明
数学の授業で書く証明は、「こうだから、こうなって、ゆえにこう」という文章である。これは読み手を納得させるための説明であり、どこまで細かく書くかは書き手の判断に委ねられている。便利だが、「本当に正しいか」を機械的に確かめる基準がない。
数理論理学では、この曖昧さを取り除くために証明を完全に形式化する。すべてのステップを、あらかじめ決めた公理と推論規則だけで埋め、省略を許さない。こうして得られるのが形式的証明である。
2. 導出としての証明
式 $A$ の形式的証明とは、式の有限列 $A_1, A_2, \dots, A_n$（$A_n = A$）であって、各 $A_i$ が次のいずれかであるものをいう。 (1) 公理である、 (2) すでに現れた式 $A_j, A_k\ (j,k < i)$ に推論規則を適用して得られる、 (3) 仮定として置かれた式である。
構文と意味で導入した $\Gamma \vdash A$ とは、まさに「仮定 $\Gamma$ のもとで $A$ の形式的証明が存在する」ことを指す。証明はもはや散文ではなく、規則どおりに並んだ記号列そのものになる。
同じことを、列ではなく木として書くと見通しがよい。各推論規則の適用を枝分かれで表したものが証明木である。葉に公理や仮定、根に結論が来る。
3. 証明検査という考え方
形式的証明の最大の利点は、正しさが機械的に確認できることである。証明列の各ステップについて「これは公理か」「これは前のどれかに規則を適用したものか」を順に照合するだけでよい。式が何を意味するかは一切問わない。
探すのは難しい、確かめるのは易しい
証明を見つけるのは一般に難しく、人間の創意や試行錯誤を要する。しかし与えられた証明が正しいかを確かめるのは、規則との照合だけで済む単純な作業である。この非対称性が、証明を計算機に検査させられる理由である。
この「検査は単純」という性質は、後の章の核心につながる。証明を生成する部分（人間や、賢いが信頼しないプログラム）と、証明を検査する小さなプログラムを分け、検査器だけを信頼するという設計である。これが LCF アーキテクチャ や de Bruijn 基準・TCB の考え方であり、証明アシスタントの信頼性の根拠になる。
4. どの規則を認めるかが体系を決める
形式的証明は「公理と推論規則」に相対的である。何を公理とし、どの規則を許すかで、導ける式の集合が変わる。たとえば排中律 $A \lor \neg A$ を公理として認めるかどうかで、古典論理と直観主義論理が分かれる（直観主義 vs 古典）。
「証明とは何か」という問いの答えは、結局「どの土台（公理と規則）の上で導出を組むか」に帰着する。次章では、論理と計算が同じ構造を持つという驚くべき対応（Curry–Howard）を一望し、証明の正体にもう一歩踏み込む。
まとめ
この章のポイント
- 形式的証明：公理から推論規則を有限回適用して結論に至る導出（列または証明木）
- $\Gamma \vdash A$ ＝「$\Gamma$ のもとで $A$ の形式的証明が存在する」
- 証明の正しさは式の意味を考えず、記号の形だけで機械的に検査できる
- 「探すのは難しいが確かめるのは易しい」非対称性が、計算機による検査の根拠
- どの公理・規則を認めるかが体系（古典 / 直観主義など）を決める
よくある質問
形式的な証明とは何か
公理から出発し、推論規則を有限回適用して目的の式に至る導出（規則の適用列、または証明木）である。各ステップは規則どおりに導かれていなければならず、正しさは式の意味を考えず記号の形だけで確認できる。日常の「納得させる説明」と違い、検査の手続きが完全に定まっている点が特徴である。
公理と推論規則はどう違うのか
公理は証明の出発点として無条件に認める式、推論規則は「すでに導けた式から新しい式を作ってよい」という書き換えの規則である。証明とは公理を起点に規則を適用して結論まで到達する道筋であり、どの公理とどの規則を認めるかが体系を決める。
なぜ証明を機械的に検査できることが重要なのか
記号の形だけで検査できれば、その検査を小さなプログラム（証明検査器）に任せられる。証明を見つけるのは難しくても、与えられた証明が正しいか確かめるのは単純な照合で済む。この「探すのは難しいが確かめるのは易しい」非対称性が、証明アシスタントや形式検証が信頼できる根拠になっている。