命題論理：基礎、構造、歴史、応用

概要

命題論理は、文論理または命題計算とも呼ばれ、真または偽のいずれかである文を表現し、それについて推論するための形式的な数学体系である。命題全体をそれ以上分解しない単位として扱い、論理結合子によって結び付けることで、各部分の真理値に依存する複合命題を形成する。形式的な扱いでは、この分野は形式体系として提示され、数学および論理学の文脈では命題計算と呼ばれることが多い。

基本要素と記法

基本となる要素は、命題と呼ばれる原子的な単位である。非形式的には、真または偽という明確な真理値をもつ平叙文を指す。形式的な文献では、これらを原子記号の集合としてまとめ、それぞれを命題と呼ぶことがある。付値は各原子命題に真理値を割り当てる。通常はP、Q、Rなどの大文字を原子命題に用い、少数の結合子によって論理式を組み立てる。P、Q、Rのような慣用的な文字は標準的な代用記号である。

代表的な論理結合子には、次のものがある。

• 連言（AND、∧で表す）、
• 選言（OR、∨で表す）、
• 否定（NOT、¬で表す）、
• 含意（IF...THEN。通常は→で表し、実質含意ともいう）、
• 双条件（IF AND ONLY IF。↔、またはiffで表す）。

構文論と意味論

論理式は、構文規則に従って原子命題や他の論理式に結合子を適用することで作られる。意味論では、原子命題への付値を前提として論理式に真理値を与える。複合論理式の真理値は通常の真理値表によって定義され、たとえば連言が真となるのは、二つの連言肢がともに真である場合に限られる。重要な意味論上の概念には、恒真式（常に真）、矛盾（常に偽）、充足可能性（ある付値の下で真）、偶然性（真となる場合も偽となる場合もある）がある。

推論と証明

命題論理では、モーダス・ポネンス（PおよびP→QからQを導く）などの推論規則、ならびに公理的計算、自然演繹、シーケント計算といった証明体系が用いられる。これらの体系は、与えられた前提から新たな論理式をどのように導出できるかを形式化する。真理値表の全列挙によって決定可能であるため、命題論理における妥当性はアルゴリズムで検査できる。しかし、多くの実用的な判定問題は充足可能性に帰着され、ブール充足可能性問題（SAT）はNP完全であることが知られる中心的な計算課題である。

標準形と計算

あらゆる命題論理式は、連言標準形（CNF）や選言標準形（DNF）などの標準的な等価形に変換できる。CNFは自動推論および現代的なSATソルバーにとり特に重要であり、これらは充足する割当てを探索するか、充足不能であることを証明する。命題論理はブール代数とデジタル回路の設計の基盤でもあり、デジタル回路では論理演算がゲートによって実装される。

歴史、拡張、応用

命題的推論の考え方は古代にさかのぼるが、代数的・形式的な特徴付けは19世紀から20世紀初頭にかけて発展した。とりわけブール代数や、記号体系を確立した論理学者たちの形式的研究が重要である。命題論理はより豊かな体系の基礎をなす。たとえば述語論理は、対象とその性質について推論するために量化子と述語を加え、様相論理は必然性と可能性のための演算子を導入する。実用上の用途には、デジタル回路設計、プログラム検証、知識表現、自動定理証明が含まれる。詳しい学習や形式的な定義については、以下にリンクされた入門書およびオンライン資料を参照されたい。

形式的な入門 • 用語と計算 • 数学的文脈 • 論理学の基礎 • 原子命題の集合 • 原子命題 • 真理値 • 記法 • 含意 • 双条件 • 述語論理