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

形式演绎系统

摘要

本课把上一单元的语言变成证明的工具。它定义什么是形式演绎系统（一种语言、若干公理模式和若干推理规则），并介绍本课程所用的两个系统中的第一个，即卢卡西维茨系统：三个公理模式，以分离规则（modus ponens）为唯一的规则。它精确定义从前提集出发的推演、定理以及关系 Γ⊢φ\Gamma \vdash \varphi，用五行推演出 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)，并证明推演的结构性质：自反性、单调性、推演之间的分离规则、切割和有穷性。接着，它通过对行数的强归纳法证明演绎定理及其逆，二者使我们能够用关于推演的推演来进行推理；并定义可证等价。最后，它不借助真值，确定这个系统在以或非为唯一联结词的语言中的界限：一种取值为 00 和 11、对公式递归计算的标记，为卢卡西维茨公理和分离规则所保持，它证明某些本应可推演的公式不可推演，甚至不能从 (v1↓v2)(v_{1} \downarrow v_{2}) 过渡到 (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2})。由此可知需要第二条规则，即双重否定替换，下一课用它来完成这个系统。

学习目标

  1. 识别公理模式 A1、A2 和 A3 的实例，并判定一个公式序列是否为从某个前提集出发的推演。
  2. 在卢卡西维茨系统中用公理、前提和分离规则构造推演，并用自反性、单调性、切割、演绎定理及其逆构造关于推演的推演。
  3. 通过对行数的强归纳法证明推演的结构性质和演绎定理。
  4. 建立可证等价，并运用可证等价是自反的、对称的和传递的这一事实。
  5. 借助一种为公理和分离规则所保持的标记证明某个公式不可推演，并用它解释卢卡西维茨系统在只有一个联结词的语言中的界限，以及为什么需要第二条规则。

什么是形式演绎系统

上一单元构造了一种语言：它确定了哪些由圆圈与圆盘组成的符号串是公式，仅此而已。然而，一种语言本身既不断言什么，也不证明什么；要证明，还需要一个出发点和一种前进的方式。因此，一个形式演绎系统由三个部分组成：确定公式的形式语言；一个公理集，即不经证明而接受的公式；以及一个推理规则集，规定可以根据已经写出的其他公式写出哪个公式。关键在于这三者都是纯粹语法的：要检查一个公式是否为公理，或者一条规则是否被正确地应用，只需看符号串本身，而不必问它们意味着什么。若是如此，形式系统中的证明就可以机械地、逐个符号地加以检查，而它的全部价值就在于这种可能性。

应当从一开始就指出，这里的公理不是像这个词的古老用法那样的“不证自明的真理”，而是被选作出发点的公式。这种选择是否恰当（公理是否在语义学将要澄清的某种意义上为真，以及它们是否足以推演出一切应当推演出的东西）是一个关于系统的问题，要用关于系统的定理而不是用直觉来回答：关于元理论的单元回答这个问题，而本课最后一节表明这个问题并非多余。

公理模式与实例

命题逻辑的系统不逐条陈述它们的公理，因为公理有无穷多条，而是通过模式来陈述：用元变元写成的元语言表达式，例如 (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi))。模式不是公式；它是一个模子。模式的一个实例是对每个元变元统一地代入某个公式后得到的公式：同一个元变元的所有出现处都代入同一个公式，而不同的元变元可以得到同一个公式，也可以得到不同的公式。

例题一个模式的实例

取 φ:=v1\varphi := v_{1} 和 ψ:=¬v2\psi := \neg v_{2}，模式 (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)) 给出实例 (v1→(¬v2→v1))(v_{1} \rightarrow (\neg v_{2} \rightarrow v_{1}))；取 φ:=(v1↓v2)\varphi := (v_{1} \downarrow v_{2}) 和 ψ:=(v1↓v2)\psi := (v_{1} \downarrow v_{2})，它给出 ((v1↓v2)→((v1↓v2)→(v1↓v2)))((v_{1} \downarrow v_{2}) \rightarrow ((v_{1} \downarrow v_{2}) \rightarrow (v_{1} \downarrow v_{2})))，因为没有什么妨碍两个元变元得到同一个公式。反之，(v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3})) 不是这个模式的实例：φ\varphi 的第一次出现和最后一次出现将得到不同的公式，代入就不是统一的。每个实例在展开缩写之后都是一个由圆圈与圆盘组成的符号串；而模式只存在于元语言之中。