⟐ 数学の作り方 How to make Mathematics

↑ ↓ 移動 Enter 開く Esc 閉じる

第3章 健全性と完全性（命題論理）

「導ける」と「正しい」は一致するのか

ここまでで2つの正しさを手にしました。意味論の ⊨φ\models\varphi（全付値で真）と、構文の ⊢φ\vdash\varphi （規則で導ける）。定義はまったく無関係です。片方は無限の付値を見渡し、もう片方は有限の記号操作。 この2つがぴったり一致するなら、それは驚くべきことです。

⊢φ  ⟺  ⊨φ.\vdash\varphi \iff \models\varphi.

左向き（⊢⇒⊨\vdash\Rightarrow\models）を健全性、右向き（⊨⇒⊢\models\Rightarrow\vdash）を完全性といいます。 健全性は「導けたものは本当に正しい」（体系が嘘をつかない）、完全性は「正しいものは必ず導ける」 （体系に穴が無い）。この章では両方を完全に証明します。とくに完全性の証明で編み出す 「無矛盾なら充足可能」という技法（極大無矛盾集合）は、次章以降の述語論理の完全性 （ゲーデル、第7章）の縮小版であり、この分野で最も重要な証明技術です。

健全性＝導けたものは正しい。完全性＝正しいものは導ける。両者で ⊢\vdash と ⊨\models が一致する。

健全性

定理 健全性定理

Γ⊢φ⇒Γ⊨φ\Gamma\vdash\varphi \Rightarrow \Gamma\models\varphi。特に ⊢φ⇒⊨φ\vdash\varphi\Rightarrow\models\varphi。

証明

Γ⊢φ\Gamma\vdash\varphi の証明 θ1,…,θn=φ\theta_1,\dots,\theta_n=\varphi の各 θk\theta_k について 「Γ\Gamma を真にする任意の付値 vv で vˉ(θk)=T\bar v(\theta_k)=\mathrm T」を kk に関する帰納法で示す。

まず公理はすべてトートロジーである（真理値表で確認できる。例：(A1) φ→(ψ→φ)\varphi\to(\psi\to\varphi) は vˉ(φ)=F\bar v(\varphi)=\mathrm F なら前件が偽で真、vˉ(φ)=T\bar v(\varphi)=\mathrm T なら後件 ψ→φ\psi\to\varphi が真で真。(A2),(A3) も同様）。

  • θk\theta_k が公理なら、トートロジーゆえ全付値で真、特に vv で真。
  • θk∈Γ\theta_k\in\Gamma なら、vv は Γ\Gamma を真にするので真。
  • θk\theta_k が θi, θj=θi→θk\theta_i,\ \theta_j=\theta_i\to\theta_k からの MP なら、帰納法の仮定で vˉ(θi)=vˉ(θi→θk)=T\bar v(\theta_i)=\bar v(\theta_i\to\theta_k)=\mathrm T。 →\to の真理値規則より vˉ(θk)=T\bar v(\theta_k)=\mathrm T。

よって vˉ(φ)=T\bar v(\varphi)=\mathrm T。vv は任意だったから Γ⊨φ\Gamma\models\varphi。∎

健全性の証明は素直です。公理が真で、MP が真を保つ——この2点だけで、導出のどの段も真だと言える。 逆の完全性は、はるかに深い議論を要します。

無矛盾性と充足可能性

完全性を「⊨⇒⊢\models\Rightarrow\vdash」の形で直接示すのは難しいので、対偶と、意味論・構文の橋になる次の言葉を使います。

定義 無矛盾

論理式の集合 Γ\Gamma が無矛盾（consistent）とは、ある論理式 φ\varphi について Γ⊢φ\Gamma\vdash\varphi と Γ⊢¬φ\Gamma\vdash\lnot\varphi が同時には成り立たないこと。 （同値：Γ⊬⊥\Gamma\not\vdash\bot。矛盾した集合からは任意の式が導ける＝爆発律による。）

完全性の核心は次のモデル存在定理に凝縮されます。「証明で矛盾しないもの（構文）は、必ず現実のモデルをもつ（意味論）」。

定理 モデル存在定理（命題論理）

Γ\Gamma が無矛盾ならば、Γ\Gamma は充足可能（Γ\Gamma の全要素を真にする付値が存在）。

これさえ言えれば完全性は一瞬で出ます（後述）。証明は2段構え：(1) 無矛盾な Γ\Gamma を、 これ以上式を足せない極限まで膨らませ（極大無矛盾集合）、(2) その極大集合から付値を読み取る、という流れです。

完全性の証明

段階1：リンデンバウムの補題（極大無矛盾集合への拡大）

定義 極大無矛盾集合

Δ\Delta が極大無矛盾とは、無矛盾であって、かつ Δ\Delta に属さないどの論理式を加えても矛盾すること。

補題 リンデンバウムの補題

任意の無矛盾集合 Γ\Gamma は、ある極大無矛盾集合 Δ⊇Γ\Delta\supseteq\Gamma に拡大できる。

証明

論理式は可算個なので φ0,φ1,φ2,…\varphi_0,\varphi_1,\varphi_2,\dots と一列に並べられる。Δ0=Γ\Delta_0=\Gamma とし、 Δn+1={Δn∪{φn}(Δn∪{φn} が無矛盾)Δn(そうでない)\Delta_{n+1}=\begin{cases}\Delta_n\cup\{\varphi_n\} & (\Delta_n\cup\{\varphi_n\}\ \text{が無矛盾})\\ \Delta_n & (\text{そうでない})\end{cases} と定める。各 Δn\Delta_n は無矛盾（帰納的に）。Δ=⋃nΔn\Delta=\bigcup_n\Delta_n とおく。

Δ\Delta は無矛盾：もし Δ⊢⊥\Delta\vdash\bot なら、その証明は有限個の式しか使わないので、ある Δn\Delta_n で すでに Δn⊢⊥\Delta_n\vdash\bot となり無矛盾性に反する。

Δ\Delta は極大：φn∉Δ\varphi_n\notin\Delta とすると、Δn+1\Delta_{n+1} の定め方から Δn∪{φn}\Delta_n\cup\{\varphi_n\} は矛盾していた。 よって Δ∪{φn}⊇Δn∪{φn}\Delta\cup\{\varphi_n\}\supseteq\Delta_n\cup\{\varphi_n\} も矛盾する。∎

「式を一つずつ吟味し、足しても矛盾しないなら足す」を全論理式について行う。有限性（証明は有限個しか使わない）が、 無限回の操作の後でも無矛盾性を保証する要です。可算だから番号づけできましたが、非可算な言語では ここでツォルンの補題（選択公理）を使います——次章以降の伏線です。

段階2：極大無矛盾集合の性質

補題 極大無矛盾集合の完全性

Δ\Delta が極大無矛盾なら、任意の論理式 φ,ψ\varphi,\psi について： （a）Δ⊢φ  ⟺  φ∈Δ\Delta\vdash\varphi \iff \varphi\in\Delta（演繹で閉じている）。 （b）φ∈Δ\varphi\in\Delta または ¬φ∈Δ\lnot\varphi\in\Delta のちょうど一方が成り立つ。 （c）(φ→ψ)∈Δ  ⟺  (φ∉Δ(\varphi\to\psi)\in\Delta \iff (\varphi\notin\Delta または ψ∈Δ)\psi\in\Delta)。

証明

（a）⇐\Leftarrow は自明。⇒\Rightarrow：Δ⊢φ\Delta\vdash\varphi かつ φ∉Δ\varphi\notin\Delta とすると、極大性より Δ∪{φ}\Delta\cup\{\varphi\} は矛盾、演繹定理から Δ⊢¬φ\Delta\vdash\lnot\varphi。これと Δ⊢φ\Delta\vdash\varphi で Δ\Delta が矛盾し不合理。

（b）両方属すれば Δ\Delta が矛盾するので、多くて一方。少なくとも一方：φ∉Δ\varphi\notin\Delta なら極大性で Δ∪{φ}\Delta\cup\{\varphi\} は矛盾、演繹定理で Δ⊢¬φ\Delta\vdash\lnot\varphi、(a) より ¬φ∈Δ\lnot\varphi\in\Delta。

（c）⇒\Rightarrow：(φ→ψ)∈Δ(\varphi\to\psi)\in\Delta かつ φ∈Δ\varphi\in\Delta なら MP で Δ⊢ψ\Delta\vdash\psi、(a) で ψ∈Δ\psi\in\Delta。 ⇐\Leftarrow：φ∉Δ\varphi\notin\Delta なら (b) で ¬φ∈Δ\lnot\varphi\in\Delta、¬φ⊢φ→ψ\lnot\varphi\vdash\varphi\to\psi（爆発律的に導ける）ゆえ (φ→ψ)∈Δ(\varphi\to\psi)\in\Delta。ψ∈Δ\psi\in\Delta なら (A1) と MP で (φ→ψ)∈Δ(\varphi\to\psi)\in\Delta。∎

(b)(c) が言っているのは、極大無矛盾集合が真理値表の規則そのものを満たすということ。 「Δ\Delta に属する ＝ 真」とみなせば、¬\lnot も →\to も付値の規則どおりに振る舞う。これで付値が作れます。

段階3：真理補題とモデル存在定理

証明

Δ⊇Γ\Delta\supseteq\Gamma を極大無矛盾集合（リンデンバウム）とし、付値を v(p):=T  ⟺  p∈Δv(p):=\mathrm T \iff p\in\Delta で定める。真理補題「任意の論理式 φ\varphi について vˉ(φ)=T  ⟺  φ∈Δ\bar v(\varphi)=\mathrm T \iff \varphi\in\Delta」を 構造的帰納法で示す。原子式は vv の定義そのもの。¬φ\lnot\varphi：vˉ(¬φ)=T  ⟺  vˉ(φ)=F  ⟺  φ∉Δ  ⟺  ¬φ∈Δ\bar v(\lnot\varphi)=\mathrm T \iff \bar v(\varphi)=\mathrm F \iff \varphi\notin\Delta \iff \lnot\varphi\in\Delta（最後は補題(b)）。φ→ψ\varphi\to\psi：真理値規則と補題(c) が そのまま対応する。

よって Δ⊇Γ\Delta\supseteq\Gamma の全要素が vv で真、すなわち Γ\Gamma は充足可能。モデル存在定理が示せた。∎

定理 完全性定理（命題論理）

Γ⊨φ⇒Γ⊢φ\Gamma\models\varphi \Rightarrow \Gamma\vdash\varphi。

証明

対偶を示す。Γ⊬φ\Gamma\not\vdash\varphi と仮定する。すると Γ∪{¬φ}\Gamma\cup\{\lnot\varphi\} は無矛盾 （もし矛盾すれば演繹定理から Γ⊢¬¬φ\Gamma\vdash\lnot\lnot\varphi、二重否定除去で Γ⊢φ\Gamma\vdash\varphi となり仮定に反する）。 モデル存在定理より Γ∪{¬φ}\Gamma\cup\{\lnot\varphi\} は充足可能——Γ\Gamma を真にし φ\varphi を偽にする付値がある。 これは Γ⊨φ\Gamma\models\varphi を否定する。ゆえに Γ⊭φ\Gamma\not\models\varphi。∎

健全性とあわせ、⊢\vdash と ⊨\models は完全に一致します。有限の記号操作で、無限の付値にわたる真理を 過不足なく捉えられる——論理学最初の到達点です。

コンパクト性

完全性の“ご褒美”として、意味論だけを見ていては非自明な定理が転がり出ます。

定理 コンパクト性定理（命題論理）

論理式の集合 Γ\Gamma が充足可能   ⟺  \iff Γ\Gamma のすべての有限部分集合が充足可能。

証明

⇒\Rightarrow は自明。⇐\Leftarrow：対偶で、Γ\Gamma が充足不能なら有限部分が充足不能、を示す。 Γ\Gamma が充足不能なら（モデル存在定理の対偶で）Γ\Gamma は矛盾、すなわち Γ⊢⊥\Gamma\vdash\bot。 この証明は有限個の Γ\Gamma の要素しか使わない。その有限部分 Γ0\Gamma_0 で Γ0⊢⊥\Gamma_0\vdash\bot、 健全性より Γ0\Gamma_0 は充足不能。∎

証明の心臓は「⊢\vdash の証明は有限」という一点。無限の条件（Γ\Gamma 全体の充足可能性）が、 有限の条件（各有限部分）に還元される。この「無限を有限に落とす」構図は、名前のとおり 位相空間のコンパクト性と深く通じており、実際 {T,F}変数\{\mathrm T,\mathrm F\}^{\text{変数}} に 積位相を入れてチコノフの定理から証明することもできます。次章以降、述語論理でもコンパクト性は 「無限の情報を有限で操る」最強の道具になります。

つまずきポイント

注意 よくある誤解

  • 健全性と完全性は別の主張。 健全性（導ける⇒正しい）は易しく、完全性（正しい⇒導ける）は難しい。「完全」は体系に穴が無いこと（第13章の不完全性とは別概念）。
  • 完全性 vs 不完全性。 ゲーデルの完全性定理（第7章）は「妥当な式は導ける」、不完全性定理（第13章）は「算術には決定できない命題がある」。矛盾せず、対象が違う。
  • モデル存在定理が完全性の本体。 「無矛盾⇒充足可能」を示せば、完全性もコンパクト性も系として出る。この技法を身につけるのが最重要。

この章のまとめ

  • 健全性（⊢⇒⊨\vdash\Rightarrow\models）は「公理が真・MP が真を保つ」で素直に証明できる。
  • 完全性（⊨⇒⊢\models\Rightarrow\vdash）の本体はモデル存在定理「無矛盾⇒充足可能」。リンデンバウムで極大無矛盾集合へ拡大し、その帰属関係から付値を読み取り（真理補題）モデルを作る。
  • 系としてコンパクト性が出る。心は「証明は有限個しか使わない」。⊢\vdash と ⊨\models は完全に一致する。

命題論理を完全に把握しました。次章から、量化子 ∀,∃\forall,\exists をもつ一階述語論理へ進み、まず構文を厳密に立てます。