跳至内容
Topos Uranos
中文 (中国)

语义学：总结与挑战

摘要

本课结束语义单元。它重建一条演绎链：从赋值向全体公式的扩张和一致引理出发，通向语义后承、语义等价及其两条工作定理（替换定理和统一代入定理）；再由此通向任意多项的定律、功能完全性和联结词集；再由此通向范式、范式算法和电路；并在每个环节指出它用到哪些结果、在哪一课中证明。本课把本单元证明的东西与它从前面单元取来的东西区分开，用三种方法判定课程自第一单元以来一直带着的那个论证，并说明为什么本单元留下的开放问题，即在每个赋值下为真的东西是否与可推演的东西一致，会通向元理论。结业测评重复入门测评的各项技能；最后是六道挑战题，比各课的习题更难，要求把不止一课的工具结合起来。

学习目标

  1. 重建本单元结果的逻辑顺序，指出每个结果所依赖的前面的结果以及证明它的那一课。
  2. 说明递归扩张、一致引理、语义替换和推广的定律如何通向功能完全性、范式的存在性以及范式算法的正确性和终止性。
  3. 把本单元证明的东西、它从前面单元取来的东西以及它留给元理论的东西区分开，特别是语义后承与可推演性的一致以及紧致性。
  4. 解决把求值、语义后承、统一代入、联结词集、范式和电路结合起来的问题。

本单元的收获

本单元的目标是给第一单元所构造的语言中的公式赋予意义，而不触动第二单元的演绎系统，并从这种意义中得出判定逻辑就公式所提出的问题的程序：一个公式是否有效，是否可满足，是否从别的公式得出，是否与另一个公式说的是同一回事。这一目标已经达到，只附带少数前提，每一个都在其位置上声明过：二值性和真值函数性，它们不是被证明而是被选择的，形式化一课展示了它们的代价；唯一可读性、递归定义、归纳法和正式缩写，它们在第一单元中已被证明或确定，在这里被使用；以及关于集合与函数的必要的最低限度，在需要的地方作了提示。有了这些前提，所走过的路可以读作一条由六段组成的演绎链，每课一段。

公式的值

关于命题逻辑的语义学的一课把赋值定义为从变元到 {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} 个子句，因此增长并不是算法的缺陷。接着，它从黑箱的真值表得到黑箱的范式，通过合并相邻的行加以化简，再把它们变成开关电路，其导通情况就是其公式的值。

下图把六段汇成一条链。中间一列的每个节点是一个定义或一个结果，按逻辑顺序编号，并用弧线连到其证明所用到的前面的环节；四周浮动的是支柱，即这条链一再求助的原理和工具，每个支柱用实线连到依靠它的环节，用虚线连到确立它的环节，而这条链没有证明的支柱（唯一可读性连同递归、归纳法和正式缩写，均来自第一单元）则画成圆环。点击一个支柱，会突出显示所有用到它的环节；每个环节都链接到证明它的那一课。请注意，归纳法和联结词的值是本单元最常用到的支柱，而值引理虽然在第三课中证明，却支撑着后三课关于合取和析取所说的几乎一切。

链的支柱

  • A唯一可读性与递归. 若 ∙φψ=∙φ′ψ′\sigI\varphi\psi = \sigI\varphi'\psi'，且四个符号串都是公式，则 φ=φ′\varphi = \varphi' 且 ψ=ψ′\psi = \psi'；因此，一条由 ∙φψ\sigI\varphi\psi、φ\varphi 及其值计算 ψ\psi 的值的规则，在公式上定义了唯一的函数。在第一单元中证明。 本单元中不加证明而采用。
  • B归纳法. 对自然数的简单归纳和强归纳，以及对公式复杂度的归纳，其仅有的情形是变元和或非 (φ↓ψ)(\varphi \downarrow \psi)。在第一单元中证明。 本单元中不加证明而采用。
  • 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)。在第一单元中确定。 本单元中不加证明而采用。
  • 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 (归纳法). 证明于: 范式算法及其应用.

通向元理论. 这条链停在语义对关于公式的每个问题都有一个程序的地方。剩下要弄清的是：在每个赋值下为真的东西，是否恰好就是在系统中可推演的东西。下一单元将比较这两个概念。