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

联结词的对称性

摘要

本课证明：运算对象的次序不改变由或非、析取、合取、双条件和不相容析取所能推出的东西。在本课程的正式缩写下，这些对称性并不显然：或非是初始联结词，卢卡西维茨的公理只谈否定和蕴涵，而双重否定替换规则只添加或去掉双重否定。因此本课先建立三件工具。第一件说明可证等价表现得像等式。第二件是基本引理，它把或非翻译成公理的语言：(φ↓ψ)(\varphi \downarrow \psi) 等价于 ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi)，这要归功于双重否定替换规则和双重否定。第三件是等价替换，双重否定替换规则并不使它成为多余；它允许在否定之下、蕴涵的两侧以及或非的两侧，把一个公式换成与之等价的任意公式（而不只是把 θ\theta 换成 ¬¬θ\neg\neg\theta）。借助这三件工具，本课把析取与合取的替代形式作为等价式加以证明（别的教材把它们当作定义），并证明五种对称性，两个方向都证，次序由定义决定：先证或非，再由它依次证其余的。

学习目标

  1. 展开正式缩写，以判定两个表达式指称同一个公式，还是指称其等价性需要推演的不同公式。
  2. 用双重否定替换规则和双重否定证明基本引理 (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)，并找出缩写所隐藏的双重否定。
  3. 运用等价替换把一个等价式移入否定、蕴涵或或非的内部，把它与只交换 θ\theta 和 ¬¬θ\neg\neg\theta 的双重否定替换规则区分开来，并在等价链中把可证等价当作等式使用。
  4. 证明析取与合取的替代形式以及两个方向上的五种对称性，把已经证明的结果串联起来。
  5. 借助对公式复杂度的归纳，把等价替换推广到任意公式。

所用的结果与有待证明的结果

关于形式演绎系统的一课确立了卢卡西维茨系统：公理 A1、A2、A3 和分离规则。它还建立了自反性（自反：若 φ∈Γ\varphi \in \Gamma，则 Γ⊢φ\Gamma \vdash \varphi）、单调性（单调）、切割规则（切割：若 Γ⊢φi\Gamma \vdash \varphi_{i} 对每个 ii 都成立，并且 Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi，则 Γ⊢ψ\Gamma \vdash \psi）、演绎定理及其逆（逆演绎），以及可证等价 φ⊣⊢ψ\varphi \dashv\vdash \psi，其含义是 {φ}⊢ψ\{\varphi\} \vdash \psi 并且 {ψ}⊢φ\{\psi\} \vdash \varphi；它还借助一个由公理和分离规则保持的标记表明，这个系统推不出某些关于或非的公式。关于四种推演技巧的一课增加了假言三段论（{(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)）、前提交换、双重否定（φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi，以及它的两个定理 ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) 和 ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi)）和逆否律的三种形式：

(φ→ψ)⊣⊢(¬ψ→¬φ),(¬φ→ψ)⊣⊢(¬ψ→φ),(φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), \qquad (\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi), \qquad (\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)

证明双重否定之后，同一课用第二条初始规则即双重否定替换补全了本课程的系统：若 χ′\chi' 由 χ\chi 把子公式 θ\theta 的一次出现替换为 ¬¬θ\neg\neg\theta，或把子公式 ¬¬θ\neg\neg\theta 的一次出现替换为 θ\theta 而得，则由 χ\chi 可推出 χ′\chi'。这样由第 ii 行得到的行以双否替换(i)(i) 为依据。从此以后，⊢\vdash 指本课程的系统（A1 至 A3、分离规则和双重否定替换），在其中自反性、单调性、切割规则、演绎定理及其逆仍然成立。这条规则作用于基础语言的符号串，因此也能达到缩写所隐藏的出现，并且可作用于或非的两个运算对象中的任一个；它的直接推论包括

(φ↓ψ)⊣⊢(¬¬φ↓ψ),(φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi), \qquad (\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)

一般地，χ⊣⊢χ′\chi \dashv\vdash \chi'，只要 χ′\chi' 由 χ\chi 经双重否定替换而得。这种形式的等价行以“双否替换”为依据，不带行号，正如“双重否定”行或“逆否”行引用一个已经证明的等价式那样。 和那里一样，已经证明的定理可以写成推演中的一行，因为它自己的推演可以插入到那个位置；并且，由那一课的“从结果到规则”引理，每种技巧也可以在任何前提集 Γ\Gamma 下作为规则使用，引用时写出它所作用的行号，如 逆否(i)(i) 或 假言三段论(i,j)(i, j)。在关于推演的推演中，“前提”表示所证规则的一个假设。

在关于命题逻辑的语言的一课中确定的正式缩写，是联结词仅有的定义：

¬φ:=(φ↓φ),(φ∨ψ):=¬(φ↓ψ),(φ∧ψ):=¬(¬φ∨¬ψ)\neg\varphi := (\varphi \downarrow \varphi), \qquad (\varphi \vee \psi) := \neg(\varphi \downarrow \psi), \qquad (\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)
(φ→ψ):=(¬φ∨ψ),(φ↔ψ):=((φ→ψ)∧(ψ→φ)),(φ⊻ψ):=¬(φ↔ψ)(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi), \qquad (\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)), \qquad (\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)

以“定义”为依据的行什么也推不出：它用另一个名字写出同一个公式，注释则说明展开或收回的是哪一个缩写（“定义 →\rightarrow”、“定义 ∨\vee”）。不妨回顾在关于自然语言的形式化的一课中观察到的现象：同一个公式可以有好几个名字，因此一个合取作为符号串也是一个析取。例如，以 ¬φ\neg\varphi 代替 φ\varphi 展开蕴涵，就得到

(¬φ→ψ)=(¬¬φ∨ψ)=¬(¬¬φ↓ψ)(\neg\varphi \rightarrow \psi) = (\neg\neg\varphi \vee \psi) = \neg(\neg\neg\varphi \downarrow \psi)

而出现在 φ\varphi 前面、被缩写所隐藏的双重否定，正是双重否定替换规则将在下文处处出场的原因。

作为等式的可证等价

本课的证明几乎都是等价链：φ1⊣⊢φ2\varphi_{1} \dashv\vdash \varphi_{2}、φ2⊣⊢φ3\varphi_{2} \dashv\vdash \varphi_{3}，依此类推。要从一条链得出 φ1⊣⊢φn\varphi_{1} \dashv\vdash \varphi_{n}，可证等价就必须表现得像等式，而这正是关于形式演绎系统的一课中关于可证等价性质的命题所确立的：这个关系是自反的（φ⊣⊢φ\varphi \dashv\vdash \varphi）、对称的（若 φ⊣⊢ψ\varphi \dashv\vdash \psi，则 ψ⊣⊢φ\psi \dashv\vdash \varphi）和传递的（若 φ⊣⊢ψ\varphi \dashv\vdash \psi 且 ψ⊣⊢χ\psi \dashv\vdash \chi，则 φ⊣⊢χ\varphi \dashv\vdash \chi），并且两个可证等价的公式作为结论可以互换（若 Γ⊢φ\Gamma \vdash \varphi 且 φ⊣⊢φ′\varphi \dashv\vdash \varphi'，则 Γ⊢φ′\Gamma \vdash \varphi'，对每个公式集 Γ\Gamma 都成立）。值得回顾后两条是怎样证明的，因为整节课都建立在它们之上：由 {φ}⊢φ′\{\varphi\} \vdash \varphi'，借助单调性，过渡到 Γ∪{φ}⊢φ′\Gamma \cup \{\varphi\} \vdash \varphi'；再由它和 Γ⊢φ\Gamma \vdash \varphi，借助切割规则，得到 Γ⊢φ′\Gamma \vdash \varphi'；传递性则是在一个方向上取 Γ={φ}\Gamma = \{\varphi\}、在另一个方向上取 Γ={χ}\Gamma = \{\chi\} 来应用这一点而得的。

此后，把一条等价链合并成一个等价式的那一步以“切割”为依据，因为它就是那个命题的工具。然而，每个环节 φi⊣⊢φi+1\varphi_{i} \dashv\vdash \varphi_{i+1} 都包含两个推演，去的和回的；由此可知，一条等价链同时证明其结论的两个方向，没有什么“留作练习”。