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

意味論：まとめと挑戦課題

要約

この課で意味論の単元を締めくくる。この課は、付値のすべての論理式への拡張と一致補題から出発して、意味論的帰結、同値、そして同値の二つの作業定理（置換定理と一様代入定理）へ、そこから任意個の項についての法則、関数的完全性、結合子の集合へ、さらにそこから標準形、その算法、回路へと至る演繹の鎖を再構成し、各環でどの結果を用い、どの課で証明されるかを示す。単元が証明したことと前の単元から受け取ったことを区別し、コースが第1単元から持ち越してきた論証を三通りの方法で判定し、単元が未解決のまま残す問い、すなわちすべての付値で真であるものが導出可能なものと一致するかという問いがなぜメタ理論へ通じるのかを説明する。まとめテストでは導入テストの技能を繰り返し、最後に六つの挑戦課題で終わる。挑戦課題は各課の演習より難しく、複数の課の道具を組み合わせることを求める。

学習目標

  1. 単元の結果の論理的な順序を再構成し、各結果が依拠する先行の結果と、それが証明される課を示すこと。
  2. 再帰的な拡張、一致補題、意味論的置換、一般化された法則が、関数的完全性、標準形の存在、およびその算法の正しさと停止性へどのように通じるかを説明すること。
  3. 単元が証明したことを、前の単元から受け取ったこと、およびメタ理論に残したこと、とりわけ意味論的帰結と導出可能性の一致およびコンパクト性から区別すること。
  4. 値の計算、意味論的帰結、一様代入、結合子の集合、標準形、回路を組み合わせる問題を解くこと。

単元で達成したこと

この単元の目的は、第1単元で構成した言語の論理式に、第2単元の演繹体系には手を触れずに意味を与え、その意味から、論理学が論理式について立てる問い、すなわち論理式が恒真かどうか、充足可能かどうか、他の論理式から帰結するかどうか、別の論理式と同じことを言うかどうかを判定する手続きを引き出すことであった。この目的は少数の前提のもとで達成され、前提はそれぞれその場所で明示された。二値性と真理関数性は証明されるのではなく選ばれるものであり、その代価は形式化の課が示した。一意読み取り可能性、再帰による定義、帰納法、公式の略記は第1単元で証明または確定され、ここで用いられる。そして集合と関数についての必要最小限の事柄は、必要なところで確認された。これらの前提のもとで、たどってきた道のりは、課ごとに一つずつ、六つの区間からなる一本の演繹の鎖として読むことができる。

論理式の値

命題論理の意味論についての課は、付値を変数から {0,1}\{0, 1\} への関数として定義し、論理式上の再帰による定義の定理によって、付値がただ一つの条項 v((φ↓ψ))=(1−v(φ))(1−v(ψ))v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi)) によってすべての論理式へ一意に拡張されることを証明した。公式の略記から、ほかに何も要請せずに、各派生結合子の値を成分の値の多項式として計算し、それとともに含意の表を得た。含意の表はここでは定理である。複雑さに関する帰納法によって一致補題を証明し、そこから、2n2^{n} 行の真理値表が、nn 個の変数をもつ論理式について無限に多くの付値が語ることをすべて含むことが従う。充足、恒真性、充足可能性、矛盾式、偶然式を定義し、⊭φ\not\models \varphi は φ\varphi が恒真でないことを言うのであって矛盾式であることを言うのではないと明確にし、⊤:=(v1→v1)\top := (v_{1} \rightarrow v_{1}) と ⊥:=¬⊤\bot := \neg\top を定め、恒真性と充足可能性の決定可能性を指数的な代価で得た。この代価は、反駁する付値を狙いを定めて探すことで減らせるが、なくすことはできない。

帰結と同値

意味論的帰結と同値についての課は、有限または無限の前提集合からの帰結を定義し、それが演繹の構造的性質（反射性、単調性、カット、推移性）をもつことを証明した。その証明は行を操作するのではなく付値を調べ尽くす。意味論的演繹定理 Γ∪{φ}⊨ψ⇔Γ⊨(φ→ψ)\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi) は含意のただ一つの偽の行に帰着し、帰結は充足不能性に帰着した。すなわち Γ⊨φ⇔Γ∪{¬φ}\Gamma \models \varphi \Leftrightarrow \Gamma \cup \{\neg\varphi\} が充足不能である。値の等しさとして定義された意味論的同値は、相互の帰結とも、双条件の恒真性とも一致することがわかった。その二つの作業定理は複雑さに関する帰納法で証明された。一つは部分論理式の一つの出現をそれと同値な論理式で置き換える置換であり、省いてはならない全体の出現の場合を含む。もう一つは変数に任意の論理式を一様に代入する一様代入であり、恒真性、同値、帰結を保存する。これらによって、多項式の恒等式として確かめられた法則のカタログは、任意の論理式の任意の箇所に適用でき、連鎖させることができる。

任意個の項についての法則

一般化されたド・モルガンの法則と分配法則についての課は、nn 個の論理式の連言と選言を左結合で再帰的に定義し、項の個数に関する帰納法によって値の補題を証明した。値の補題は、連言が真であるのはそのすべての項が真であるとき、かつそのときに限り、選言が真であるのはある項が真であるとき、かつそのときに限ることを述べる。これと、結合子の同値との両立性とによって、一般化された結合律を得た。これは証明可能な同値についても成り立つように同値の連鎖で証明された。さらに、順序と繰り返しからの独立性、一般化されたド・モルガンの法則、一般化された分配法則を得た。分配法則の二つの添字に関する帰納法は、帰納法の仮定が第二のリストのすべての長さを覆うように組み立てられた。双対の法則は、二重の帰納法を繰り返すことなく、ド・モルガンの法則によって得られた。

真理関数

関数的完全性についての課は、表から論理式へという逆の道をたどった。nn 個の引数をもつ真理関数を数え（22n2^{2^{n}} 個ある）、各論理式がそのうちちょうど一つを表すこと、二つの論理式が同値であるのは同じ関数を表すとき、かつそのときに限ることを示し、関数的完全性の定理を証明した。行の連言はちょうどその行で真であり、関数が 11 をとる行の連言の選言がその関数を表す。この論理式は円と円盤の記号列であるから、否定論理和だけで十分である。否定論理和の判定基準により、{¬,∧}\{\neg, \wedge\}、{¬,∨}\{\neg, \vee\}、{¬,→}\{\neg, \rightarrow\}、および否定論理積も十分である。そして閉包原理により、{∧,∨,→,↔}\{\wedge, \vee, \rightarrow, \leftrightarrow\} の論理式はすべて 11 を保存するので、この集合は十分ではない。

標準形

標準形についての課は、同値な論理式の各類から決まった形の代表を選んだ。リテラル、節、基本連言を定義し、標準形の否定がその双対と同値であることを証明した。双対は、各連言を選言に、各リテラルを反対のリテラルに取り替える。表から主標準形を構成し、それは変数を固定すれば一意である。そして二つの標準形の存在を二通りに証明した。一つは表からであり、関数的完全性の系としてである。もう一つは複雑さに関する帰納法によるものであり、ただ一つの場合は否定論理和で、それは成分の否定の連言と同値である。帰納法の仮定は二つの形を同時に要求する。否定がそれらを入れ替えるからである。最後に、連言標準形の恒真性と選言標準形の充足可能性が、その相補対を見れば一目でわかることを示した。

算法と回路

標準形のアルゴリズムとその応用についての課は、二番目の存在証明を、表記に作用する手続きに変えた。¬\neg、∧\wedge、∨\vee 以外の結合子を消去し、否定を変数まで押し下げ、分配する。表記における置換によってアルゴリズムの正しさを証明した。この置換は置換定理を略記に合わせたものである。また、各段階で減少する三つの測度によって停止性を証明した。その最後のものは連言を積として読む。さらに、⋁i=1n(pi∧qi)\bigvee_{i=1}^{n} (p_i \wedge q_i) の連言標準形は必然的に 2n2^{n} 個の節をもつことを証明したので、増大はアルゴリズムの欠陥ではない。続いて、ブラックボックスの標準形をその表から求め、隣接する行を併合して簡単にし、スイッチ回路に変えた。回路の導通はその論理式の値である。

次の図は、六つの区間を一本の鎖にまとめたものである。列の各節点は定義か結果で、論理的な順序で番号が付き、その証明が用いる前の環と弧で結ばれている。そのまわりに浮かぶのが支え、すなわち鎖が何度も立ち返る原理と道具であり、それぞれはよりかかる環と実線で、確立される環と点線で結ばれる。ただし、この鎖が証明しないもの（再帰とあわせた一意読み取り可能性、帰納法、公式の略記で、いずれも第1単元のもの）は輪として描かれる。支えを押すと、それを使うすべての環が強調され、各環はそれが証明される課へのリンクになっている。帰納法と結合子の値が単元で最もよく使われる支えであること、そして値の補題は第3課で証明されるものの、最後の三つの課が連言と選言について述べることのほとんどすべてを支えていることに注意しよう。

鎖の支え

  • A一意読み取り可能性と再帰. ∙φψ=∙φ′ψ′\sigI\varphi\psi = \sigI\varphi'\psi' であり、四つの記号列がすべて論理式であるならば、φ=φ′\varphi = \varphi' かつ ψ=ψ′\psi = \psi' である。したがって、∙φψ\sigI\varphi\psi の値を φ\varphi、ψ\psi とそれらの値から計算する規則は、論理式上のただ一つの関数を定義する。第1単元で証明される。 この単元では証明なしに認める。
  • B帰納法. 自然数に関する単純な帰納法と累積帰納法、および論理式の複雑さに関する帰納法。後者の場合は変数と否定論理和 (φ↓ψ)(\varphi \downarrow \psi) だけである。第1単元で証明される。 この単元では証明なしに認める。
  • C公式の略記. ¬φ:=(φ↓φ)\neg\varphi := (\varphi \downarrow \varphi)、(φ∨ψ):=¬(φ↓ψ)(\varphi \vee \psi) := \neg(\varphi \downarrow \psi)、(φ∧ψ):=¬(¬φ∨¬ψ)(\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)、(φ→ψ):=(¬φ∨ψ)(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi)、(φ↔ψ):=((φ→ψ)∧(ψ→φ))(\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi))、(φ⊻ψ):=¬(φ↔ψ)(\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)。第1単元で定められる。 この単元では証明なしに認める。
  • D結合子の値. a=v(φ)a = v(\varphi)、b=v(ψ)b = v(\psi) のとき：v(¬φ)=1−av(\neg\varphi) = 1 - a、v((φ∨ψ))=a+b−abv((\varphi \vee \psi)) = a + b - ab、v((φ∧ψ))=abv((\varphi \wedge \psi)) = ab、v((φ→ψ))=1−a(1−b)v((\varphi \rightarrow \psi)) = 1 - a(1 - b)、v((φ↔ψ))=ab+(1−a)(1−b)v((\varphi \leftrightarrow \psi)) = ab + (1 - a)(1 - b)、v((φ⊻ψ))=a+b−2abv((\varphi \veebar \psi)) = a + b - 2ab。ただし a2=aa^{2} = a。 確立される環: 1. 付値の拡張.
  • E一致補題. 二つの付値が φ\varphi の変数で一致すれば、それらは φ\varphi に同じ値を与える。だから 2n2^{n} 行の表がすべてを語る。 確立される環: 2. 一致補題と表.
  • F意味論的置換. θ≡θ′\theta \eqsem \theta' であり、χ′\chi' が χ\chi における θ\theta の一つの出現を θ′\theta' で置き換えて得られるならば、χ≡χ′\chi \eqsem \chi' である。 確立される環: 7. 意味論的置換定理.
  • G同値の法則. 任意の論理式についての二重否定、べき等律、交換律、結合律、分配律、ド・モルガンの法則、吸収律、恒等律、支配律、排中律、無矛盾律。 確立される環: 9. 同値の法則.
  • H値の補題. v(⋀i=1nφi)=1v\left( \bigwedge_{i=1}^{n} \varphi_i \right) = 1 であるのは v(φi)=1v(\varphi_i) = 1 がすべての ii について成り立つとき、かつそのときに限る。v(⋁i=1nφi)=1v\left( \bigvee_{i=1}^{n} \varphi_i \right) = 1 であるのは v(φi)=1v(\varphi_i) = 1 がある ii について成り立つとき、かつそのときに限る。 確立される環: 10. 値の補題と両立性.

  1. 第 1 区間 論理式の値

    • 否定論理和の条項によって論理式の値を計算し、略記から各派生結合子の値を導くこと。
    • 一致補題を証明し、それによって 2n2^{n} 行の表で十分であることを正当化すること。
    • ⊭φ\not\models \varphi を矛盾式と混同せずに論理式と集合を分類し、反駁する付値を探して恒真性を判定すること。

    1. 付値の拡張. 各付値 vv は条項 v((φ↓ψ))=(1−v(φ))(1−v(ψ))v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi)) によってすべての論理式へ一意に拡張される。略記を展開すると、¬\neg、∨\vee、∧\wedge、→\rightarrow、↔\leftrightarrow、⊻\veebar の値が計算される。

      支え: A (一意読み取り可能性と再帰), C (公式の略記). 証明される授業: 命題論理の意味論.

    2. 一致補題と表. vv と v′v' が V(φ)V(\varphi) で一致すれば v(φ)=v′(φ)v(\varphi) = v'(\varphi) である。これは複雑さに関する帰納法による。したがって、すべての付値における φ\varphi の値は、その表の 2n2^{n} 行における値にほかならない。

      使う結果: 1. 付値の拡張. 支え: B (帰納法). 証明される授業: 命題論理の意味論.

    3. 分類と判定. 各論理式は、恒真、偶然式、矛盾式のちょうど一つである。φ\varphi が恒真であるのは ¬φ\neg\varphi が矛盾式であるとき、かつそのときに限り、矛盾式であるのは ⊨¬φ\models \neg\varphi のとき、かつそのときに限る。⊤\top と排中律は恒真、⊥\bot は矛盾式であり、恒真性と充足可能性は行を調べ尽くすことで判定される。

      支え: D (結合子の値), E (一致補題). 証明される授業: 命題論理の意味論.

  2. 第 2 区間 帰結と同値

    • 有限または無限の集合からの帰結を、反例モデルを示すか、それが存在しないことを証明して判定すること。
    • 意味論的演繹定理と、帰結の充足不能性への帰着を適用すること。
    • 一つの出現の置換と一様代入を区別し、どちらも複雑さに関する帰納法で証明すること。
    • 各法則を正しく名指しながら、同値を連鎖によって確立すること。

    1. 帰結とその性質. Γ⊨φ\Gamma \models \varphi とは、Γ\Gamma を充足するすべての付値が φ\varphi を充足することである。∅⊨φ\emptyset \models \varphi であるのは ⊨φ\models \varphi のとき、かつそのときに限る。反射性、単調性、カット、推移性が成り立ち、充足不能な集合はあらゆる論理式を帰結としてもつ。

      使う結果: 3. 分類と判定. 証明される授業: 意味論的帰結と同値.

    2. 意味論的演繹と充足不能性. Γ∪{φ}⊨ψ⇔Γ⊨(φ→ψ)\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi) は含意のただ一つの偽の行による。{φ1,…,φn}⊨ψ⇔  ⊨(φ1→(φ2→⋯(φn→ψ)⋯ ))\{\varphi_1, \ldots, \varphi_n\} \models \psi \Leftrightarrow\; \models (\varphi_1 \rightarrow (\varphi_2 \rightarrow \cdots (\varphi_n \rightarrow \psi) \cdots)) である。そして Γ⊨φ\Gamma \models \varphi であるのは Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} が充足不能であるとき、かつそのときに限る。

      使う結果: 4. 帰結とその性質. 支え: D (結合子の値). 証明される授業: 意味論的帰結と同値.

    3. 意味論的同値. φ≡ψ\varphi \eqsem \psi であるのは φ⊨ψ\varphi \models \psi かつ ψ⊨φ\psi \models \varphi であるとき、かつそのときに限り、また ⊨(φ↔ψ)\models (\varphi \leftrightarrow \psi) であるとき、かつそのときに限る。同値は反射的、対称的、推移的であり、同値な二つの論理式は前提としても結論としても取り替えがきく。

      使う結果: 4. 帰結とその性質. 支え: D (結合子の値). 証明される授業: 意味論的帰結と同値.

    4. 意味論的置換定理. θ≡θ′\theta \eqsem \theta' ならば、χ\chi において θ\theta の一つの出現（全体の出現を含む）を θ′\theta' で置き換えると、χ\chi と同値な論理式が得られる。すべての出現を同時に置き換えても同じである。

      使う結果: 1. 付値の拡張, 6. 意味論的同値. 支え: A (一意読み取り可能性と再帰), B (帰納法). 証明される授業: 意味論的帰結と同値.

    5. 一様代入. w(vn)=v(σ(vn))w(v_n) = v(\sigma(v_n)) ならば v(σ(χ))=w(χ)v(\sigma(\chi)) = w(\chi) である。したがって ⊨χ\models \chi ならば ⊨σ(χ)\models \sigma(\chi) でもあり、代入は同値と帰結を保存するが、充足可能性も偶然式であることも保存しない。

      使う結果: 1. 付値の拡張, 4. 帰結とその性質, 6. 意味論的同値. 支え: A (一意読み取り可能性と再帰), B (帰納法). 証明される授業: 意味論的帰結と同値.

    6. 同値の法則. カタログの法則は a2=aa^{2} = a のもとで多項式の恒等式として確かめられる。置換と推移性によって、それらは部分論理式に適用され、連鎖させられる。

      使う結果: 3. 分類と判定, 6. 意味論的同値. 支え: D (結合子の値), F (意味論的置換). 証明される授業: 意味論的帰結と同値.

  3. 第 3 区間 任意個の項についての法則

    • nn 個の項の連言と選言を左結合の記号列として展開し、その値を計算すること。
    • 項の個数に関する帰納法によって、一般化された結合律、順序からの独立性、一般化されたド・モルガンの法則を証明すること。
    • 一般化された分配法則を二つの添字に関する帰納法で証明し、それが生む項を数えること。

    1. 値の補題と両立性. α≡α′\alpha \eqsem \alpha' かつ β≡β′\beta \eqsem \beta' ならば、¬α≡¬α′\neg\alpha \eqsem \neg\alpha'、(α∧β)≡(α′∧β′)(\alpha \wedge \beta) \eqsem (\alpha' \wedge \beta')、(α∨β)≡(α′∨β′)(\alpha \vee \beta) \eqsem (\alpha' \vee \beta') である。nn 個の項の連言が 11 をとるのはすべての項が 11 をとるとき、かつそのときに限り、選言はある項が 11 をとるとき、かつそのときに限る。同値な項は同値な連言と選言を与える。

      使う結果: 6. 意味論的同値. 支え: D (結合子の値), B (帰納法). 証明される授業: 一般化されたド・モルガンの法則と分配法則.

    2. 結合律と順序. 二つのリストの連言どうしの連言は、それらを連結したリストの連言と同値であり、どのまとめ方も左結合のものと同値である。同じ項をもつ二つのリストは、順序や繰り返しにかかわらず、同値な連言と選言を与える。

      支え: H (値の補題), G (同値の法則), B (帰納法). 証明される授業: 一般化されたド・モルガンの法則と分配法則.

    3. 一般化されたド・モルガンの法則. ¬⋀i=1nφi≡⋁i=1n¬φi\neg \bigwedge_{i=1}^{n} \varphi_i \eqsem \bigvee_{i=1}^{n} \neg\varphi_i かつ ¬⋁i=1nφi≡⋀i=1n¬φi\neg \bigvee_{i=1}^{n} \varphi_i \eqsem \bigwedge_{i=1}^{n} \neg\varphi_i。二項の法則を最後の結合に適用し、帰納法の仮定を内側に残るものに適用する。

      支え: H (値の補題), G (同値の法則), B (帰納法). 証明される授業: 一般化されたド・モルガンの法則と分配法則.

    4. 一般化された分配法則. (⋁i=1nφi)∧(⋁j=1mψj)≡⋁i,j(φi∧ψj)\left( \bigvee_{i=1}^{n} \varphi_i \right) \wedge \left( \bigvee_{j=1}^{m} \psi_j \right) \eqsem \bigvee_{i,j} (\varphi_i \wedge \psi_j)。ここで項は nmnm 個あり、辞書式順序に並ぶ。また、二つの連言の選言を分配する双対の法則は、ド・モルガンの法則による。

      使う結果: 11. 結合律と順序, 12. 一般化されたド・モルガンの法則. 支え: H (値の補題), G (同値の法則), B (帰納法). 証明される授業: 一般化されたド・モルガンの法則と分配法則.

  4. 第 4 区間 真理関数

    • 真理関数を数え、二つの論理式が表す関数を比べて同値を判定すること。
    • 表の論理式を構成し、任意の関数を否定論理和だけで書くこと。
    • 結合子の集合が十分であることを否定論理和の判定基準で、あるいは十分でないことをその論理式が保存する性質で証明すること。

    1. 真理関数. 22n2^{2^{n}} 個の真理関数があり、引数は nn 個である。変数が v1,…,vnv_1, \ldots, v_n の中にある論理式は、そのうちちょうど一つ fφf_\varphi を表し、φ≡ψ⇔fφ=fψ\varphi \eqsem \psi \Leftrightarrow f_\varphi = f_\psi である。

      使う結果: 6. 意味論的同値. 支え: E (一致補題). 証明される授業: 関数的完全性.

    2. 関数的完全性. 行の連言はちょうどその行で 11 をとる。ff が 11 をとる行の連言の選言は（そのような行がなければ (v1∧¬v1)(v_{1} \wedge \neg v_{1}) は）ff を表す。そしてすべての論理式はその表の論理式と同値である。

      使う結果: 14. 真理関数. 支え: H (値の補題), D (結合子の値). 証明される授業: 関数的完全性.

    3. 十分な集合と十分でない集合. 否定論理和は、略記が展開されるので十分である。KK の論理式が (1−a)(1−b)(1 - a)(1 - b) の値を表せば、集合 KK は十分であり、{¬,∧}\{\neg, \wedge\}、{¬,∨}\{\neg, \vee\}、{¬,→}\{\neg, \rightarrow\}、{↑}\{\uparrow\} もそうである。{∧,∨,→,↔}\{\wedge, \vee, \rightarrow, \leftrightarrow\} の論理式は 11 をとる。すべての変数が 11 をとるときはつねにそうである。したがってこの集合は十分ではない。

      使う結果: 15. 関数的完全性. 支え: C (公式の略記), B (帰納法), D (結合子の値). 証明される授業: 関数的完全性.

  5. 第 5 区間 標準形

    • リテラル、節、標準形を見分け、記号列の形をその値から区別すること。
    • 表から主標準形を構成し、その一意性を証明すること。
    • 両方を要求する帰納法の仮定によって、標準形の存在を帰納法で証明すること。
    • 連言標準形の恒真性と選言標準形の充足可能性を一目で判定すること。

    1. リテラルと双対性. ¬ℓ≡ℓ∗\neg\ell \eqsem \ell^{*}。基本連言が充足可能であるのは相補対を含まないとき、かつそのときに限り、節が恒真であるのは相補対を含むとき、かつそのときに限る。標準形の否定はその双対と同値であり、したがって φ\varphi の連言標準形は ¬φ\neg\varphi の選言標準形の双対である。

      使う結果: 12. 一般化されたド・モルガンの法則. 支え: G (同値の法則), F (意味論的置換), H (値の補題). 証明される授業: 標準形.

    2. 主標準形. φ\varphi が充足可能ならば、その主選言標準形と同値であり、恒真でなければ、その主連言標準形と同値である。変数 v1,…,vnv_1, \ldots, v_n を固定すれば、二つの主標準形が同値であるのは同じ記号列であるとき、かつそのときに限り、充足可能な二つの論理式が同値であるのは同じ主選言標準形をもつとき、かつそのときに限る。

      使う結果: 15. 関数的完全性, 17. リテラルと双対性. 支え: H (値の補題), E (一致補題). 証明される授業: 標準形.

    3. 帰納法による存在. (φ↓ψ)≡(¬φ∧¬ψ)(\varphi \downarrow \psi) \eqsem (\neg\varphi \wedge \neg\psi)。標準形は連言と選言について閉じている。連言の選言標準形と選言の連言標準形は一般化された分配法則による。両方の形についての帰納法の仮定をおいた帰納法によって、すべての論理式は選言標準形と連言標準形をもつ。

      使う結果: 17. リテラルと双対性, 11. 結合律と順序, 13. 一般化された分配法則. 支え: B (帰納法), F (意味論的置換). 証明される授業: 標準形.

    4. 一目でわかること. 連言標準形が恒真であるのは、そのどの節も相補対を含むとき、かつそのときに限る。選言標準形が充足可能であるのは、相補対を一つも含まない基本連言があるとき、かつそのときに限る。

      使う結果: 17. リテラルと双対性. 支え: H (値の補題). 証明される授業: 標準形.

  6. 第 6 区間 算法と回路

    • 書き換えのアルゴリズムを適用し、双条件の消去の適切な仕方を選ぶこと。
    • その正しさと停止性を証明し、連言標準形が指数的に増大しうる理由を説明すること。
    • ブラックボックスの標準形を求めて簡単にし、それらからスイッチ回路を構成すること。

    1. アルゴリズムの正しさと停止性. 部分表記を同値なもので置き換えると同値な表記が得られる。各規則は同値であり、既約な表記はあるまとめ方の標準形である。測度 M1M_1、M2M_2（M2(¬φ)=2M2(φ)M_2(\neg\varphi) = 2^{M_2(\varphi)} として）、M3M_3（M3(φ∧ψ)=M3(φ) M3(ψ)M_3(\varphi \wedge \psi) = M_3(\varphi)\,M_3(\psi) として）は各段階で減少する。

      使う結果: 19. 帰納法による存在, 11. 結合律と順序. 支え: G (同値の法則), D (結合子の値), B (帰納法). 証明される授業: 標準形のアルゴリズムとその応用.

    2. 指数的な増大. ⋁i=1n(pi∧qi)\bigvee_{i=1}^{n} (p_i \wedge q_i) は 2n2^{n} 個の節からなる連言標準形と同値であり、それと同値な連言標準形はどれも、恒真でない節を少なくとも 2n2^{n} 個もつ。

      使う結果: 19. 帰納法による存在, 17. リテラルと双対性. 支え: H (値の補題). 証明される授業: 標準形のアルゴリズムとその応用.

    3. 隣接する行と回路. (κ∧ℓ)∨(κ∧ℓ∗)≡κ(\kappa \wedge \ell) \vee (\kappa \wedge \ell^{*}) \eqsem \kappa と双対の同値。直並列回路が状態 vv で導通するのは v(φC)=1v(\varphi_C) = 1 のとき、かつそのときに限り、すべての真理関数はある回路によって実現される。

      使う結果: 15. 関数的完全性, 18. 主標準形, 17. リテラルと双対性, 11. 結合律と順序. 支え: G (同値の法則), F (意味論的置換), D (結合子の値), B (帰納法). 証明される授業: 標準形のアルゴリズムとその応用.

メタ理論へ. 鎖は、意味論が論理式についての各問いに対して手続きをもつところで止まる。残るのは、すべての付値で真であるものが、体系で導出されるものとちょうど一致するかどうかを知ることである。次の単元が二つの概念を比較する。