跳至内容
Topos Uranos

摘要

本课开启课程的第二个单元,这一单元专讲演绎。本课介绍单元的五节课以及把它们串联起来的线索,从形式演绎系统的定义,直到德摩根律与分配律;把本单元放到课程的路线中,位于已经建成的语言与随后到来的语义学和元理论之间,并预先说明后两者将对它说些什么;说明为什么选择公理系统,这个系统分两个阶段建造(卢卡西维茨系统,有三个公理模式和分离规则;本课程的系统,在它之上增加双重否定替换规则),并解释为什么需要这第二条规则、为什么把它作为公设而不是加以证明;用一个简短的推演展示一个初等的推理隐藏着多少工作;指明从上一单元所取用的东西,即唯一可读性、归纳法(自然数上的强归纳法与结构归纳法)和缩写的展开;最后给出学习本单元的建议。

学习目标

  1. 描述本单元五节课的先后次序,并说明每一节课用到前一节课的哪些结果。
  2. 把演绎放到课程的路线中,区分可推演性 Γ⊢φ\Gamma \vdash \varphi 与语义后承 Γ⊨φ\Gamma \models \varphi,并说明可靠性与完备性将断言什么。
  3. 从三个模式在或非中能看到什么、不能看到什么出发,说明为什么本课程的系统要在卢卡西维茨系统之上增加第二条初始规则,即双重否定替换。
  4. 按编号行阅读一个简短的推演,区分公式的推演与关于推演的推演,认出本单元从上一单元取用的东西,并从入门测评出发安排本单元的学习。

入门测评

在学习本单元之前,先测一测自己的起点是有益的。这份测评是自我测评:不计分,唯一的目的是为学习指引方向。它的十三道题分为两类。前三道涉及本单元假定已从上一单元学到的东西:唯一可读性、强归纳法和缩写的展开;答错其中任何一道的人,在继续之前应当复习题目所指出的那节课。其余十道按顺序对应本单元的五节课:第一课三道,第二课三道,第三课两道,第四课一道,第五课一道。从未学过演绎系统的人不必指望答对,这也无关紧要:每个答案,无论对错,都会解释要点,并指出讲解这一要点的那节课。同样的技能会在单元末尾的总结课中再次测量。

入门测评

开始本单元之前,先测一测你的起点。这是一次简短的自我测评:不计分,结果只保存在你的浏览器中。

  1. 第 1 题来自前面的单元符号串 ∙∙∘∙∘∘∙∘∙\sigI\sigI\sigO\sigI\sigO\sigO\sigI\sigO\sigI 是一个复合公式,形如 ∙φψ\sigI\varphi\psi。它的成分 φ\varphi 和 ψ\psi 分别是什么?

  2. 第 2 题来自前面的单元在用强归纳法证明每个自然数 nn 都具有性质 P(n)P(n) 时,证明 P(n)P(n) 的时候可以假设什么?

  3. 第 3 题来自前面的单元按照本课程的正式缩写,(φ→ψ)(\varphi \rightarrow \psi) 用或非和否定写出来,是哪个公式?

  4. 第 4 题模式 A1 是 (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi))。公式 (v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3})) 是 A1 的实例吗?

  5. 第 5 题在一个推演中已经有行 ψ\psi 和 (φ→ψ)(\varphi \rightarrow \psi),其中 φ\varphi 和 ψ\psi 是不同的公式。对这两行应用分离规则,可以写出哪个公式?

  6. 第 6 题已知 {φ}⊢ψ\{\varphi\} \vdash \psi,即存在一个 ψ\psi 的推演,其唯一的前提是 φ\varphi。那么演绎定理断言什么?

  7. 第 7 题不添加其他前提,由集合 {(φ→ψ),(ψ→χ)}\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} 可推出什么?

  8. 第 8 题双重否定替换规则(双否替换)在一行中只改变子公式的一次出现,并且作用于基础语言的符号串。子公式 ¬v1\neg v_{1} 在 (v1→v2)(v_{1} \rightarrow v_{2}) 所表示的符号串中出现几次?

  9. 第 9 题由 (¬φ→ψ)(\neg\varphi \rightarrow \psi) 通过逆否律,不添加双重否定,得到哪个公式?

  10. 第 10 题(φ∨ψ)(\varphi \vee \psi) 与 (¬φ→ψ)(\neg\varphi \rightarrow \psi) 表示同一个公式吗?

  11. 第 11 题已知 φ⊣⊢φ′\varphi \dashv\vdash \varphi',即二者可以互相推出。是什么保证了也有 ¬φ⊣⊢¬φ′\neg\varphi \dashv\vdash \neg\varphi'?

  12. 第 12 题由前提集 Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} 推出了一个公式 χ\chi 及其否定 ¬χ\neg\chi。可以得出什么结论?

  13. 第 13 题蕴涵的否定 ¬(φ→ψ)\neg(\varphi \rightarrow \psi) 等价于哪个公式?