1 基本概念

命題論理は、個々の文の内容そのものよりも、真か偽かという値の組み合わせ方に注目する論理体系である。日常言語の断片的な発話を厳密に扱うための道具としてだけでなく、数学推論を整理する基盤としても機能する。基本単位命題と呼ばれ、これらを論理結合子でつないで複合的な式を作る。

1.1 命題

命題とは、真または偽のいずれかに定まる文や主張をいう。たとえば「2は偶数である」は真、「3は偶数である」は偽であるため、いずれも命題として扱える。一方、疑問文や命令文のように真偽を直接判定できない表現は、通常は命題に含めない。

1.2 真偽値

真偽値は、命題が真であるか偽であるかを表す値である。命題論理では、これを抽象化して扱うことで、内容の違う文同士でも同じ形式の推論として比較できる。古典的な体系では、真と偽の二値を採用するのが基本である。

1.3 論理結合子

論理結合子は、複数の命題を組み合わせて新しい命題を作る記号や演算である。代表的なものに否定、連言、選言、含意、同値がある。これらにより、単純な文から複雑な論理構造を表現できる。

1.3.1 否定

否定は、ある命題が真であるとき偽に、偽であるとき真にする操作である。記号では「でない」や ¬ で表されることが多い。命題の反対を作る最も基本的な結合子である。

1.3.2 連言

連言は、二つの命題がともに真である場合に限って真となる結合である。日本語では「かつ」に対応し、両方の条件を同時に満たす状況を表す。どちらか一方でも偽なら、全体は偽となる。

1.3.3 選言

選言は、少なくとも一方の命題が真であれば真となる結合である。ふつう「または」に対応し、広くは複数の可能性を許す表現として用いられる。命題論理では、包括的な意味での「または」が標準的である。

1.3.4 含意

含意は、「前件ならば後件」という形を表す結合である。前件が真で後件が偽のときだけ偽になり、それ以外では真とされる。条件付きの推論や規則形式化する際の中心的な記号である。

1.3.5 同値

同値は、二つの命題が同じ真偽値をもつときに真となる結合である。記号では ↔ などで表される。互いに同じ内容を別の形で言い換えている関係を示すのに向いている。

1.4 論理式

論理式は、命題変数と論理結合子を規則に従って組み合わせた表現である。単独の命題から始まり、より複雑な条件や推論を一つの構造として記述できる。論理学では、式の真偽や変形可能性が重要な研究対象となる。

2 意味論

意味論は、論理式がどのような条件で真になるかを定める枠組みである。構文が式の作り方を扱うのに対し、意味論はその式が何を意味し、どう評価されるかを明らかにする。命題論理では、真理値の割り当てを通して式全体の性質を調べる。

2.1 真理値評価

真理値評価は、各命題変数に真か偽を割り当て、そこから複合式の値を順に決める手続きである。結合子ごとの定義に従えば、任意の論理式の真偽を計算できる。これにより、抽象的な式でも具体的な条件下での挙動を調べられる。

2.2 真理

真理表は、命題変数のすべての真偽の組み合わせに対する論理式の値を一覧にした表である。各行が一つの評価を表し、式がどのような入力で真になるかを視覚的に示す。命題論理の基本的な検証手段として広く使われる。

2.3 恒真

恒真式は、どのような真理値割り当ての下でも常に真となる論理式である。論理的な妥当性を示す代表例であり、式そのものの内容に依存せず真である点に特徴がある。推論規則の正しさを確かめる際にも重要である。

2.4 矛盾

矛盾式は、どの評価のもとでも常に偽となる論理式である。互いに両立しない条件を一つの式にまとめたものとみなせる。恒真式とは対照的に、いかなる場合にも成立しない。

2.5 充足可能性

充足可能性とは、少なくとも一つの真理値割り当てで式が真になる性質である。ある式が充足可能であれば、完全に不可能な条件ではないといえる。反対に、どの割り当てでも真にならない式は充足不能であり、矛盾式に当たる。

3 推論と証明

命題論理では、個々の式の真偽だけでなく、複数の式から別の式が導けるかどうかが重視される。推論は、前提が与えられたときに結論が正当に得られるかを問う作業である。証明体系は、その導出を形式的な手順として整える。

3.1 妥当性

妥当性は、前提がすべて真である場合に結論も必ず真になる関係をいう。推論全体が意味論的に正しいとき、その議論は妥当であるとされる。命題論理の中心目標の一つは、この性質を厳密に判定することである。

3.2 論理的帰結

論理的帰結は、ある集合の前提から式が必然的に導かれるときに成り立つ関係である。記号的には、前提集合が結論を含意する形で表されることが多い。妥当性は、この帰結関係を用いて定式化できる。

3.3 推論規則

推論規則は、既知の式から新しい式を導くための正当な型である。これらは証明の各段階を支える基本部品であり、形式体系の操作規則として働く。適切に定められた規則に従えば、導出の各行が意味論的に保証される。

3.3.1 仮言三段論法

仮言三段論法は、「AならばB」「BならばC」から「AならばC」を導く規則である。条件の連鎖をまとめる働きをもち、含意の推論で頻出する。日常の論証でも自然に現れる型である。

3.3.2 分離規則

分離規則は、Aと「AならばB」からBを導く規則である。モーダス・ポネンスとも呼ばれ、命題論理の最も基本的な推論の一つである。条件が満たされたときに結論を取り出す役割を持つ。

3.3.3 連言導入

連言導入は、AとBがそれぞれ成り立つとき、AかつBを得る規則である。個別に確認された事実を一つの複合命題へまとめる。証明の中で情報統合する際に用いられる。

3.3.4 連言除去

連言除去は、AかつBからA、またはBを取り出す規則である。複合的な情報から必要な部分だけを抽出する操作に当たる。証明では、まとめた条件を再利用するときに便利である。

3.4 証明体系

証明体系は、許される推論規則と証明の書式を定めた枠組みである。自然演繹、シークエント計算、ヒルベルト体系など、さまざまな形式がある。いずれも、妥当な推論を機械的に扱えるようにすることを目的とする。

4 形式的性質と標準形

命題論理の式は、内容を変えずに別の形へ変形できることが多い。こうした同値変形を利用すると、式の比較や簡約が容易になる。標準形は、複雑な式を一定の形に整え、解析や計算をしやすくする方法である。

4.1 同値変形

同値変形は、真偽を保ったまま論理式を書き換える操作である。異なる見た目でも同じ意味を持つ式を相互に移せるため、証明や計算の整理に役立つ。代数的な変形に近い性質をもつ。

4.2 ド・モルガンの法則

ド・モルガンの法則は、否定と連言・選言の関係を与える基本法則である。たとえば「AかつBでない」は「Aでない、またはBでない」と同値になる。否定を内側へ移す際の標準的な道具として使われる。

4.3 分配法則

分配法則は、連言と選言が互いに分配し合う性質を示す。たとえば「Aかつ(BまたはC)」は「AかつB または AかつC」と同値である。式を展開したり整理したりする場面で役立つ。

4.4 ドゥアル性

ドゥアル性は、連言と選言、真と偽を入れ替えた対応を指す。ある定理が成り立つとき、その双対的な形も成り立つことが多い。命題論理の対称性を理解するうえで重要な観点である。

4.5 標準形

標準形は、論理式を決められた構造にそろえた表現である。等価な式を一様な形にすることで、比較や計算をしやすくする。命題論理では、連言標準形と選言標準形が代表的である。

4.5.1 連言標準形

連言標準形は、選言のまとまりを連言で結んだ形に整えた表現である。各節が比較的単純な条件の集合として扱えるため、機械処理に向いている。充足可能性の解析でも頻繁に用いられる。

4.5.2 選言標準形

選言標準形は、連言のまとまりを選言で並べた形である。複数の可能な状況を列挙するのに適しており、式の構造を明確にできる。論理式の整理や理論的比較で重視される。

4.6 論理式の簡約

論理式の簡約は、同値なまま式をより短く、扱いやすくする操作である。不要な部分を取り除いたり、重複をまとめたりして、計算量や理解の負担を減らす。実用面では、回路設計や自動処理と結びつくことが多い。

5 計算機科学への応用

命題論理は、計算機科学で非常に広く利用される。回路の動作、プログラムの正しさ、証明の自動化など、離散的な条件判定が必要な領域と相性がよい。論理式を計算可能な形で扱える点が、その応用範囲を広げている。

5.1 回路理論

回路理論では、論理ゲートの振る舞いを命題論理でモデル化する。入力信号と出力信号の関係を真理値として表せるため、複雑な回路も論理式として解析できる。設計の最適化や誤り検出にも役立つ。

5.2 プログラム検証

プログラム検証は、コードが意図した性質を満たすかを確かめる分野である。条件分岐やループの前後関係を論理式で記述すると、正しさの検討が体系化される。命題論理は、その基礎的な枠組みとして利用される。

5.3 自動定理証明

自動定理証明は、計算機を用いて論理的結論を導く技術である。命題論理は、探索や証明検索の対象として扱いやすく、アルゴリズム設計の基盤になる。形式化された証明を機械的に生成する手法の出発点でもある。

5.4 充足可能性問題

充足可能性問題は、与えられた論理式が真となる評価が存在するかを問う問題である。命題論理では代表的な決定問題として知られ、計算理論との結びつきが強い。回路検査、制約充足、推論の自動化など、多方面で重要な役割を果たす。