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

健全性と完全性

要約

前の二つの単元は、同じ言語の上に、前提から「出てくる」ことの二つの概念を築いた。一つは演繹 Γ⊢φ\Gamma \vdash \varphi であり、公理と規則によって記号列から記号列を得るが、それらが何を意味するかは問わない。もう一つは意味論的帰結 Γ⊨φ\Gamma \models \varphi であり、付値を調べ尽くすが、演繹は一つも書かない。この課では、有限の前提集合の場合に二つの概念が一致することを証明する。健全性（Γ⊢φ⇒Γ⊨φ\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi）は演繹の行数に関する累積帰納法によって証明され、公理ごと、規則ごとに一つの場合があり、二重否定置換の規則の場合もそこに含まれる。そこから体系の無矛盾性と、ある論理式が導出不可能であることを証明する方法が導かれる。逆向き、すなわち完全性には新しい道具が必要である。それがカルマーの補題であり、論理式の真理値表の各行を演繹に変換する。その複雑さに関する帰納法には複合的な場合が一つしかない。否定論理和が唯一の原始結合子だからである。この場合のために、否定論理和に関する二つの補題を体系の中で演繹する。続いて、行を固定する仮定を場合分けの証明によって一つずつ消去すると、すべてのトートロジーが定理であることが得られ、さらに二つの演繹定理によって、有限の前提集合の帰結はすべてその集合から演繹できることが得られる。ここから、有限の前提からの導出可能性が決定可能であること、および証明可能な同値と意味論的同値が一致することが従う。無限の前提の場合は次の課に残される。それにはコンパクト性定理が必要だからである。

学習目標

  1. 健全性と完全性を弱い形、有限の形、強い形で述べ、それらを独立な性質として区別し、完全性を「健全性によって」得る議論がなぜ循環しているかを説明する。
  2. 行数に関する累積帰納法によって、二重否定置換の規則の場合も含めて健全性を証明し、それを使って体系の無矛盾性と具体的な論理式の導出不可能性を証明する。
  3. 否定論理和に関する二つの補題を本コースの体系の中で演繹し、それらを使って、複雑さに関する帰納法によりカルマーの補題を証明する。
  4. 仮定を場合分けの証明で消去して弱完全性を証明し、二つの演繹定理によって有限の前提集合に関する完全性を証明する。
  5. 演繹と帰結の一致を用いて、導出可能性、証明可能な同値、無矛盾性を判定し、体系に規則を加えたときに何が起こるかを分析する。

本コースの体系についての二つの問い

演繹に関する単元は本コースの体系を定めた。ウカシェヴィチの公理図式 A1、A2、A3 と二つの規則、すなわちモーダス・ポネンス（MP）と二重否定置換（二重否定置換）である。後者は四つの演繹技法の課が二重否定を証明した後に加えたものである。集合 Γ\Gamma からの演繹とは論理式の有限列であって、その各論理式は公理であるか、Γ\Gamma の要素であるか、先行する二つの論理式にモーダス・ポネンスを適用した結果であるか、先行する一つの論理式に二重否定置換を適用した結果である。そして Γ⊢φ\Gamma \vdash \varphi は、Γ\Gamma からの演繹であって最後の論理式が φ\varphi であるものが存在することを意味する。意味論に関する単元は、意味論的帰結と同値の課で関係 Γ⊨φ\Gamma \models \varphi を定義した。すなわち、Γ\Gamma のすべての論理式を充足する付値はすべて φ\varphi を充足する。二つの関係は同じ形で書かれ、左に集合、右に論理式が置かれる。しかし、その性質は正反対である。前者は構文論的で存在的である。それは、有限なもの、すなわち演繹が存在し、それを記号ごとに確かめられると主張する。後者は意味論的で全称的である。それはすべての付値について何かを主張するが、付値は無限に多く、そのそれぞれが無限に多くの変数に値を与える。

そこで体系について二つの問いが立つ。第一に、体系は演繹すべきものだけを演繹するか。各集合 Γ\Gamma と各論理式 φ\varphi について、Γ⊢φ\Gamma \vdash \varphi ならば Γ⊨φ\Gamma \models \varphi であるとき、体系は健全であるという。前提から演繹されるものは、前提を真にするあらゆる付値のもとで真である。第二に、体系は演繹すべきものをすべて演繹するか。Γ⊨φ\Gamma \models \varphi ならば Γ⊢φ\Gamma \vdash \varphi であるとき、体系は完全であるという。完全性には、どの前提集合を扱うかに応じて三つの段階がある。

  • 弱完全性：⊨φ\models \varphi ならば ⊢φ\vdash \varphi。すべてのトートロジーは定理である。
  • 有限の前提集合に関する完全性：{γ1,…,γk}⊨φ\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi ならば {γ1,…,γk}⊢φ\{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi。
  • 強完全性：Γ⊨φ\Gamma \models \varphi ならば Γ⊢φ\Gamma \vdash \varphi。ここで Γ\Gamma は任意の集合であり、無限でもよい。

この課では健全性と、完全性の最初の二つの段階を証明する。三つ目はコンパクト性定理の課で証明する。なぜこのように分けるのかは、この課の最後で説明する。

言うべきでないこと

スペイン語では健全性が「solvencia」と呼ばれることがあるが、これは英語 soundness の直訳である。スペイン語の用語は「corrección」であり、本コースの日本語の用語は「健全性」である。また、健全性を体系の「表現の集合から一つの表現を推論する」性質と定義すべきでもない。それは導出可能性そのものであって、体系の性質ではない。しかし、本質的な誤りは別の二つである。

一つ目は、健全性と完全性が「互いに推論できる」と言うことである。両者は独立な性質である。ウカシェヴィチの体系は、二重否定置換の規則がなければ、健全である（この課の証明から一つの場合を除けばそれが示される）が、完全ではない（形式的演繹体系の課は、この体系が演繹しないトートロジーを示した）。また、すべての論理式を公理とする体系は、完全であるが健全ではない。例題 2 で両方の例を調べる。

二つ目はより重大である。循環した議論を完全性の証明として示すからである。その要点はこうである。φ⊬ψ\varphi \nvdash \psi ならば、演繹定理により ⊬(φ→ψ)\nvdash (\varphi \rightarrow \psi)。「健全性によって」⊭(φ→ψ)\not\models (\varphi \rightarrow \psi)。意味論的演繹定理により φ⊭ψ\varphi \not\models \psi。しかし健全性が言うのは、導出可能なものは恒真であるということであり、その対偶が言うのは、恒真でないものは導出可能でないということである。

⊢χ  ⇒  ⊨χ,⊭χ  ⇒  ⊬χ\vdash \chi \;\Rightarrow\; \models \chi, \qquad \not\models \chi \;\Rightarrow\; \nvdash \chi

議論のその一歩は逆向き、すなわち ⊬χ\nvdash \chi から ⊭χ\not\models \chi へと進んでおり、これは ⊨χ⇒⊢χ\models \chi \Rightarrow \vdash \chi の対偶、つまり弱完全性である。もしそうであれば、この議論は証明しようとするものを前提している。したがって、完全性は「簡単な仕方で推論される」ものではない。それは本コースで最も深い結果であり、その証明がこの課の大部分を占める。最後に、完全性を「真であるすべての表現には証明がある」とまとめるのは不正確である。証明をもつのは恒真な論理式、すなわちあらゆる付値のもとで真であるものであって、ある付値のもとで真であるものではない。変数 v1v_{1} は多くの付値のもとで真であるが、定理ではない。