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

演绎：总结与挑战

摘要

本课结束专讲演绎的单元。它重建一条演绎之链：从卢卡西维茨系统的定义（三个公理模式和分离规则）出发，到演绎定理以及该系统在或非语言中的界限；由此到四种基本技巧，以及完成本课程系统的双重否定替换规则；从或非的基本引理到等价替换和各种对称性，再由此到经典逻辑的规则以及德摩根律与分配律；并在每一环指出它用到哪些结果、在哪一课中证明。它区分本单元证明了的东西与它接受下来的东西，把已取得的成果放回课程计划中衡量，并解释为什么本单元留下的问题，即可推演的东西是否与真的东西相一致，会通向语义单元。它在结业测评中重复入门测评的各项技能，最后给出六道挑战题，难度高于各课的习题，要求综合运用其中几课的工具。

学习目标

  1. 重建本单元各结果的逻辑顺序，指出每个结果所依据的先前结果以及证明它的那一课。
  2. 解释演绎定理、双重否定、双重否定替换规则、逆否律、基本引理与等价替换如何环环相扣，以及为什么经典规则和德摩根律与分配律都依赖于它们。
  3. 区分本单元证明了的东西、它接受下来的东西（公理模式、两条初始规则、强归纳法、结构归纳法和唯一可读性）以及它留给后续单元的东西，特别是推演与真之间的关系。
  4. 解答综合运用标记、双重否定替换规则、演绎定理、分情况证明、归谬法、等价替换以及德摩根律与分配律的问题。

本单元的收获

本单元的目标是为上一单元的语言配备一个演绎系统，即一种纯语法的、由一些公式得到另一些公式的方式，并用这个系统逐行证明数学据以推理的各种技巧。这一目标已经实现，只有少数保留，每一处都已在相应位置说明：三个公理模式和两条初始规则，它们不是证明出来的，而是选定的，而这一选择是否恰当，是本单元提出却没有完全回答的问题；强归纳法、结构归纳法、唯一可读性和递归定义，它们在上一单元中已经证明，在这里加以使用；以及集合论中不可缺少的部分（子集、并集和有穷集），在需要的地方作了回顾。除这些保留之外，走过的道路可以读作一条分为四段的演绎之链。

卢卡西维茨系统及其界限

关于形式演绎系统的一课把一个系统定义为一种语言、一些公理和一些规则，它们都只需看符号串就能检验，并确定了本课程系统的第一阶段，即卢卡西维茨系统：模式 A1、A2 和 A3，以及作为唯一规则的分离规则，唯一可读性使它能够无歧义地应用。它定义了从前提集 Γ\Gamma 出发的推演和关系 Γ⊢φ\Gamma \vdash \varphi，用五行推演出 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)，并证明了结构性质：自反性、单调性、推演之间的分离规则、切割规则和有穷性。借助这些性质以及对行数的强归纳法，它证明了演绎定理及其逆，演绎定理的第二种情形要求事先推演出 (φ→φ)(\varphi \rightarrow \varphi)；由它们得到可证等价，它是自反的、对称的和传递的。最后，它确立了该系统的界限：一个取值 00 和 11 的标记，在初始形式 (α↓β)(\alpha \downarrow \beta) 上递归地定义，照常处理否定和蕴涵，被 A1、A2、A3 和分离规则所保持，并让 (v1↓v2)(v_{1} \downarrow v_{2}) 这样的公式的值保持自由。由此可知，((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}) 不是卢卡西维茨系统的定理，并且由 (v1↓v2)(v_{1} \downarrow v_{2}) 推不出 (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2})，反之亦然。由于每个标记都给 θ\theta 和 ¬¬θ\neg\neg\theta 同一个值，这一课还指出，即使双重否定得到证明，也补救不了这一界限。

四种技巧与新规则

关于四种推演技巧的一课首先证明了“从结果到规则”引理：若 {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta，则同一结论可以从任何集合 Γ\Gamma 得到，只要它能推出各个 αi\alpha_{i}；此外还有 ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))。正是这条引理使每种技巧都能以三种方式呈现（从前提出发、作为定理和作为规则）；关于对称性和关于德摩根律的两课把等价链与切割规则结合起来，为此依靠的是第一课中可证等价的性质，那是同一想法应用于单个前提的情形；在链中每个结果只出现一次，即在它被证明的地方。借助这条引理，这一课用七行从 A1 和 A2 推演出假言三段论，用演绎定理推演出前提交换，推演出双重否定（它的第一个方向两次把 A3 应用于一个用 A1 造出的蕴涵，第二个方向把第一个方向应用于 ¬φ\neg\varphi，并使用 A3），以及三种形式的逆否律，它们以三种方式分配一个蕴涵中的否定；这四种技巧在卢卡西维茨系统中就已成立。

证明了双重否定之后，这一课用第二条初始规则即双重否定替换（双否替换）完成了本课程的系统：由 χ\chi 可推出 χ′\chi'，只要 χ′\chi' 是把 χ\chi 中子公式 θ\theta 的一次出现替换为 ¬¬θ\neg\neg\theta，或把 ¬¬θ\neg\neg\theta 的一次出现替换为 θ\theta 而得到的。这条规则必须作为公设，因为标记 m1m_{1} 给双重否定的各定理以 11，却把 (v1↓v2)(v_{1} \downarrow v_{2}) 与 (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}) 区分开来；双否替换不保持 m1m_{1}，因此扩大了可推演的范围，但它保持诚实标记，因此扩大得并不过分。这条规则作用于基础语言的符号串，在那里否定会把它的运算对象复制一份：(φ→ψ)(\varphi \rightarrow \psi) 两次含有子公式 ¬φ\neg\varphi，要在它的前件前面加上双重否定，就需要应用两次。同一观察支撑着演绎定理的推广：如果某一行是由这条规则得到的，归纳假设给出一个后件为前一行的蕴涵，再应用两次规则，在这个后件的每份副本中各一次，就得到所要的蕴涵；其余结构性质用同样的证明成立。最初的推论是：一个公式与由它经这条规则得到的每个公式等价，特别是 (φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi) 和 (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)；而相应的蕴涵，其他系统把它们当作公理，在这里则是定理。

联结词与替换

关于联结词的对称性的一课处理了圆圈与圆盘的语言所特有的困难：卢卡西维茨公理只谈否定和蕴涵，而几乎没有哪个或非是这两者之一。基本引理 (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi) 架起了桥梁：由于 ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi) 就是 ¬¬(¬¬φ↓ψ)\neg\neg(\neg\neg\varphi \downarrow \psi)，双否替换规则加上内层的双重否定，双重否定加上外层的双重否定；反方向上，双重否定和这条规则把它们去掉。借助基本引理，等价替换先在否定之下和蕴涵两边用逆否律和假言三段论证明，然后推广到或非的两个运算对象，再由此推广到析取和合取。规则与替换并不使对方成为多余：规则只在 θ\theta 与 ¬¬θ\neg\neg\theta 之间互换，而替换允许任意等价的公式；而用基本引理证明的替换反过来又依赖于这条规则。这一课随后证明了，其他教材当作定义的那些形式是等价式：(φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)，它需要两次应用规则，在外层否定造出的每份副本中各一次；以及 (φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)，它需要双重否定；相反，(φ∧ψ)(\varphi \wedge \psi) 与 ¬(φ→¬ψ)\neg(\varphi \rightarrow \neg\psi) 是同一个符号串。最后，它按照定义所规定的顺序证明了五种对称性：或非的对称性用基本引理和逆否律证明，其余每一种都用前一种证明，必要时借助否定之下的替换加以转移。

经典规则与定律

关于经典逻辑的技巧的一课证明了下列规则，全部带着一个逐行传递的前提集 Γ\Gamma：析取与合取的引入和消去、排中律和不矛盾律、爆炸原理、两种形式的归谬法以及分情况证明，后者既可以用一个公式及其否定，也可以用任意析取。依赖的顺序是严格的：爆炸原理依赖于析取的规则；经典形式的归谬法依赖于爆炸原理和 A3；分情况证明依赖于逆否律和归谬法。这些证明都不直接援引双否替换规则：这条规则通过替代形式和等价替换起作用。关于德摩根律与分配律的一课让这些规则协同工作：德摩根第一定律由合取的定义和双重否定得出；第二定律则要求进入或非的内部，在那里双否替换规则介入两次，每个运算对象一次，且不需要对称性；由它可知 (φ↓ψ)(\varphi \downarrow \psi) 等价于 (¬φ∧¬ψ)(\neg\varphi \wedge \neg\psi)，即上一单元约定的读法“既非 φ\varphi 也非 ψ\psi”；其变体包括 ¬(φ→ψ)⊣⊢(φ∧¬ψ)\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi)。两条分配律都用分情况证明在两个方向上得到证明，每个方向选用合适的分情况证明形式。

下图把四段汇成一条链。中间一列的每个节点是一个定义或一个结果，按逻辑顺序编号，并用弧线连到其证明所用到的前面的环节；四周浮动的是支柱，即这条链一再求助的原理和工具，每个支柱用实线连到依靠它的环节，用虚线连到确立它的环节，而这条链没有证明的支柱（被接受的公理模式，以及上一单元的工具）则画成圆环。双重否定替换规则虽然同样不加证明而被接受，却连到引入它的那一环节，因为那里解释了为什么必须把它作为公设。点击一个支柱，会突出显示所有用到它的环节；每个环节都链接到证明它的那一课。请注意，除公理之外，演绎定理和双重否定是本单元最常用到的支柱，而新规则支撑着本单元关于或非所说的一切：推广后的演绎定理、基本引理、替代形式以及德摩根第二定律。

链的支柱

  • A唯一可读性与递归. 若 ∙φψ=∙φ′ψ′\sigI\varphi\psi = \sigI\varphi'\psi'，且四个符号串都是公式，则 φ=φ′\varphi = \varphi' 且 ψ=ψ′\psi = \psi'；由此，一条规则，若它计算 ∙φψ\sigI\varphi\psi 的值所依据的是 φ\varphi、ψ\psi 以及它们的值，便在公式上定义唯一的一个函数。已在上一单元中证明。 本单元中不加证明而采用。
  • B强归纳法. 如果一个性质每当对所有较小的自然数成立时就对一个自然数成立，那么它对所有自然数成立。上一单元由简单归纳法推出了它，这里把它应用于一个推演的行数。 本单元中不加证明而采用。
  • C卢卡西维茨公理. 模式 A1，(φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi))；A2，((φ→(ψ→χ))→((φ→ψ)→(φ→χ)))((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))；以及 A3，((¬ψ→¬φ)→(φ→ψ))((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))。予以接受。 本单元中不加证明而采用。
  • D双重否定替换. 本课程系统的第二条初始规则：由 χ\chi 可推出 χ′\chi'，只要 χ′\chi' 是把 χ\chi 中子公式 θ\theta 的一次出现替换为 ¬¬θ\neg\neg\theta，或把 ¬¬θ\neg\neg\theta 的一次出现替换为 θ\theta 而得到的。在证明双重否定之后作为公设引入。 确立于: 8. 双重否定替换.
  • E演绎定理. Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi 当且仅当 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)；在卢卡西维茨系统中证明，并在本课程的系统中多一种情形而仍然成立。 确立于: 3. 演绎定理与可证等价.
  • F从结果到规则. 若 {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta，且 Γ⊢αi\Gamma \vdash \alpha_{i} 对每个 ii 成立，则 Γ⊢β\Gamma \vdash \beta：每种从前提出发证明的技巧都可以在任意前提集之下应用。 确立于: 5. 从结果到规则.
  • G双重否定. φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi，以及定理 ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) 和 ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi)。 确立于: 7. 双重否定.
  • H等价替换. 若 φ⊣⊢φ′\varphi \dashv\vdash \varphi'，则可以用 φ′\varphi' 代替 φ\varphi，在否定之下，在蕴涵、或非、析取和合取的两边，而不改变等价关系。 确立于: 12. 等价替换.

  1. 第 1 段 卢卡西维茨系统及其界限

    • 识别模式的实例，并判定一个公式序列是否是从某个前提集出发的推演。
    • 用对行数的强归纳法证明推演的结构性质和演绎定理。
    • 用自反性、单调性、切割规则、演绎定理及其逆构造关于推演的推演。
    • 借助一个被公理和分离规则保持的标记证明某个公式推不出来，并用它解释卢卡西维茨系统的界限。

    1. 系统、推演与同一律. 卢卡西维茨系统的公理是 A1 至 A3 的统一代入实例，其唯一规则是分离规则。Γ⊢φ\Gamma \vdash \varphi，若存在一个以 φ\varphi 结尾的有穷公式序列，其中每个公式是公理、Γ\Gamma 的元素，或由前面两个公式用分离规则得到。第一个定理 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) 用 A1 和 A2 以五行推演出来。

      依据: A (唯一可读性与递归), C (卢卡西维茨公理). 证明于: 形式演绎系统.

    2. 结构性质. 若 φ∈Γ\varphi \in \Gamma，则 Γ⊢φ\Gamma \vdash \varphi；若 Γ⊆Δ\Gamma \subseteq \Delta 且 Γ⊢φ\Gamma \vdash \varphi，则 Δ⊢φ\Delta \vdash \varphi；由 Γ⊢φ\Gamma \vdash \varphi 和 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi) 得 Γ⊢ψ\Gamma \vdash \psi；若 Γ⊢φi\Gamma \vdash \varphi_{i} 对每个 ii 成立，且 Γ∪{φ1,…,φr}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{r}\} \vdash \psi，则 Γ⊢ψ\Gamma \vdash \psi；若 Γ⊢φ\Gamma \vdash \varphi，则 Γ\Gamma 的某个有穷子集就足够了。

      使用: 1. 系统、推演与同一律. 证明于: 形式演绎系统.

    3. 演绎定理与可证等价. Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi 当且仅当 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)，用对行数的强归纳法，借助 A1、A2 和同一律证明。由此，可证等价 φ⊣⊢ψ\varphi \dashv\vdash \psi 是自反的、对称的和传递的，而两个等价的公式可从同样的集合推出。

      使用: 1. 系统、推演与同一律, 2. 结构性质. 依据: B (强归纳法), C (卢卡西维茨公理). 证明于: 形式演绎系统.

    4. 卢卡西维茨系统的界限. 一个递归定义的、取值 00 和 11 的标记满足 m(¬φ)=1−m(φ)m(\neg\varphi) = 1 - m(\varphi) 和 m((φ→ψ))=1−m(φ)(1−m(ψ))m((\varphi \rightarrow \psi)) = 1 - m(\varphi) \left( 1 - m(\psi) \right)，而 A1、A2、A3 和分离规则保持标记 11；由此 ((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}) 不是卢卡西维茨系统的定理，且 {(v1↓v2)}⊬(¬¬v1↓v2)\{(v_{1} \downarrow v_{2})\} \nvdash (\neg\neg v_{1} \downarrow v_{2})，反之亦然。由于每个标记都给双重否定以 11，替换必须作为公设。

      使用: 1. 系统、推演与同一律. 依据: A (唯一可读性与递归), B (强归纳法), C (卢卡西维茨公理). 证明于: 形式演绎系统.

  2. 第 2 段 四种技巧与新规则

    • 把一个从前提出发的结果转化为一个定理和一条可在任意前提集之下应用的规则。
    • 串联蕴涵，调整前件的顺序，加上和去掉双重否定，并为每个蕴涵选择相应的逆否律形式。
    • 应用双重否定替换规则，找出缩写所隐藏的出现，并在否定造出的每份副本中重复应用它。
    • 用标记解释为什么这条规则要作为公设，并证明演绎定理在加入它之后仍然成立。

    1. 从结果到规则. 若 {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta，则由 Γ⊢α1\Gamma \vdash \alpha_{1}、…\ldots、Γ⊢αn\Gamma \vdash \alpha_{n} 得 Γ⊢β\Gamma \vdash \beta，并且 ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))；特别地，若 α⊣⊢α′\alpha \dashv\vdash \alpha'，则 Γ⊢α\Gamma \vdash \alpha 当且仅当 Γ⊢α′\Gamma \vdash \alpha'。

      使用: 2. 结构性质. 依据: E (演绎定理). 证明于: 四种推演技巧.

    2. 假言三段论与前提交换. {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)，由 A1 和 A2 出发的一个七行推演；以及 {(φ→(ψ→χ))}⊢(ψ→(φ→χ))\{(\varphi \rightarrow (\psi \rightarrow \chi))\} \vdash (\psi \rightarrow (\varphi \rightarrow \chi))。

      使用: 1. 系统、推演与同一律. 依据: C (卢卡西维茨公理), E (演绎定理), F (从结果到规则). 证明于: 四种推演技巧.

    3. 双重否定. ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi)，把 A3 两次应用于 A1 从 ¬¬φ\neg\neg\varphi 造出的一个蕴涵；⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi)，把前一结果应用于 ¬φ\neg\varphi，并使用 A3；由此 φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi，在卢卡西维茨系统中就已成立。

      依据: C (卢卡西维茨公理), E (演绎定理). 证明于: 四种推演技巧.

    4. 双重否定替换. 双否替换规则作为公设引入，因为标记给双重否定以 11，却不这样对待或非内部的替换。若 χ′\chi' 由 χ\chi 经这条规则得到，则 χ⊣⊢χ′\chi \dashv\vdash \chi'；特别地，(φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi) 和 (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)。

      使用: 3. 演绎定理与可证等价, 4. 卢卡西维茨系统的界限. 依据: G (双重否定). 证明于: 四种推演技巧.

    5. 本课程的系统中的演绎定理. 自反性、单调性、切割规则和有穷性在新规则下仍然成立，而且 Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi 当且仅当 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)：在新情形中，由于 (φ→χ)(\varphi \rightarrow \chi) 就是 ((¬φ↓χ)↓(¬φ↓χ))((\neg\varphi \downarrow \chi) \downarrow (\neg\varphi \downarrow \chi))，规则应用两次，在 χ\chi 的每份副本中各一次。由此，⊢((φ↓ψ)→(¬¬φ↓ψ))\vdash ((\varphi \downarrow \psi) \rightarrow (\neg\neg\varphi \downarrow \psi)) 及其逆都是定理。

      使用: 2. 结构性质, 3. 演绎定理与可证等价. 依据: B (强归纳法), D (双重否定替换). 证明于: 四种推演技巧.

    6. 逆否律. (φ→ψ)⊣⊢(¬ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi)、(¬φ→ψ)⊣⊢(¬ψ→φ)(\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi) 和 (φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)：两端互换位置，每一端在换过去时改变符号。

      使用: 6. 假言三段论与前提交换. 依据: C (卢卡西维茨公理), E (演绎定理), G (双重否定), F (从结果到规则). 证明于: 四种推演技巧.

  3. 第 3 段 联结词与替换

    • 展开缩写，以判定两个表达式指称的是同一个符号串，还是其等价性需要推演的两个公式。
    • 用基本引理把或非翻译为否定和蕴涵。
    • 用等价替换把一个等价关系移入公式内部，把它与双重否定替换规则区分开来，并串联等价式。
    • 按照定义所规定的顺序证明五种对称性。

    1. 基本引理. (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)：由于 ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi) 就是 ¬¬(¬¬φ↓ψ)\neg\neg(\neg\neg\varphi \downarrow \psi)，双否替换规则加上内层的双重否定，双重否定加上外层的；反方向上，双重否定和这条规则把它们去掉。

      依据: D (双重否定替换), G (双重否定). 证明于: 联结词的对称性.

    2. 等价替换. 若 φ⊣⊢φ′\varphi \dashv\vdash \varphi'，则 ¬φ⊣⊢¬φ′\neg\varphi \dashv\vdash \neg\varphi'、(φ→ψ)⊣⊢(φ′→ψ)(\varphi \rightarrow \psi) \dashv\vdash (\varphi' \rightarrow \psi) 且 (ψ→φ)⊣⊢(ψ→φ′)(\psi \rightarrow \varphi) \dashv\vdash (\psi \rightarrow \varphi')；借助基本引理，在或非的两边同样成立，再由此推及析取与合取。与双否替换规则不同，它允许任意等价的公式。

      使用: 6. 假言三段论与前提交换, 10. 逆否律, 11. 基本引理. 依据: E (演绎定理). 证明于: 联结词的对称性.

    3. 替代形式. (φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)，需要两次应用双否替换规则，在外层否定造出的每份副本中各一次；(φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)，由双重否定；而 (φ∧ψ)(\varphi \wedge \psi) 与 ¬(φ→¬ψ)\neg(\varphi \rightarrow \neg\psi) 是同一个符号串。

      依据: D (双重否定替换), G (双重否定). 证明于: 联结词的对称性.

    4. 五种对称性. (φ↓ψ)⊣⊢(ψ↓φ)(\varphi \downarrow \psi) \dashv\vdash (\psi \downarrow \varphi)，由基本引理和逆否律；由它依次得到 ∨\vee、∧\wedge、↔\leftrightarrow 和 ⊻\veebar 的对称性，每一种都用前一种，必要时借助否定之下的替换加以转移。

      使用: 11. 基本引理, 10. 逆否律. 依据: H (等价替换). 证明于: 联结词的对称性.

  4. 第 4 段 经典规则与定律

    • 在带前提的情况下证明析取与合取的引入和消去、排中律和不矛盾律。
    • 在带前提的情况下证明爆炸原理、归谬法和分情况证明，并解释为什么不带前提它们就不够用。
    • 用推演证明德摩根律、它们的变体以及两个方向上的分配律。
    • 通过有依据的等价链把公式化为简单的范式。

    1. 联结词的规则. 对任意 Γ\Gamma：由 φ\varphi 得 (φ∨ψ)(\varphi \vee \psi)；由 (φ∨ψ)(\varphi \vee \psi) 和 ¬φ\neg\varphi 得 ψ\psi；由 φ\varphi 和 ψ\psi 得 (φ∧ψ)(\varphi \wedge \psi)；由 (φ∧ψ)(\varphi \wedge \psi) 得 φ\varphi 和 ψ\psi；此外，⊢(φ∨¬φ)\vdash (\varphi \vee \neg\varphi) 且 ⊢¬(φ∧¬φ)\vdash \neg(\varphi \wedge \neg\varphi)。

      使用: 1. 系统、推演与同一律, 2. 结构性质, 6. 假言三段论与前提交换, 10. 逆否律, 13. 替代形式, 14. 五种对称性. 依据: C (卢卡西维茨公理), E (演绎定理), F (从结果到规则), G (双重否定). 证明于: 经典逻辑的技巧.

    2. 爆炸原理与归谬法. 若 Γ⊢φ\Gamma \vdash \varphi 且 Γ⊢¬φ\Gamma \vdash \neg\varphi，则 Γ⊢ψ\Gamma \vdash \psi 对一切 ψ\psi 成立；若由 Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} 能推出 ψ\psi 和 ¬ψ\neg\psi，则 Γ⊢φ\Gamma \vdash \varphi；若由 Γ∪{φ}\Gamma \cup \{\varphi\} 能推出它们，则 Γ⊢¬φ\Gamma \vdash \neg\varphi。

      使用: 1. 系统、推演与同一律, 2. 结构性质, 15. 联结词的规则. 依据: C (卢卡西维茨公理), E (演绎定理), G (双重否定). 证明于: 经典逻辑的技巧.

    3. 分情况证明. 若 Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi 且 Γ∪{¬φ}⊢ψ\Gamma \cup \{\neg\varphi\} \vdash \psi，则 Γ⊢ψ\Gamma \vdash \psi；若 Γ∪{φ}⊢χ\Gamma \cup \{\varphi\} \vdash \chi、Γ∪{ψ}⊢χ\Gamma \cup \{\psi\} \vdash \chi 且 Γ⊢(φ∨ψ)\Gamma \vdash (\varphi \vee \psi)，则 Γ⊢χ\Gamma \vdash \chi。

      使用: 2. 结构性质, 10. 逆否律, 15. 联结词的规则, 16. 爆炸原理与归谬法. 依据: E (演绎定理). 证明于: 经典逻辑的技巧.

    4. 德摩根律. ¬(φ∧ψ)⊣⊢(¬φ∨¬ψ)\neg(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \vee \neg\psi)，由定义和双重否定；¬(φ∨ψ)⊣⊢(¬φ∧¬ψ)\neg(\varphi \vee \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi)，在或非的每个运算对象中各应用一次双否替换规则；由此 (φ↓ψ)⊣⊢(¬φ∧¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi) 且 ¬(φ→ψ)⊣⊢(φ∧¬ψ)\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi)。

      依据: D (双重否定替换), G (双重否定), H (等价替换). 证明于: 德摩根律与分配律.

    5. 分配律. (φ∧(ψ∨χ))⊣⊢((φ∧ψ)∨(φ∧χ))(\varphi \wedge (\psi \vee \chi)) \dashv\vdash ((\varphi \wedge \psi) \vee (\varphi \wedge \chi)) 与 (φ∨(ψ∧χ))⊣⊢((φ∨ψ)∧(φ∨χ))(\varphi \vee (\psi \wedge \chi)) \dashv\vdash ((\varphi \vee \psi) \wedge (\varphi \vee \chi))，各自在两个方向上用分情况证明；借助对称性，从右边也成立。

      使用: 14. 五种对称性, 15. 联结词的规则, 17. 分情况证明. 依据: H (等价替换). 证明于: 德摩根律与分配律.

走向语义. 这条链停在推演已涵盖数学据以推理的全部技巧之处。还有待知道的是：推演出的东西是否恰好就是在每个赋值下都为真的东西；下一单元将定义真，最后一个单元将比较这两个概念。

依据的缩写

本单元的推演用一个缩写为每一行注明依据，各课所用的缩写相同。这里把它们汇集起来，按引入它们的那一课排列。“前提”指题设中的一个假设，在关于推演的推演中则指所证规则的一个假设。括号中的数字指出规则所应用的行；一个已经证明的等价式，在作为一行写出时不带编号，在应用于某一行时则带上被变换的那一行的编号，在应用于该行的某一部分时也是如此，此时用“等价替换”。

  • 第一课：A1、A2 和 A3（公理模式）；MP(i,j)(i, j)（分离规则，modus ponens）；定义（缩写的展开或收回，后接所展开的联结词：“定义 ∨\vee”“定义 ⊣⊢\dashv\vdash”）；同一律（即定理 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)）；自反（自反性：若 φ∈Γ\varphi \in \Gamma，则 Γ⊢φ\Gamma \vdash \varphi）；单调（单调性）；切割（切割规则：已推演出的公式可以用作前提）；有穷（有穷性）；演绎定理及逆演绎（演绎定理的逆）。
  • 第二课：假言三段论；前提交换；双重否定；双否替换(i)(i)（在第 ii 行应用双重否定替换；不带编号的双否替换指一个公式与由它经这条规则得到的公式之间的等价）；逆否（逆否律，三种形式中的任何一种）；“例题 nn”（同一课中例题 nn 的一个结果，作为一行写出）。
  • 第三课：基本引理（(φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)）；等价替换（任何一种形式的等价替换，后接所应用的等价式：“等价替换，德摩根(i)(i)”）；替代形式（析取与合取的替代形式，(φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi) 和 (φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)）；对称（联结词的对称性）。
  • 第四课：∨\vee引入与 ∨\vee消去（析取的引入和消去）；∧\wedge引入与 ∧\wedge消去（合取的引入和消去）；排中律；不矛盾律（这一缩写为定理命名，但不为本单元的任何一行提供依据）；爆炸（爆炸原理）；分情况(i,j)(i, j) 与分情况(i,j,k)(i, j, k)（分情况证明，用一个公式及其否定，或用一个析取）；“无前提分情况”（不带集合 Γ\Gamma 的分情况证明，只在一道题中出现）；归谬（归谬法，两种形式）。
  • 第五课：德摩根（德摩根律）；分配律；结合律（析取的结合律）；实例(i)(i)（第 ii 行对任意公式成立，用其他公式代替其元变元重新写出；注明所作的代入）。
  • 本课的挑战题：M3（第三道挑战题用来代替 A3 的模式）。