モデルが存在するとはどういうことか|充足可能性 - 記号論理学

充足可能性(satisfiability)は、論理式にモデルが存在するかどうかを問う概念です。モデルの存在は、論理式の「実現可能性」を意味し、数学基礎論において中心的な役割を果たします。

充足可能性の定義

論理式 φ(または論理式の集合 Γ)が充足可能(satisfiable)であるとは、φ を真にする構造(モデル)が存在することです。

記号では、M ⊨ φ となる構造 M が存在するとき、φ は充足可能といいます。

充足可能

モデルが存在する。「実現できる」状況がある。

充足不能

どの構造でも偽。矛盾した要求を含む。

充足可能性と妥当性

充足可能性と妥当性(validity)は密接に関連しています。

φ が妥当(すべての構造で真)であることと、¬φ が充足不能であることは同値です。

妥当性

すべての構造で真。⊨ φ と書く。トートロジーの一般化。

充足可能性

少なくとも一つの構造で真。モデルが存在する。

この関係から、妥当性の判定と充足不能性の判定は本質的に同じ問題であることがわかります。

理論とモデル

公理の集合 T を理論(theory)と呼びます。T のモデルとは、T に含まれるすべての公理を満たす構造のことです。

群論は、結合律、単位元の存在、逆元の存在という公理からなる理論です。群の公理をすべて満たす構造が群論のモデルであり、それが数学でいう「群」です。

公理の集合 T を定める

T のすべての公理を満たす構造を考える

それが T のモデル

無矛盾性と充足可能性

理論 T が無矛盾(consistent)であるとは、T から矛盾が導けないことです。完全性定理により、次が成り立ちます。

T が無矛盾 ⇔ T はモデルを持つ(充足可能)

この同値性は非常に重要です。無矛盾性という構文的な概念と、モデルの存在という意味論的な概念が一致するからです。

充足可能性の例

∃x(P(x) ∧ Q(x)) は充足可能です。台集合 {a} で、P も Q も真と解釈すれば、この式は真になります。

∀x(P(x) ∧ ¬P(x)) は充足不能です。どの構造でも、P(x) ∧ ¬P(x) は偽なので、その全称量化も偽です。

充足可能な式の例

∃x P(x)、∀x(P(x) → Q(x))、P(a) ∨ ¬P(a)

充足不能な式の例

P(a) ∧ ¬P(a)、∀x ¬(x = x)

有限モデルと無限モデル

充足可能な式でも、有限モデルしか持たない場合と、無限モデルを必要とする場合があります。

∃x∃y(x ≠ y) は「異なる2つの要素が存在する」を意味し、要素が2つ以上の構造でのみ真です。

∀x∃y(x < y) は「どの要素より大きい要素がある」を意味し、有限構造では真にできません。無限構造(自然数など)が必要です。

充足可能性問題

与えられた論理式が充足可能かどうかを判定する問題を、充足可能性問題といいます。

命題論理の充足可能性問題(SAT)は、NP完全として知られる重要な計算問題です。述語論理の充足可能性問題は決定不能、つまりアルゴリズムで一般的に解くことはできません。

ただし、述語論理はセミ決定可能です。充足不能な式は有限時間で検出できます(完全性定理より)。充足可能な式の確認は、一般には終わらない可能性があります。

次回は、コンパクト性定理について学びます。