「その議論、本当に正しい?」と思ったとき、その「正しさ」を厳密に定める学問が論理学です。この講義では、シンプルな命題論理から出発し、「すべての」「ある」を扱う述語論理、証明の限界を示すゲーデルの定理、そして計算機科学や哲学への応用まで順に追います。
ねらい — 「真か偽か」だけを扱う、もっともシンプルな論理の世界から始めよう。
命題(めいだい)とは「真か偽かが決まる文」のことです。「東京は日本の首都だ」(真)、「2+2=5」(偽)が命題の例です。命題変数 p, q, r などに ∧(かつ)∨(または)¬(でない)→(ならば)↔(同値)という「結合子(けつごうし)」を組み合わせると、複雑な命題を組み立てられます。
それぞれの結合子には「真理値表(しんりちひょう)」という対応表があり、組み合わせた命題の真偽は構成素の真偽から機械的に決まります。例えば「p かつ q」は p と q が両方真のときだけ真です。どんな真偽の組み合わせでも常に真になる命題を「トートロジー」、常に偽になる命題を「矛盾」と呼びます。
ねらい — 「すべての人間は死ぬ。ソクラテスは人間だ。よってソクラテスは死ぬ」——命題論理では表せないこの推論を扱う道具を学ぼう。
命題論理では「すべての人間は死ぬ」という文を一つの文字に圧縮するしかなく、「ソクラテスは人間だ」との関係を追えません。述語論理(じゅつごろんり)は、「P(x)」(x は死ぬ)という「述語(じゅつご)」と「∀x(すべての x)」「∃x(ある x が存在する)」という「量化子(りょうかし)」を導入して、この関係を表現できるようにします。
述語論理は「モデル」(もでる)を使って解釈されます。対象の集まり(例えば「人間全員」)と、その上で成り立つ関係(「x は死ぬ」)を決めると、論理式が真か偽かが決まります。一階述語論理(いっかいじゅつごろんり)は数学全体を基礎づける言語として使われています。
ねらい — 「証明」を機械的に検証できるルールの集まりとして捉えると、論理はコンピューターでも扱えるようになります。
自然演繹(しぜんえんえき)などの「証明体系(しょうめいたいけい)」は、推論で使えるルール(推論規則)をまとめたものです。証明とは「公理(こうり:証明なしに認める出発点)」から、推論規則だけを使って結論を導く、有限のステップの列のことです。機械的に確かめられるので、コンピューターでも検証できます。
証明体系には「健全性(けんぜんせい)」と「完全性(かんぜんせい)」という2つの重要な性質があります。健全性は「証明できる式は必ず真」、完全性は「真である式は必ず証明できる」という性質です。一階述語論理ではゲーデルの完全性定理が成り立ち、両者が一致します——「証明できる」と「真である」が同じことを意味するわけです。
ねらい — 「どんな数学も完全に証明しつくせる体系は作れない」——20世紀最大の発見の一つを、大まかに理解してみよう。
1931年、ゲーデルは驚くべきことを証明しました。「算術(整数の計算)を含む程度に強力な無矛盾な形式体系には、必ず『真だけど証明できない命題』が存在する」——これが第一不完全性定理です。つまり、どんなに頑張っても「すべての数学的真実を証明できる完全な体系」は作れないのです。20世紀初頭にヒルベルトが夢見た「数学を完全に形式化する計画」に、ゲーデルが終止符を打ちました。
第二不完全性定理はさらに踏み込んで「その体系は自分自身の無矛盾性を体系の中で証明できない」ことを示します。「私はこの文が証明できない」という命題を数式で構成するという天才的なアイデア(自己言及)が証明の核心です。論理学・哲学・計算理論に深い影響を与えた、20世紀でも指折りの知的成果です。
数学は「すべてを証明できる夢の体系」を持てない——ゲーデルが20世紀に届けた、驚くべき洞察。
ねらい — 論理学は純粋数学だけでなく、コンピューターのバグ検出や哲学にまで使われています。
様相論理(ようそうろんり)は「可能性(〜かもしれない)」や「必然性(必ず〜だ)」を扱える論理です。例えば「明日雨が降ることは可能だ」を ◇(可能)、「三角形の内角の和は必ず180度だ」を □(必然)で表します。哲学の認識論や、ソフトウェアの正しさを形式的に検証する時相論理(じそうろんり)に応用されています。
直観主義論理(ちょっかんしゅぎろんり)は「排中律(はいちゅうりつ)——P か not P のどちらかは必ず真——を認めない」論理です。「証明せずに存在を仮定してはいけない」という厳しい立場で、プログラムが正しく動くことを証明する研究と深く結びついています。Curry–Howard 対応(型理論)は「証明とプログラムが同じ構造を持つ」という発見で、論理と計算を統一する枠組みです。