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

四种推演技巧

摘要

上一课的卢卡西维茨系统由三个公理模式和唯一一条规则即分离规则构成；手段如此之少，每个推演都必须从公理出发构造，连公式 (φ→φ)(\varphi \rightarrow \varphi) 也需要五行。本课增加四种技巧，它们只需证明一次，此后反复使用：假言三段论，它把蕴涵串联起来；前提交换，它允许改变前件的次序；双重否定，它允许添加和去掉两个相连的否定；以及逆否律，它有三种形式，允许通过否定蕴涵的两端而把蕴涵倒转过来。每种技巧都用三条公理、分离规则和上一课的元定理逐行完整地证明，并以三种形式得到：作为从前提出发的推演，作为定理，以及作为在任何前提集下都可应用的规则。证得双重否定之后，本课用第二条初始规则即双重否定替换来完善系统，它允许在公式的任何位置添加或去掉两个否定，包括三条公理无法触及的或非内部；本课说明为什么这条规则必须作为公设引入，验证推演的性质得以保持，用新的情形扩充演绎定理，并得出它的初步推论。

学习目标

  1. 借助演绎定理把形如 {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta 的结果转化为定理，并借助单调性和切割规则把它转化为在任何前提集 Γ\Gamma 下都可应用的规则。
  2. 既通过由 A1 和 A2 出发的直接推演，也通过借助演绎定理对推演进行推理，来证明假言三段论和前提交换，并用它们串联蕴涵、调整蕴涵的次序。
  3. 用 A1 至 A3 和分离规则证明双重否定的两个方向，并在推演中用它们添加或去掉两个相连的否定。
  4. 陈述双重否定替换规则，在基础语言的符号串中找出子公式的出现，包括被缩写隐藏的出现，并在推演中应用这条规则。
  5. 用标记说明为什么双重否定替换必须作为公设引入，并证明推演的性质和演绎定理在扩充后的系统中仍然成立。
  6. 证明逆否律的三种形式，并在面对带有否定的蕴涵时选择相应的形式。
  7. 把四种技巧和新规则与公理、分离规则和演绎定理结合起来，构造非平凡的推演，并用相应的缩写为每一行给出依据。

出发时的工具

在关于形式演绎系统的一课中确立了卢卡西维茨系统。它的语言是圆圈与圆盘的语言，用关于命题逻辑的语言的一课中的正式缩写书写；它的公理是下面三个模式的全部实例，其中 φ\varphi、ψ\psi 和 χ\chi 是任意公式；它唯一的规则是分离规则。

  • 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))。
  • MP：由 φ\varphi 和 (φ→ψ)(\varphi \rightarrow \psi) 推出 ψ\psi。

φ\varphi 的一个由公式集 Γ\Gamma 出发的推演，是一个以 φ\varphi 结尾的有穷公式序列，其中每个公式或是公理，或是 Γ\Gamma 的元素，或是对前面两个公式应用分离规则的结果；若这样的推演存在，就写作 Γ⊢φ\Gamma \vdash \varphi，若 Γ\Gamma 为空，则写作 ⊢φ\vdash \varphi，并称 φ\varphi 是定理。同一课证明了我们在这里要用的元定理：自反性（自反：若 φ∈Γ\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 取 11 到 nn 的每个值，且 Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi，则 Γ⊢ψ\Gamma \vdash \psi），有穷性（若 Γ⊢φ\Gamma \vdash \varphi，则 Γ\Gamma 的某个有穷子集就已足够），演绎定理（若 Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi，则 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)）及其逆（逆演绎），以及定理 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)，在依据中我们把它缩写为同一律。最后，φ⊣⊢ψ\varphi \dashv\vdash \psi（可证等价）的意思是 {φ}⊢ψ\{\varphi\} \vdash \psi 且 {ψ}⊢φ\{\psi\} \vdash \varphi。

需要记住，¬\neg 和 →\rightarrow 不是基础语言的符号，而是缩写：¬φ\neg\varphi 是符号串 (φ↓φ)(\varphi \downarrow \varphi)，而 (φ→ψ)(\varphi \rightarrow \psi) 是 (¬φ∨ψ)(\neg\varphi \vee \psi)，即 ¬(¬φ↓ψ)\neg(\neg\varphi \downarrow \psi)。三条公理只谈论否定和蕴涵，同一课借助一种取值为 00 和 11、被它们和分离规则所保持的标记，表明了由此产生的界限：在卢卡西维茨系统中，由 (v1↓v2)(v_{1} \downarrow v_{2}) 推演不出 (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2})，或非有一部分处在它的能力之外。因此，本课分两个阶段进行。直到双重否定为止（包括双重否定），⊢\vdash 指卢卡西维茨系统，所证的一切都不依赖于展开缩写。证得双重否定之后，给系统添加第二条初始规则，即双重否定替换，它作用于展开后的符号串；从这时起，⊢\vdash 指本课程的系统，即卢卡西维茨系统加上这条规则。由于前一系统中的每个推演也是后一系统中的推演，此前所证的一切都不会丢失。

推演的两种风格

推演有两种写法，两者都会用到。第一种是严格意义上的推演，即一个公式序列，其中每一行是公理、前提或分离规则的结果；每一行的依据写作 A1、A2、A3、前提或 MP(i,j)(i, j)，其中第 ii 行是前件，第 jj 行是前件恰好为第 ii 行的蕴涵（引入新规则之后，还有双否替换(i)(i)）。第二种是关于推演的推演，它的各行不是公式，而是形如 Γ⊢φ\Gamma \vdash \varphi 的断言；每一行都以一个已证的元定理为依据，整个序列是元语言中的一段推理，它保证存在一个第一种风格的推演，尽管并不把它写出来。第二种风格的依据按如下方式理解。

  • 自反：右边的公式属于左边的集合。
  • A1、A2、A3：右边的公式是该模式的实例；公理的实例可以用只有一行的推演从任何 Γ\Gamma 推出。
  • MP(i,j)(i, j)：推演之间的分离规则，应用于第 ii 行 Γ⊢φ\Gamma \vdash \varphi 和第 jj 行 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)，两者的 Γ\Gamma 相同。
  • 演绎定理(i)(i) 和逆演绎(i)(i)：应用于第 ii 行的演绎定理或其逆。
  • 已证定理的名称，如同一律或双重否定：右边的公式是该定理的实例，由单调性可从任何 Γ\Gamma 推出，因为空集包含于 Γ\Gamma。
  • 前提，在关于推演的推演中：该行是正在证明的规则的假设之一。

本课的每个结果都用元变元陈述，因而对任意公式都成立：它的证明是一个模式，在其中每个元变元处代入一个公式，就得到另一个证明，因为公理模式的实例仍是实例，每次分离规则的应用也仍是分离规则的应用（新规则的每次应用同样如此）。例如，由 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) 可得 ⊢(¬ψ→¬ψ)\vdash (\neg\psi \rightarrow \neg\psi)，即以 ¬ψ\neg\psi 代替 φ\varphi。这种手法，即把一个结果应用于比陈述中更复杂的公式，在后面最为有用。

从结果到规则

本课的技巧是从固定的前提出发证明的，例如 {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)；但它们是在带有其他前提的推演中间使用的，在那里 (φ→ψ)(\varphi \rightarrow \psi) 和 (ψ→χ)(\psi \rightarrow \chi) 不是前提，而是已经推出的公式。下面的引理是单调性和切割规则的直接推论，它一劳永逸地允许这样使用。

引理从结果到规则

若 {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta，则对每个公式集 Γ\Gamma，由 Γ⊢α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))。

证明

  1. Γ∪{α1,…,αn}⊢β\dato{mon}{\Gamma \cup \{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta}

    由假设，β\beta 可从各公式 αi\alpha_{i} 推出。由于 {α1,…,αn}\{\alpha_{1}, \ldots, \alpha_{n}\} 包含于 Γ∪{α1,…,αn}\Gamma \cup \{\alpha_{1}, \ldots, \alpha_{n}\}，单调性允许把 Γ\Gamma 加入前提。

  2. Γ⊢β\Gamma \vdash \resaltar{\beta}

    若每个 αi\alpha_{i} 又都可从 Γ\Gamma 推出，切割规则便消去了加入的前提。

  3. ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))

    对于定理形式，演绎定理应用 nn 次，从最后一个到第一个依次解除前提；每次应用都把被解除的前提变成一个蕴涵的前件。

由此可知，每种从前提出发证明的技巧都有三种形式：结果本身，解除其前提所得的定理，以及在任何 Γ\Gamma 下都可应用的规则。在关于推演的推演中，引用规则时写出技巧的名称和它所应用的各行的行号，如假言三段论(3,4)(3, 4)，而引理保证这一步是合法的。