1.4 本書で利用する公理

ZFC は数学の基礎を解析・正当化する上で重要な公理であるものの、あまりにも原始的で実用するのは難しい。ZFC で定理を証明するのは高機能なプログラミング言語を使わずに機械語を直接打ち込んでプログラムを書くようなものと言える ── ある推定によると、ZFC を使った \(2 + 2 = 4\) の厳密な証明には \(20{,}000\) ものステップが必要になる！そこで本講義では ZFC から議論を始めることはせず、大量の命題を公理として受け入れる: 高校の数学で習う様々な命題を公理として使用する。

こう定めれば証明を書くのが楽になるものの、ときには公理の曖昧な定義が問題になる場合もある。例えば、証明の途中で「この事実を証明するべきか？それとも公理として使っていいのか？」と悩むことがあるかもしれない。仮定しても構わない命題と証明が求められる命題は状況や読み手ごとに異なるので、絶対的な回答は存在しない。ただ一般的なガイドラインとして、証明されない命題を使うときは正直に「証明せずに使う」と書いた方がいいだろう。

1.4.1 論理的演繹

論理的演繹 (logical deduction) を使うと、証明済みの命題を利用して新しい命題を証明できる。論理的演繹のルールを定める規則を推論規則 (inference rule) と呼ぶ。

最も基礎的な推論規則は modusモーダス ponensポネンスである。この規則は「命題 \(P\) の証明と命題 \(P \ \operatorname{\text{\footnotesize IMPLIES}}\ Q\) の証明を合わせると命題 \(Q\) の証明になる」と定める。

数学者は推論規則を奇妙な記法で書くことがある。例えば modus ponens は次のように書かれる:

推論規則

\[ \frac{P,\quad P \ \operatorname{\text{\footnotesize IMPLIES}}\ Q}{Q} \]

横線の上にある命題を前件 (antecedent)、仮定 (assumption) 、前提 (premise) などと呼び、下にある命題を後件 (succedent)、結論 (conclusion)、帰結 (consequent) などと呼ぶ。この記法は前件が証明されるとき後件も証明されることを意味する。

推論規則の重要な要件として健全性 (soundness) がある: \(P\), \(Q\), \(\ldots\) に真理値 (真または偽) を割り当てるとき、前件が真になる割り当てでは後件も真にならなければならない。つまり、公理から健全な推論規則を使って命題を証明するとき、証明される任意の命題は真になる。

自然で健全な推論規則は他にも多くある。例えば:

推論規則

\[ \frac{P \ \operatorname{\text{\footnotesize IMPLIES}}\ Q,\quad Q \ \operatorname{\text{\footnotesize IMPLIES}}\ R}{P \ \operatorname{\text{\footnotesize IMPLIES}}\ R} \]

推論規則

\[ \frac{\operatorname{\text{\footnotesize NOT}} (P) \ \operatorname{\text{\footnotesize IMPLIES}}\ \operatorname{\text{\footnotesize NOT}} (Q)}{Q \ \operatorname{\text{\footnotesize IMPLIES}}\ P} \]

一方で、次の規則は健全でない:

健全でない推論規則

\[ \frac{\operatorname{\text{\footnotesize NOT}} (P) \ \operatorname{\text{\footnotesize IMPLIES}}\ \operatorname{\text{\footnotesize NOT}} (Q)}{P \ \operatorname{\text{\footnotesize IMPLIES}}\ Q} \]

実際、\(P\) と \(Q\) にそれぞれ \(\textbf{T}\) と \(\textbf{F}\) を割り当てると、前件は真になるのに対して後件は偽になる。

公理と同様に、本講義では使用する推論規則の集合を形式的に定めることはしない。証明の各ステップが明確かつ「論理的」でありさえすればよい。特に、以前に証明した命題から新しい帰結を得るときは、どの命題を使用するかを書くべきである。

1.4.2 証明のパターン

理論上は、公理あるいは以前に証明した命題から始まって証明したい命題で終わる任意の論理的演繹が証明となる。最初はこの自由度に圧倒されるかもしれない。どのように証明を始めるべきかも分からない！

良いニュースがある: 多くの証明は標準的なテンプレートのいずれかに従っている。もちろん証明ごとに詳細は異なるものの、テンプレートを使えば穴を埋めるだけで証明が完成する。これから本章では標準的な証明のパターンをいくつか見ていきながら、基本的なアイデアとよくある落とし穴、そして具体的な例を説明する。多くのテンプレートは入れ子にできる: つまり、証明の大枠では一つのテンプレートを利用し、細かい部分では他のテンプレートを利用する証明が可能である。次章以降では、より高度な証明技法に触れる。