メタ理論：まとめと挑戦課題

要約

この課は、メタ理論に充てられた単元を締めくくり、それとともにコースの内容を締めくくる。この課は演繹の鎖を再構成する。すなわち、公理の恒真性から体系の健全性へ、否定論理和についての二つの補題からカルマーの補題を経て有限個の前提に対する完全性へ、二つの証拠の補題からコンパクト性定理へ、そしてそれを介して強い完全性へ、節形式から融合法の健全性と反駁完全性へと至る鎖であり、各環について、それがどの結果を用い、どの課で証明されたかを示す。また、コースの先立つ三つの部分、すなわち言語、演繹、意味論が $\vdash$ と $\models$ の一致にどのように収束し、それぞれがこの一致に何を寄与するかを示し、コースが証明したもの、認めたもの、未解決のまま残したものを区別する。まとめテストでは導入テストの技能を繰り返し、最後に、各課の演習より難しく、複数の課の道具を組み合わせることを求める六つの挑戦課題を示す。

学習目標

単元の結果の論理的な順序を再構成し、各結果がどの先行する結果に依拠し、どの課で証明されたかを示し、コンパクト性と強い完全性の順序の理由を説明する。
言語、演繹、意味論が $\vdash$ と $\models$ の一致にどのように収束するか、そしてコースの各単元のどの結果がこの一致に不可欠であるかを説明する。
コースが証明したもの、認めたもの（公理図式、原始規則、帰納法）、未解決のまま残したもの（充足可能性を判定するコストと量化子をもつ論理）を区別する。
標識、カルマーの補題、一様代入、コンパクト性、融合を組み合わせる問題を解き、それぞれの場合に一致の易しい側を利用する。

この単元で得られたもの

この単元の目標は、先行する単元が同じ言語の上に築いた二つの関係、すなわち導出可能性 $\Gamma \vdash \varphi$ と意味論的帰結 $\Gamma \models \varphi$ を比較し、両者が一致することを証明することであった。この目標は、言明としては留保なしに達成された。前提の任意の集合について、有限であれ無限であれ、両者は同一の関係であり、融合は帰結を判定する第三の方法を与え、それもまた健全かつ完全である。留保は方法にあり、それぞれはしかるべき箇所で述べられた。第一の課の完全性は構成的だが実用的ではない。それが生み出す演繹は真理値表と同じだけ長いからである。コンパクト性は付値の存在を保証するが、それを見つける方法は教えない。融合は判定を行うが、最悪の場合のコストは未解決の問題である。これらの留保を踏まえれば、たどった道は、四つの区間からなる演繹の鎖として読むことができる。

健全性

健全性と完全性の課は、まず用語を定めた。体系は、 $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$ ならば健全であり、逆が成り立つならば完全であって、完全性には三つの段階（弱い完全性、有限集合に対する完全性、強い完全性）がある。この課は、完全性を「健全性によって」得ようとする循環論法の正体を暴いた。その論法は $\nvdash \chi$ から $\not\models \chi$ へ移るが、この一歩は実は弱い完全性の対偶である。またこの課は、二つの性質が互いに独立であることを示した。次に、A1、A2、A3 の各代入例が恒真であることを証明した。それを偽にする付値を仮定すると、含意の偽の行によって不可能な値に至るからである。そして健全性を行数についての累積帰納法で証明した。公理の場合、前提の場合、意味論的モーダス・ポネンスの場合があり、二重否定置換の規則については同値 $\theta \eqsem \neg\neg\theta$ と意味論的置換定理を用いる。行から行へと伝わる性質は恒真性ではなく、前提を充足する一つの固定された付値によって充足されることであり、そのため健全性は前提があっても、たとえ前提が無限であっても成り立つ。そこから、充足可能な集合の無矛盾性、特に体系そのものの無矛盾性が導かれ、さらに演繹の単元にはなかった方法、すなわち反例モデルによってある演繹が存在しないことを証明する方法が得られた。

カルマーと有限の完全性

同じ課は逆を二段階で証明した。第一段階はカルマーの補題である。 $\varphi$ の変数がすべて $u_{1}, \ldots, u_{n}$ の中にあるならば $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ であり、これはすべての付値 $v$ について成り立つ。ここで $\psi^{v}$ は $\psi$ （ $v(\psi) = 1$ のとき）または $\neg\psi$ （そうでないとき）である。体系は各行から、その行が論理式について述べることを演繹する。複雑さについての帰納法には複合的な場合が一つしかない。すなわち $(\alpha \downarrow \beta)$ であり、否定論理和が唯一の原始結合子だからである。その場合には三つの部分的な場合があり、体系の二つの補題を必要とする。第二の補題は二つの形をもつ。 $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ は連言導入、二重否定、二重否定置換の規則の二回の適用によって演繹され、 $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ と $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ は選言導入によって演繹される。第二段階は前提を消去する。 $\varphi$ がトートロジーならば、それは $2^{n}$ 個の行のそれぞれの前提から演繹でき、場合分けによる証明が最後の変数のリテラル、次に最後から二番目の変数のリテラル、というように消去していき、 $\vdash \varphi$ に至る。これが弱い完全性である。意味論的演繹定理と統語論的演繹定理の逆によって、完全性は有限個の前提の集合へと拡張される。こうして、有限個の前提については、演繹と帰結が一致し、証明可能な同値と意味論的同値が一致し、導出可能性は真理値表がそれに答えるので決定可能である。

コンパクト性と強い完全性

コンパクト性定理の課は、カルマーの補題が届かない無限の場合を扱った。無限個の前提は一つの含意に移し入れることができないからである。この課は、演繹に一切言及することなく、集合が充足可能であることと、その有限部分集合がすべて充足可能であることとが同値であることを証明した。 $v_{1}, \ldots, v_{n}$ に対する値の列は、集合の各有限部分集合がそれを延長するある付値によって充足されるとき、良い列と呼ばれる。二つの証拠の補題は、良い列が良い列へと延長されることを保証する。どちらの延長も良くないならば、二つの有限の証拠の和集合が、列が良いことと矛盾するからである。そして、可能なときはいつも $1$ を優先して得られる付値は、各論理式を充足する。これは一致補題から従う。各論理式は有限個の変数しかもたないからである。この構成は選択公理を必要としない。変数には番号が付いており、各段階に規則があるからである。コンパクト性からその同値な形、すなわち充足不能性の形と帰結の形が導かれる。後者と有限個の前提に対する完全性と単調性から強い完全性が導かれ、強い完全性と健全性から完全な一致が導かれる。すなわち、 $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ がすべての $\Gamma$ について成り立ち、集合が無矛盾であることと充足可能であることは同値である。この課は、この順序が好みの問題ではないことを注意した。まだ得られていない強い完全性からコンパクト性を導くことは循環になるからである。この課は最後に、可算グラフの彩色を扱った。これは無限の問題を、有限部分が充足可能な論理式の集合に翻訳するものである。また、論理式の集合が表現できるものの限界も扱った。

融合

融合法の課は、論理式の集合を節の集合に置き換えた。節はリテラルの有限集合であり、二つの表現がある。一つは節形式で、同じモデルをもつ。もう一つは定義的な形で、各複合的な部分表記に新しい変数を導入し、充足可能性だけを保ち、二の累乗のようにではなく論理式のように増大する。節の上ではただ一つの規則が働く。 $C$ と $D$ から、 $\ell \in C$ かつ $\ell^{*} \in D$ のとき、 $(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\})$ が得られる。反駁とは $\Box$ に至る生成列である。健全性は、体系の健全性と同じく生成列についての帰納法によって、融合節がその前提の帰結であることを用いて証明され、反駁完全性は変数の個数についての帰納法によって、一つの変数の消去を介して証明される。この消去は充足可能性を保ち、その証明はモデルを構成する。無限集合については、ここでもコンパクト性による。そこから、 $\Gamma \models \varphi$ であることと $\Gamma \cup \{\neg\varphi\}$ のある節形式が反駁をもつこととが同値であることが従う。また飽和は有限である。 $n$ 個の変数では節は $4^{n}$ 個を超えないからである。飽和は真理値表なしに充足可能性を判定する。この課は、最悪の場合のコストが誰にも分かっていない充足可能性問題と、速く判定できる二つの場合、すなわちホーン節と二つのリテラルからなる節を紹介した。

次の図は、四つの区間を一本の鎖にまとめたものである。中央の列の各節点は一つの結果であり、論理的な順序で番号が付けられ、その証明が用いる先行する環と弧で結ばれている。周囲に浮かんでいるのは支え、すなわち鎖が繰り返し頼る原理と道具である。各支えは、それに依拠する環とは実線で、それを確立する環とは破線で結ばれ、先行する単元から来る支えは輪として描かれる。支えをクリックすると、それを用いるすべての環が強調表示される。各環は、それを証明する課へのリンクになっている。健全性とコンパクト性が、一方は第一の区間で、他方は第三の区間で確立され、後続の区間に再び現れること、そして単元で最も多く用いられる支えが付値と一致補題であり、それに次ぐのが帰納法であって、その三つの形、すなわち演繹の行についての、論理式の複雑さについての、節集合の変数の個数についての帰納法として現れることに注目せよ。

鎖の支え

A帰納法と再帰. 自然数についての累積帰納法、論理式の複雑さについての帰納法（その唯一の複合的な場合は $(\alpha \downarrow \beta)$ ）、および再帰的定義。第一単元で証明された。この単元では証明なしに認める。
Bコースの体系. A1、A2、A3、モーダス・ポネンスと二重否定置換の規則。反射性、単調性、演繹どうしのモーダス・ポネンス、有限性、および $\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi)$ 。第二単元で定められた。この単元では証明なしに認める。
C導出された技法. 二重否定は四つの演繹技法の課から。連言導入、選言導入、場合分けによる証明（ $\Gamma \cup \{\psi\} \vdash \chi$ かつ $\Gamma \cup \{\neg\psi\} \vdash \chi$ ならば $\Gamma \vdash \chi$ ）は古典論理の技法の課から。第二単元で証明された。この単元では証明なしに認める。
D付値と一致補題. $v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta))$ 。二つの付値が $V(\varphi)$ の上で一致するならば、それらは $\varphi$ に同じ値を与える。恒真性は $2^{n}$ 個の行で判定される。第三単元で証明された。この単元では証明なしに認める。
E意味論的帰結. 含意の偽の行、単調性、 $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ 、 $\Gamma \models \varphi$ であることと $\Gamma \cup \{\neg\varphi\}$ が充足不能であることの同値、意味論的置換定理。第三単元で証明された。この単元では証明なしに認める。
F連言形式. 値の補題。各論理式は連言標準形と同値であり、それには $2^{n}$ 個の節が必要になりうる。リテラルの選言が恒真であることと相補対を含むこととは同値である。第三単元で証明された。この単元では証明なしに認める。
G健全性. $\Gamma \vdash \varphi$ ならば $\Gamma \models \varphi$ 。これはすべての集合 $\Gamma$ について成り立つ。反例モデルはある演繹が存在しないことを証明する。確立される環: 2. 健全性.
Hコンパクト性. 論理式の集合が充足可能であることと、その有限部分集合がすべて充足可能であることとは同値である。したがって、充足不能な集合は、すでにある有限部分において充足不能である。確立される環: 11. コンパクト性定理.

第 1 区間健全性
- 真理値表を作らずに、図式の各代入例が恒真であることを確かめる。
- 二重否定置換の規則の場合を含めて、行数についての累積帰納法で健全性を証明する。
- 反例モデルによってある論理式が導出可能でないことを証明し、健全性から無矛盾性を導く。
1. 公理の恒真性. A1、A2、A3 の各代入例は恒真である。それを偽にする付値は、含意の偽の行によって不可能な値を要求することになる。
  支え: E (意味論的帰結). 証明される授業: 健全性と完全性.
2. 健全性. $\Gamma \vdash \varphi$ ならば $\Gamma \models \varphi$ 。これはすべての $\Gamma$ について成り立つ。行数についての累積帰納法により、公理の場合、前提の場合、意味論的モーダス・ポネンス、そして二重否定置換の規則には $\theta \eqsem \neg\neg\theta$ と意味論的置換を用いる。
  使う結果: 1. 公理の恒真性. 支え: A (帰納法と再帰), B (コースの体系), E (意味論的帰結). 証明される授業: 健全性と完全性.
3. 無矛盾性と反例モデル. 充足可能な集合はすべて無矛盾である。体系は無矛盾であり、 $\nvdash v_{1}$ である。ある付値が $\Gamma$ を充足し $\varphi$ を偽にするならば、 $\Gamma \nvdash \varphi$ であり、真理値表がそれを証明する。恒真でないものは定理ではない。
  支え: G (健全性), D (付値と一致補題). 証明される授業: 健全性と完全性.
第 2 区間カルマーと有限の完全性
- 否定論理和についての二つの補題を、必要なときは二重否定置換の規則を用いて、体系の中で演繹する。
- カルマーの補題を、複合的な場合を一つだけもつ複雑さについての帰納法で証明する。
- 場合分けによる証明で行の前提を消去し、二つの演繹定理で有限個の前提を取り出す。
- 有限個の前提のもとでの導出可能性、証明可能な同値、無矛盾性を真理値表で判定する。
1. 否定論理和の導入. $\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta)$ かつ $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ 。否定の連言は $\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta)$ である。二重否定が外側の否定を除き、二重否定置換の規則が内側の二つの否定を除く。
  支え: B (コースの体系), C (導出された技法). 証明される授業: 健全性と完全性.
2. 否定論理和の否定. $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ かつ $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ 。 $\neg(\alpha \downarrow \beta)$ は $(\alpha \vee \beta)$ にほかならないので、選言導入で足りる。
  支え: B (コースの体系), C (導出された技法). 証明される授業: 健全性と完全性.
3. カルマーの補題. $V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}$ ならば $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ であり、これはすべての付値 $v$ について成り立つ。帰納法の段階には一つの場合 $(\alpha \downarrow \beta)$ しかなく、 $\alpha$ と $\beta$ の値に応じて三つの部分的な場合に分かれる。
  使う結果: 4. 否定論理和の導入, 5. 否定論理和の否定. 支え: A (帰納法と再帰), D (付値と一致補題), B (コースの体系). 証明される授業: 健全性と完全性.
4. 弱い完全性. $\models \varphi$ ならば $\vdash \varphi$ 。カルマーの補題が各行から $\varphi$ を演繹し、場合分けによる証明が最後の変数から最初の変数へとリテラルを消去する。補題は $2^{n}$ 回、場合分けによる証明は $2^{n} - 1$ 回用いられる。
  使う結果: 6. カルマーの補題. 支え: C (導出された技法). 証明される授業: 健全性と完全性.
5. 有限個の前提に対する完全性. $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$ 。意味論的演繹定理がトートロジーへ導き、弱い完全性がそれを演繹し、演繹定理の逆が前提を元に戻す。
  使う結果: 7. 弱い完全性. 支え: E (意味論的帰結), B (コースの体系). 証明される授業: 健全性と完全性.
6. 有限の一致と判定. 有限の $\Gamma$ について、 $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ であり、 $\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi$ である。したがって、有限個の前提からの導出可能性は真理値表によって決定可能である。
  使う結果: 8. 有限個の前提に対する完全性. 支え: G (健全性), D (付値と一致補題). 証明される授業: 健全性と完全性.
第 3 区間コンパクト性と強い完全性
- 変数の値を一つずつ固定してコンパクト性を証明し、良い列という不変量と二つの証拠の論法を用いる。
- 充足可能性の形、充足不能性の形、帰結の形の間を行き来する。
- 循環に陥らずにコンパクト性から強い完全性を得て、そこから無矛盾性と充足可能性の一致を得る。
- 無限の対象についての問題を論理式の集合として符号化し、コンパクト性によって解く。
1. 二つの証拠の補題. すでに固定された値の列 $s$ が良い（集合の各有限部分集合がそれを延長するある付値によって充足される）ならば、 $(s, 1)$ または $(s, 0)$ は良い。どちらも良くないならば、二つの有限の証拠の和集合が、 $s$ が良いことと矛盾する。
  支え: D (付値と一致補題). 証明される授業: コンパクト性定理.
2. コンパクト性定理. $\Gamma$ が充足可能であることと、その有限部分集合がすべて充足可能であることとは同値である。 $v_{n + 1}$ を $1$ に（ $(s_{n}, 1)$ が良いならば）、そうでなければ $0$ に固定し、得られた付値は一致補題によって各論理式を充足する。変数に番号が付いているので、選択公理は必要ない。
  使う結果: 10. 二つの証拠の補題. 支え: A (帰納法と再帰), D (付値と一致補題). 証明される授業: コンパクト性定理.
3. 同値な形. $\Gamma$ が充足不能であることと、その有限部分のどれかが充足不能であることとは同値である。 $\Gamma \models \varphi$ であることと、 $\Gamma_{0} \models \varphi$ がある有限の $\Gamma_{0} \subseteq \Gamma$ について成り立つこととは同値である。そして後者の形は逆に定理を含意する。
  使う結果: 11. コンパクト性定理. 支え: E (意味論的帰結). 証明される授業: コンパクト性定理.
4. 強い完全性. $\Gamma \models \varphi$ ならば $\Gamma \vdash \varphi$ 。これはすべての $\Gamma$ について成り立つ。帰結の形が有限の $\Gamma_{0}$ を与え、有限個の前提に対する完全性が $\Gamma_{0} \vdash \varphi$ を与え、単調性が $\Gamma \vdash \varphi$ を与える。
  使う結果: 8. 有限個の前提に対する完全性, 12. 同値な形. 支え: B (コースの体系). 証明される授業: コンパクト性定理.
5. 演繹は帰結である. $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ がすべての $\Gamma$ について成り立つ。定理はちょうどトートロジーであり、集合が無矛盾であることと充足可能であることとは同値である。
  使う結果: 13. 強い完全性. 支え: G (健全性). 証明される授業: コンパクト性定理.
6. 可算グラフの彩色. 各頂点と各色に対して変数 $x_{i,c}$ をとり、各頂点がちょうど一つの色をもち、隣接する頂点は異なる色をもつことを表す論理式をとれば、可算グラフは、その有限部分グラフがすべて $k$ 色で彩色可能ならば、それ自身も彩色可能である。
  支え: H (コンパクト性), F (連言形式). 証明される授業: コンパクト性定理.
第 4 区間融合
- 論理式の集合を、連言形式または定義的な形によって節の集合として表す。
- 一つの段階で二つの相補対を消去することなく反駁を作る。
- 融合の健全性と反駁完全性を、まず有限集合について、次にコンパクト性によって任意の集合について証明する。
- 飽和によって帰結を判定し、速く判定できる場合を見分ける。
1. 節形式. 節はリテラルの有限集合であり、あるリテラルが値 $1$ をとるときに充足され、 $\Box$ は充足不能である。 $\Gamma$ の節形式は同じモデルをもち、 $\Gamma \models \varphi$ であることと $\Gamma \cup \{\neg\varphi\}$ の節形式が充足不能であることとは同値である。
  支え: F (連言形式), E (意味論的帰結). 証明される授業: 融合法.
2. 定義的節形式. 各部分表記に新しい変数とその定義節をとれば、 $T(\varphi)$ と $\varphi$ は充足同値であり、節は高々 $4k + 1$ 個で、各節のリテラルは高々三つである。定義的な形は有限個の前提のもとでの帰結を判定する。
  使う結果: 16. 節形式. 支え: A (帰納法と再帰), D (付値と一致補題). 証明される授業: 融合法.
3. 融合の健全性. $\{C, D\} \models R_{\ell}(C, D)$ は $\ell$ の値による場合分けで示される。生成列についての累積帰納法により、 $S \models C$ は、節 $C$ が $S$ から生成されるときは常に成り立つ。 $S$ が反駁をもつならば、それは充足不能である。
  使う結果: 16. 節形式. 支え: A (帰納法と再帰). 証明される授業: 融合法.
4. 一つの変数の消去. $E_{p}(S)$ は $p$ も $\neg p$ も含まない節を残し、 $p$ についての融合節を加える。それは $p$ を含まず、 $S$ と充足同値である。そのモデルから $S$ のモデルが得られる。 $p$ の値を選べばよい。
  使う結果: 18. 融合の健全性. 支え: D (付値と一致補題). 証明される授業: 融合法.
5. 有限の反駁完全性. 有限で充足不能な節の集合はすべて反駁をもつ。変数の個数についての帰納法による。最後の変数を消去し、各融合節の前提を挿入する。
  使う結果: 19. 一つの変数の消去. 支え: A (帰納法と再帰). 証明される授業: 融合法.
6. 反駁完全性. 節の集合は、有限であれ無限であれ、充足不能であることと反駁をもつこととが同値である。したがって、 $\Gamma \models \varphi$ であることと $\Gamma \cup \{\neg\varphi\}$ の節形式が反駁をもつこととは同値である。
  使う結果: 16. 節形式, 18. 融合の健全性, 20. 有限の反駁完全性. 支え: H (コンパクト性). 証明される授業: 融合法.
7. 飽和は判定する. $n$ 個の変数では、生成される節の集合は高々 $4^{n}$ 個の要素をもつ。飽和は停止し、真理値表なしに充足可能性を判定するが、常に真理値表より速いわけではない。
  使う結果: 18. 融合の健全性, 20. 有限の反駁完全性. 証明される授業: 融合法.

コースの到達点. 鎖は、コースの二つの側面が同一の関係として認識され、それを判定する方法が得られたところで終わる。残された未解決の問題は、もはや命題論理についての問題ではなく、そのコストと量化子への拡張についての問題である。