1.1 命題

次に二つの命題を示す。一つ目の命題は真であり、二つ目の命題は偽である:

「正しさが真または偽のいずれか」という条件は何も意味していないと思ったかもしれない。この条件は「どうしてあなたはロメオなの？」や「A をよこせ！」といった文を命題に含めないために存在する。また、状況によって真偽が変化する「今は五時だ」や「明日の株価は上がる」といった文もこの条件によって命題ではなくなる。

残念ながら、命題の真偽が常に簡単に分かるとは限らない:

(素数とは、\(1\) より大きい整数であって \(1\) と自身以外の正整数で割り切れないものを言う。素数を小さい順に五個並べると \(2\), \(3\), \(5\), \(7\), \(11\) となる。) この命題の真偽を確かめるために数値実験を行ってみよう。次のように \(p(n)\) を定義する¹:

まず \(p(0) = 41\) は素数である。その後

も全て素数となる。ふむ、もしかしたら主張 1.1.3 は真なのかもしれない。実際、\(n=39\) とした \(p(39) = 1601\) まで \(p(n)\) は全て素数となる。

しかし \(p(40) = 40^{2} + 40 + 41 = 41 \cdot 41\) は素数でない。よって主張 1.1.3 は偽と分かる: 「全ての非負整数 \(n\) に対して \(p(n)\) は素数である」は正しくない。実は、全ての非負整数を素数に対応付ける整数係数多項式は (定数を除いて) 存在しないことを示すのは難しくない (問題 1.25)。この例が示すのは、一般に無限集合に関する命題は有限のサンプルだけでは (どれだけサンプルが多くても) 真偽を確認できないという事実である。

なお、「全ての自然数で \(\cdots\) 」や「全ての要素で \(\cdots\) 」の形をした命題は非常によく現れるので、専用の記法が存在する。この記法を使うと、主張 1.1.3 は次のように書ける:

ここで使われている記号 \(\forall\) は「全ての \(\cdots\) について (for all \(\ldots\))」を意味する。記号 \(\mathbb{N}\) は非負整数 \(0\), \(1\), \(2\), \(3\), \(\ldots\) 全体の集合を表す (\(\mathbb{N}\) の要素を全部知りたいときは教官に聞いてみよ)。記号 \(\in\) は「 \(\cdots\) に属する」あるいは「 \(\cdots\) の要素である」を意味する。\(\mathbb{N}\) の後にあるピリオドは文節を分けるためだけにある。

もっと極端な命題の例を二つ示す:

Euler はこの命題の成立を 1769 年に予想した。しかし 218 年後、マサチューセッツ通り沿いにあるリベラルアーツ大学に通っていた Noamノーム Elkiesエルキース が予想を否定的に解決した。彼が発見した反例は \(a = 95800\), \(b = 217519\), \(c = 414560\), \(d = 422481\) だった。

この Euler による予想を論理的な記法を使って書き換えたものを次に示す:

ここで \(\mathbb{Z}^{+}\) は正整数全体の集合を表す。この命題のように \(\forall\) が連続するときは、読みやすいように短縮系が使われることが多い:

サンプリングだけで反例を見つけるのが難しい命題の例をもう一つ示す: 方程式を満たす最小の \(x\), \(y\), \(z\) はそれぞれ \(1000\) 桁以上にもなる！

証明が見つかるまでに数世紀を要した有名な問題をさらにいくつか紹介しよう:

この定理の間違った証明はいくつも発表されてきた。十九世紀末に発表されたある証明など、間違いが十年間も指摘されないままだった。四色定理の長大な正しい証明は 1976 年に数学者 Appelアッペル と Hakenハーケン によって示された。彼らの証明では複雑なコンピュータープログラムを使って四色で彩色可能な地図を分類する手法が利用された。そのプログラムで分類できない数千種類の地図は Haken と彼の助手によって手動で確認された ── 助手の一人は Haken の 15 才の娘だった。

この証明の正しさを疑うのには十分な理由があった ── 証明が長すぎて、コンピューターを使わなければ検証できなかったからである。誰もコンピューターの計算が正しいことを保証できず、数千個の地図が手動で正しく彩色できていることを再検証する労力を割こうとする者もいなかった。それから二十年後、人間が読解可能な四色定理の証明が発表された。ただし、この証明でも数百個の特別な地図の彩色可能性を調べるためにコンピューターが使用されている³。

1630 年、Fermat は読んでいた本に「この命題の真に驚くべき証明を見つけたが、この本の余白が狭すぎて記すことができない」と書き込んだ。それから数百年の間に \(n\) が \(4{,}000{,}000\) 以下の場合に対する命題は証明された。しかし、それだけでは全ての \(n\) で命題が成り立つかどうかは分からない。この点で、Fermat の最終定理は先述の Euler による予想と似た状況にあった。ついに 1994 年、英国人数学者 Andrewアンドリュー Wilesワイルズ が証明を発表した。七年間にわたって屋根裏部屋で誰にも知らせずに行われた孤独な研究の結果だった。彼の証明はどんな本の余白にも収まらない⁴。

最後に、簡単に表明できるものの真偽が分かっていない命題の例をもう一つ示す:

この予想は 1742 年に初めて公表された。\(10^{18}\) までの全ての偶数に対して成り立つことが分かっているものの、全ての偶数に対して成り立つかどうかは誰にも分からない。

情報科学者にとって最も重要な証明はプログラムやシステムの正しさ ── 期待通りに動作すること ── の証明である。誰もが知るようにプログラムはバグを含みがちなので、プログラムの正しさを証明する手法に取り組む研究者や実務者のコミュニティは近年規模を増している。この取り組みは CPU チップの設計で大きな成功を収めており、チップの正しさを証明することで過去に発生した悪名高いバグの一部を完全に避けられるようになっている。

プログラムとシステムを検証する数学的手法の開発は現在でも活発な研究領域である。第 5 章では、そういった手法をいくつか紹介する。