跳至内容
Topos Uranos

摘要

在数学中推理的人引入和消去合取与析取,援引排中律,排除矛盾的东西,区分情况,进行归谬,而几乎总是没有意识到自己在这样做。本课证明,所有这些技巧都是本课程的演绎系统的派生规则,并以它们被使用的形式来证明它们:带有一个在整个推演中保持不变的前提集 Γ\Gamma。本课先回顾,每条已证的规则在语境 Γ\Gamma 中都成立;然后证明析取与合取的引入和消去、排中律与不矛盾律、爆炸原理、两种形式的归谬法以及分情况证明,先是用一个公式及其否定,再用任意一个析取。问题把这些技巧应用于皮尔士律和二难推理等经典定律,并说明为什么不带前提地证明它们是不够的。

学习目标

  1. 把先前证明的规则和等价应用于形如 Γ⊢φ\Gamma \vdash \varphi 的行,并用单调性和切割规则为这一步提供依据。
  2. 带前提地证明析取与合取的引入规则和消去规则,只在允许之处展开正式缩写。
  3. 推出排中律和不矛盾律,并在每一步区分什么是定义、什么是定理。
  4. 带前提地证明爆炸原理、两种形式的归谬法和分情况证明,并解释为什么不带前提的版本不够。
  5. 结合这些技巧构造经典定律(皮尔士律、输出律、二难推理)的推演,并把一个公式的可推演性与一个前提集的不一致性联系起来。

语境中的规则

在关于形式演绎系统的一课中确立了卢卡西维茨系统:公理模式 A1、A2 和 A3,分离规则(MP),以及从前提集 Γ\Gamma 出发的推演这一概念,连同它最初的几条性质:自反性(自反:若 φ∈Γ\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,它也引作 MP),演绎定理(若 Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi,则 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi))及其逆(逆演绎)。关于四种推演技巧的一课和关于联结词的对称性的一课加入了假言三段论、前提交换、双重否定、三种形式的逆否律(逆否)、等价替换、对称性(对称)以及析取与合取的替代形式。前一课在证明双重否定之后,还给本课程的系统补充了第二条初始规则,即双重否定替换(双否替换):若 χ′\chi' 由 χ\chi 把子公式 θ\theta 的一次出现替换为 ¬¬θ\neg\neg\theta,或把 ¬¬θ\neg\neg\theta 的一次出现替换为 θ\theta 而得,则由 χ\chi 可推出 χ′\chi'。此后,⊢\vdash 指这个系统(A1 至 A3、MP 和双否替换),在其中自反性、单调性、切割规则、演绎定理及其逆仍然成立;本课的技巧都是它的派生规则,尽管它们的证明都没有直接引用双否替换:这条规则通过替代形式和等价替换起作用,而关于对称性的一课正是借助它证明了这两者。

然而,在数学中没有人不带前提地推理:人们从一些公理、从一个定理的条件、从为讨论某种情况而作的假设出发进行推理。若是这样,一种推理技巧只有在带着一个逐行传递的前提集 Γ\Gamma 陈述时才有用。由此可知,本课的每条规则都对任意的 Γ\Gamma 陈述和证明;不带前提的情形是特殊情形 Γ=∅\Gamma = \emptyset,而不是反过来。

这些证明是关于推演的推演:每一行断言某个东西可从一个集合推出,即 Γ⊢φ\Gamma \vdash \varphi,其依据指向前面的行。在这些证明中,“前提”标出规则的陈述所假定的行;而一条公理(A1、A3)或一个已证定理(如同一律,即定理 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi))的名称,标出这样一行 Γ⊢φ\Gamma \vdash \varphi:其中 φ\varphi 是该模式或该定理的一个实例,可从任何集合推出。

关于四种推演技巧的一课借助单调性和切割规则证明了“从结果到规则”引理,它使这种工作方式成为可能:若 {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta,且 Γ⊢αi\Gamma \vdash \alpha_{i} 对每个 ii 成立,则 Γ⊢β\Gamma \vdash \beta。取 n=1n = 1,并在等价 α⊣⊢α′\alpha \dashv\vdash \alpha' 的每个方向上应用它,它说的是:Γ⊢α\Gamma \vdash \alpha 当且仅当 Γ⊢α′\Gamma \vdash \alpha'。因此,每条已证的规则和每个已证的等价都可应用于带前提的推演的各行:若某一行是 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi),逆否律允许在它下面写出 Γ⊢(¬ψ→¬φ)\Gamma \vdash (\neg\psi \rightarrow \neg\varphi),并以“逆否”和该行的行号作为依据。对于关于对称性的一课中的两种替代形式(它们将不断被使用),写作“替代形式”:

(φ∨ψ)⊣⊢(¬φ→ψ)(φ∧ψ)⊣⊢¬(φ→¬ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi) \qquad (\varphi \wedge \psi) \dashv\vdash \neg(\varphi \rightarrow \neg\psi)

必须强调,这两个等价中的第一个并不是定义;第二个,正如关于对称性的一课所表明的,是符号串的恒等,但它与第一个一起引作“替代形式”。按定义,(φ∨ψ)(\varphi \vee \psi) 是 ¬(φ↓ψ)\neg(\varphi \downarrow \psi),(¬φ→ψ)(\neg\varphi \rightarrow \psi) 是 (¬¬φ∨ψ)(\neg\neg\varphi \vee \psi),它们是不同的符号串;“按蕴涵的定义”把其中一个读作另一个,正是本课要避免的错误。相反,“定义”专用于以另一个名称书写同一个符号串,例如把 (φ→ψ)(\varphi \rightarrow \psi) 读作 (¬φ∨ψ)(\neg\varphi \vee \psi)。