コンテンツへスキップ
Topos Uranos
日本語

コンパクト性定理

要約

演繹は有限列であり、有限個の前提しか用いない。これに対して、論理式の無限集合の充足は、ただ一つの付値が値 11 を無限個の論理式に同時に与えることを要求し、その定義のどこにも有限部分を調べれば足りるとは書かれていない。コンパクト性定理は、それで足りると主張する。論理式の集合が充足可能であるのは、その有限部分集合がどれも充足可能であるとき、かつそのときに限る。この課はこれを、演繹を経由せずに、直接の意味論的論証によって証明する。変数 v1,v2,…v_1, v_2, \ldots の値を一つずつ固定し、各段階で、集合のどの有限部分集合も、すでに固定されたものを尊重する付値によってなお充足可能であるという不変量を保つ。可能な二つの選択のどちらもそれを保たないとすれば、その失敗の二つの有限な証拠の合併が前の不変量に矛盾する。そして最後に、各論理式は有限個の変数しかもたないので、一致補題によって充足される。変数には番号が付いているので、この構成は選択公理を必要としない。コンパクト性からはその同値な形（集合が充足不能であるのは、ある有限部分が充足不能であるとき、かつそのときに限る。論理式が集合の帰結であるのは、ある有限部分の帰結であるとき、かつそのときに限る）が導かれ、前の課の有限個の前提に対する完全性と合わせて、強完全性が導かれる。すなわち、Γ⊨φ\Gamma \models \varphi ならば Γ⊢φ\Gamma \vdash \varphi が、すべての集合 Γ\Gamma について成り立ち、ここから演繹と意味論的帰結はつねに一致する。この課は組合せ論的応用で終わる。有限部分の彩色からの無限グラフの彩色、無限の言明に隠れている有限の上界、そして論理式の集合が表現できるものの限界である。

学習目標

  1. 有限充足可能な集合を定義し、変数の値を逐次固定することによってコンパクト性定理を証明し、不変量、二つの証拠の論証、一致補題の役割と、構成が選択公理を必要としない理由を説明する。
  2. コンパクト性の同値な形、すなわち充足不能性の形と帰結の形を述べ、証明し、応用し、それぞれから他へ移る。
  3. コンパクト性、有限個の前提集合に対する完全性、単調性から強完全性を導き、そこから演繹と意味論的帰結の一致、および無矛盾性と充足可能性の一致を得る。
  4. 無限集合に関する組合せ論的問題（彩色、順序、マッチング）を論理式の集合に符号化し、コンパクト性によって解き、定理が保証することと保証しないことを区別する。

これまでの課から用いること

この課はほとんど全面的に意味論の中で進み、そこから次のことを用いる。付値とは関数 v ⁣:V→{0,1}v\colon V \to \{0, 1\} であり、集合 VV、すなわち変数 v1,v2,v3,…v_1, v_2, v_3, \ldots の集合の上で定義され、すべての論理式へ一意的に拡張される。付値が論理式の集合 Γ\Gamma を充足するとは（v⊨Γv \models \Gamma と書く）、その各論理式に値 11 を与えることであり、Γ\Gamma は、ある付値がそれを充足するとき充足可能、そうでないとき充足不能である。これらはすべて命題論理の意味論の課にあり、この課の中心的な道具である一致補題もそこにある。二つの付値が φ\varphi の変数（それは有限集合 V(φ)V(\varphi) をなす）の上で一致するならば、それらは φ\varphi に同じ値を与える。

意味論的帰結と同値の課からは、Γ⊨φ\Gamma \models \varphi の定義（Γ\Gamma を充足するどの付値も φ\varphi を充足する）、その構造的性質、とくに単調性（Γ⊆Δ\Gamma \subseteq \Delta かつ Γ⊨φ\Gamma \models \varphi ならば、Δ⊨φ\Delta \models \varphi）と第五の性質（充足不能な集合はすべての論理式を帰結にもつ）、そして帰結と充足不能性の定理、すなわち Γ⊨φ\Gamma \models \varphi であるのは Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} が充足不能であるとき、かつそのときに限る、を用いる。一般化されたド・モルガンの法則と分配法則の課からは値の補題を用いる。⋀i=1nφi\bigwedge_{i=1}^{n} \varphi_i が値 11 をとるのは、そのすべての項が値 11 をとるとき、かつそのときに限り、⋁i=1nφi\bigvee_{i=1}^{n} \varphi_i がそうであるのは、ある項が値 11 をとるとき、かつそのときに限る。最後に、⊤:=(v1→v1)\top := (v_1 \rightarrow v_1) はトートロジーであり、⊥:=¬⊤\bot := \neg\top は矛盾式である。

演繹の側では、形式的演繹体系の課が単調性（単調性：Γ⊆Δ\Gamma \subseteq \Delta かつ Γ⊢φ\Gamma \vdash \varphi ならば、Δ⊢φ\Delta \vdash \varphi）と有限性（有限性：Γ⊢φ\Gamma \vdash \varphi ならば、ある有限部分集合 Γ0\Gamma_0 で Γ\Gamma に含まれるものが Γ0⊢φ\Gamma_0 \vdash \varphi を満たす）を証明し、四つの演繹技法の課が、両者が本課程の体系（公理図式 A1、A2、A3、モーダス・ポネンス、二重否定の置換（二重否定置換））で成り立つことを確かめた。以下、記号 ⊢\vdash はこの体系を指す。最後に、健全性と完全性の課が健全性定理（Γ⊢φ\Gamma \vdash \varphi ならば Γ⊨φ\Gamma \models \varphi、すべての Γ\Gamma について）と有限個の前提集合に対する完全性を証明した。{γ1,…,γk}⊨φ\{\gamma_1, \ldots, \gamma_k\} \models \varphi ならば、{γ1,…,γk}⊢φ\{\gamma_1, \ldots, \gamma_k\} \vdash \varphi である。