跳至内容
Topos Uranos

数理逻辑 I:课程计划

摘要

本课是课程的开篇单元,阐述课程完整的学习计划。它说明课程的宗旨、面向的对象、预设的少量知识以及通往的课程;陈述课程提出的七个总体学习目标;解释塑造本课程所研究系统的三项决定;描述课程的六个单元及其所含各课;估算课程所需的总学习量、各单元的分配、建议的学习节奏及其折合的可转换学分;最后说明各课的构成方式,并就如何学习本课程提出建议。

学习目标

  1. 描述课程各单元的顺序,并说明每个单元为后续单元提供了什么。
  2. 陈述课程的总体学习目标,并认出哪些单元服务于每个目标。
  3. 解释确定本课程系统的各项决定:圆圈与圆盘的语言、第二条初始规则,以及紧致性与强完备性的先后顺序。
  4. 根据各单元的估计学时,计算整门课程或其一部分所需的学习量,并据此规划个人的学习节奏。

宗旨

所有数学课程都要求证明,所有哲学课程都要求论证;然而,没有一门课程把推理本身作为对象,而且都把“结论从前提推出”是什么意思视为不言自明。本课程正是以这个问题为主题。它的宗旨是为最简单的逻辑语言构建第一个以推理为对象的完整数学理论,并把它的四个部分都摆在眼前:一种语言,其公式可以被识别并无歧义地读出;一个演算,它产生推演而不顾及符号的意义;一种意义,它在其变元的每个赋值下给每个公式指派真值;以及演算与意义相互吻合的证明。

若是如此,本课程就不是一套操作符号的规则汇编,而是一个以完备性定理为中心结果的理论,前面的一切都在为它作准备。对公式集 Γ\Gamma 和公式 φ\varphi,可推演性 Γ⊢φ\Gamma \vdash \varphi 说的是:存在一个由公理和规则构造、以 φ\varphi 结尾的有穷公式序列;语义后承 Γ⊨φ\Gamma \models \varphi 说的是:每个使 Γ\Gamma 中公式为真的赋值都使 φ\varphi 为真。这两种关系出自相反的观念,一个是语法的、存在的,另一个是语义的、全称的;然而本课程证明了 Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi。由此可知,任何关于从某些前提推出什么的问题,都可以从较容易的一侧来回答:给出一个推演,逐行检查一张表,或者像最后一节内容课所教的那样,用归结来反驳。

对象与预备知识

本课程面向开始学习数学、计算机科学或哲学的人,也面向在任何学习阶段想确切知道什么是证明、以及为什么可以信赖证明的人:刚进入大学数学、在证明上屡屡受挫的学生,需要电路、程序和可满足性问题之逻辑的计算机科学学生,以及想从论证的逻辑走向其理论的哲学学生。

这是一门 1 级课程,没有先修要求,内容自成一体。它不假定学过逻辑,不假定懂集合论,也不假定曾经证明过定理。它所用到的集合知识(属于、包含、并、公式集)、函数知识(赋值是从变元到 {0,1}\{0, 1\} 的函数)、符号串知识和归纳法,都在需要的地方讲授:集合与符号串在第 1 单元关于语言的那一课中讲,归纳法在下一课中、使用之前讲。它只假定两件事:仔细阅读,因为在形式语言中多一个或少一个符号就会改变符号串;以及自然数的初等算术,在本课程中,和在本站其他地方一样,自然数从 11 开始。

通往何处

由上可知本课程在本站中的位置。它没有先修要求,是数学、计算机科学和哲学三个学习方案的目标课程,因为在这三者中,推理既是工具又是对象。它有三门互补的课程,可以在它之前、与它并行或在它之后学习,顺序不限。亚里士多德逻辑研究词项逻辑和三段论,三段论的有效性取决于“所有”和“有的”这类本课程排除在外的词,并展示演算是从哪一传统中发展而来的。代数与几何 I从皮亚诺公理出发建起一座演绎大厦,并在数上实际运用本课程作为对象来研究的公理化方法和归纳法;它的学习计划建议先学本课程或与之并行。最后,C++ 程序设计 I把这里的理论付诸实践:判定一个符号串是否合式、逐行检查真值表、计算范式或寻找反驳,都是可以写成程序的过程。

然而,本课程留下一个表达力的问题:它的语言不能说“所有”或“有的”,用汉语表述的论证在形式化时,从第 1 单元起就失去了量词。因此,它预定的后续课程是数理逻辑 II,专讲谓词逻辑,它将以量词和取值于对象的变元走同一条路:它将保持可靠性、完备性和紧致性,所用的方法本课程已有预示,但在那里语义后承将不再是可判定的。

总体学习目标

下列目标描述完成本课程的人应当能做什么。每个目标都表述为可观察的表现,以便能用具体的任务来检验;每节内容课也各自声明本课的目标,它们服务于一个或几个总体目标,而结课课则显示每个目标在哪些单元和哪些课中得到训练。七个目标都编了号,以便引用。

  1. 目标 1. 区分对象语言与元语言,并按形成规则判定一个符号串是否为公式。
  2. 目标 2. 将自然语言的陈述句和论证形式化,指出形式化保留了什么、失去了什么。
  3. 目标 3. 在本课程的系统(卢卡西维茨公理、modus ponens 和双重否定替换)中构造推演,综合运用公理、初始规则和派生规则。
  4. 目标 4. 用对自然数、对公式复杂度和对推演长度的归纳法证明元定理。
  5. 目标 5. 用真值表和等价式判定有效性、可满足性、语义后承和语义等价。
  6. 目标 6. 把公式变换为范式,并用范式表示真值函数和电路。
  7. 目标 7. 解释并运用可靠性、完备性和紧致性,并用归结判定不可满足性。

目标 3 和目标 7 各有自己的单元,即演绎和元理论;目标 5 和目标 6 分享语义单元,前者在其前半部分,后者在后半部分。目标 2 有一节专门的课,即形式化那一课,此后每当问题用文字提出时都会得到练习。目标 1 和目标 4 则是贯穿性的:在语言之内说的话与关于语言说的话之间的区别贯穿四个单元,而归纳法是本课程所有重要证明的形式,从公式的唯一可读性到系统的可靠性和卡尔马引理。由此可知,它们的达成不能归于某一节课,而应在整个课程中逐步培养。

本课程的系统及其决定

命题逻辑课程可以有多种构建方式,常见的教材在语言、初始联结词和演绎系统上各不相同。本课程作出三项决定,最好从一开始就了解,因为它们解释了乍看之下可能显得奇怪的地方。

圆圈与圆盘的语言

本课程的语言的字母表只有两个符号:圆圈 ∘\sigO 和圆盘 ∙\sigI。第 nn 个变元是 nn 个圆圈后接一个圆盘的符号串 vn=∘n∙v_{n} = \sigO^{n}\sigI,因此 v1=∘∙v_{1} = \sigO\sigI,v2=∘∘∙v_{2} = \sigO\sigO\sigI;形成规则只有一条:若 φ\varphi 和 ψ\psi 是公式,则 ∙φψ\sigI\varphi\psi 也是公式,它缩写为 (φ↓ψ)(\varphi \downarrow \psi),读作“既非 φ\varphi 也非 ψ\psi”。因此,或非 ↓\downarrow 是唯一的初始联结词,其余联结词都是只定义一次的缩写:¬φ\neg\varphi 是 (φ↓φ)(\varphi \downarrow \varphi),析取 (φ∨ψ)(\varphi \vee \psi) 是 ¬(φ↓ψ)\neg(\varphi \downarrow \psi),再由它们定义合取、蕴涵、双条件和不相容析取。它们的任何其他写法都是需要证明的定理,而不是定义。

这一选择有一个代价,即可读性,本课程在元语言中付出这个代价:没有人天天书写圆圈和圆盘的符号串,而是书写它们的缩写名称,这些名称随时都可以展开为它们所指的符号串。然而,这个代价得到了多倍的回报。两个符号就足以表示无穷多个变元,因此每个公式都是二元字母表上的有穷符号串。联结词写在其参数之前,所以不需要括号:唯一可读性由一个权重论证来证明,它给每个变元指派 +1+1,给每个联结圆盘指派 −1-1。又因为每个复合公式都是一个或非,每个对复杂度的归纳证明只有一种复合情形,这使后续各单元的所有证明都得以缩短。一个联结词就足以表达任何其他联结词,这一点不是假定的:语义单元会证明它。

第二条初始规则

演绎系统以扬·卢卡西维茨的系统为出发点:三个用否定和蕴涵写成的公理模式,以及作为唯一规则的 modus ponens。这些模式是为以否定和蕴涵为初始联结词的语言而制定的;在圆圈与圆盘的语言中,像 (v1↓v2)(v_{1} \downarrow v_{2}) 这样的公式既不是否定也不是蕴涵,对公理来说是不透明的。演绎单元的第一课借助一种标记证明了卢卡西维茨系统推演不出 ((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}):所有公理都带有这种标记,modus ponens 保持它,而这个公式没有它。

若是如此,系统就必须补充,而自然的补救办法似乎是证明双重否定 φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi,第二课从三个模式推演出了它。标记表明这还不够:双重否定的定理保持这种标记,然而即使有了它们,也不能在一个或非内部把 v1v_{1} 换成 ¬¬v1\neg\neg v_{1}。因此,第二课在证明双重否定之后,增加了第二条初始规则,即双重否定替换:由公式 χ\chi 可以推出把其中子公式 θ\theta 的一次出现替换为 ¬¬θ\neg\neg\theta、或把 ¬¬θ\neg\neg\theta 的一次出现替换为 θ\theta 后所得的公式。于是,本课程的系统由卢卡西维茨的三个模式、modus ponens 和这条规则组成。

其他针对或非的系统用量身定制的公理模式达到同样的效果。本课程选择一条规则,理由有二:它比 modus ponens 还要简单,因为它只取一行、只改变一处出现;它也毫无人为之处,因为它表达的正是双重否定已经说出的内容,即 θ\theta 与 ¬¬θ\neg\neg\theta 可以互换,只是推广到公式中的任何位置。此外,它是可靠的,因为它保持每一行的真值;它也保持演绎定理,只是在证明中多了一种情形。有了它就足以推演出一切应当推演出的东西,这正是最后一个单元的完备性定理。

紧致性先于强完备性

完备性有三个层次:弱完备性说每个重言式都是定理;有穷完备性说有穷前提集的每个语义后承都可以从它推演出来;强完备性说同样的事对任意集合,包括无穷集合,也成立。本课程的方法即卡尔马引理,处理的是一个公式的有穷多个变元和有穷的前提,因此能达到前两个层次,而达不到第三个。要达到第三个层次,只需当 Γ⊨φ\Gamma \models \varphi 时,有某个有穷部分 Γ0\Gamma_{0},取自 Γ\Gamma,已经满足 Γ0⊨φ\Gamma_{0} \models \varphi;而这恰恰就是紧致性定理所断言的。

许多教材先用别的方法证明强完备性,再由它推出紧致性。而在本课程中,强完备性正是所要寻求的,由它得出紧致性将是循环论证。因此顺序颠倒过来:关于紧致性的那一课在语义内部证明它,不提及任何推演,逐个固定 v1,v2,…v_{1}, v_{2}, \ldots 的值,然后才用三行得出强完备性,即 Γ⊨φ⇒Γ⊢φ\Gamma \models \varphi \Rightarrow \Gamma \vdash \varphi 对每个集合 Γ\Gamma 都成立。

内容

本课程分为六个单元:本介绍、四个内容单元和一个结课单元。每个内容单元以一节导言课开始,介绍单元中的各课、它在课程中的位置、它预设的知识和它要解决的问题,并以入门测评开头;以一节总结课结束,总结课重建单元的演绎链条,把它与课程的其余部分联系起来,在结业测评中重复入门测评所考查的技能,并提出六道难度高于各课习题的挑战题。

第 0 单元 课程介绍

它由本课组成,本课确定课程的宗旨、总体目标、各项决定、内容、学习量和设计。

第 1 单元 语言

它的目标是构建本课程所研究的语言,证明每个公式只有一种读法,并把它与用汉语表述的论证联系起来。

  1. 语言:导言。
  2. 什么是数理逻辑:有效性与真理的对照、反例、悖论,以及对象语言与元语言的区分。
  3. 命题逻辑的语言:集合与符号串、圆圈与圆盘的语言、它的形成规则和缩写。
  4. 自然数上与公式上的归纳法:简单归纳、强归纳和结构归纳,权重引理,唯一可读性,以及递归定义。
  5. 自然语言的形式化:词典,陈述句和论证的翻译,以及实质蕴涵所失去的东西。
  6. 语言:总结与挑战。

第 2 单元 演绎

它的目标是给语言配上一个演算,即本课程的系统,并在其中把数学使用却不加命名的各种推理形式各推演一次。

  1. 演绎:导言。
  2. 形式演绎系统:卢卡西维茨系统、带前提的推演、演绎定理,以及显示其局限的标记。
  3. 四种推演技巧:假言三段论、前提交换、双重否定、换质位和双重否定替换。
  4. 联结词的对称性:或非基本引理、等价替换、联结词的替代形式及其五种对称性。
  5. 经典逻辑的技巧:每个联结词的规则、排中律、分情形证明和归谬法,均带前提。
  6. 德摩根律与分配律:它们双向的证明,以及在其他公式内部的等价替换。
  7. 演绎:总结与挑战。

第 3 单元 语义

它的目标是赋予公式意义,用意义判定有效性和语义后承,并把每个公式化归为范式。

  1. 语义学:导言。
  2. 命题逻辑的语义学:赋值及其递归扩张、一致引理、真值表、有效性和可满足性。
  3. 语义后承与语义等价:从集合出发的语义后承、语义演绎定理、替换和统一代入。
  4. 广义德摩根律与分配律:nn 项的合取与析取及其定律,用归纳法证明。
  5. 功能完全性:每个真值函数都有一个公式,或非单独就够用,以及联结词完全集。
  6. 范式:文字、子句、析取范式与合取范式、它们的对偶性和存在性。
  7. 范式算法及其应用:一个正确且终止的算法,以及开关电路的设计与化简。
  8. 语义学:总结与挑战。

第 4 单元 元理论

它的目标是证明推演与语义后承相互吻合,先对有穷前提,再对任意前提,并提供判定它们的第三种方式。

  1. 元理论:导言。
  2. 可靠性与完备性:对行数归纳证明可靠性、一致性、卡尔马引理,以及弱完备性和有穷完备性。
  3. 紧致性定理:它的语义证明、它的等价形式、由它得出的强完备性,以及它的组合应用。
  4. 归结法:子句形式、归结规则、它的可靠性与反驳完备性,以及它的代价。
  5. 元理论:总结与挑战。

第 5 单元 课程总结

它由数理逻辑 I:最终回顾一课组成,这一课回顾七个总体目标,用一幅图显示每个目标在哪些单元和哪些课中得到训练,按目标汇集各次结业测评的第一次作答,并指出学习从这里通往何处。

学习量与学分

一门课程的学习量不以讲授学时来衡量,异步课程中并没有讲授学时,而以学习者的全部工作来衡量:阅读、跟随证明和推演、解题和复习。估算在本站所有课程中采用同一方法:按每分钟一百词计算每节课正文的阅读时间,每个公式算作一个词,每道例题二十分钟,每道练习题三十五分钟,每道挑战题四十五分钟,每次入门测评或结业测评十二分钟,再加上十分之一的复习余量。

结果

本课程各课共含 9090 道例题、9090 道练习题和 2424 道挑战题,另有八次单元测评。各单元估计的学习量,取整到小时,如下:

  • 第 0 单元,课程介绍:不到 11 小时。
  • 第 1 单元,语言:3030 小时。
  • 第 2 单元,演绎:3636 小时。
  • 第 3 单元,语义:4343 小时。
  • 第 4 单元,元理论:2525 小时。
  • 第 5 单元,课程总结:不到 11 小时。

总计约 137137 小时的学习量。这个数字应按其本来面目理解:它是对一位学习全部证明、解答全部习题和挑战题的学习者的估计。已经学过逻辑的人,或只做练习题而不做挑战题的人,所需时间会少得多;从未证明过定理的人可能需要更多,尤其是在演绎和语义两个单元,这两个单元也是篇幅最长的。

然而,这个数字是名义上的:它决定课程的学分,并假定以恒定速度阅读、每道挑战题用四分之三小时。在用真实学生测量之前,最好给它配上一个现实的区间。如果阅读速度只有假定的一半,就像用纸笔抄写每个推演、用手拆分每个圆圈与圆盘的符号串时那样,而每道挑战题需要七十五分钟而非四十五分钟,同一方法会得出约 174174 小时。因此,可预期的学习量介于约 137137 小时与约 174174 小时之间。上限是一个审慎的界限,而不是测量结果;待了解学习者实际所用的时间后,区间将予以修正,在此之前学分按名义数字计算。

建议节奏

为了给各种节奏命名,本计划采用与本站其他计划相同的标准:全日制学习相当于一个 6060 学分的学年,约 16501650 小时,分布在约四十周内,即每周约 4040 小时;半日制为其一半,即每周约 2020 小时。由此得出建议的节奏:一个十六周的学期,每周学习约 88 或 99 小时,略多于全日制的五分之一;按现实区间计算,每周 99 至 1111 小时。这个学期可以与代数与几何 I共享,当推演已是熟悉的对象时,那门课的证明读起来会更顺畅。

强化节奏为每周约 2020 小时,即半日制,七周即可完成本课程。较宽松的节奏为每周约 44 或 55 小时,需要两个学期,两学期的分量几乎各占一半:第 0 至第 2 单元,即语言和演绎,约占 6767 小时;第 3 至第 5 单元,即语义、元理论和课程总结,约占 6969 小时。

折合可转换学分

可转换学分体系以课程要求修读者完成的全部工作来衡量课程,而不是以课堂面授学时来衡量,目的是使在一所院校完成的学业能在另一所院校得到承认。欧洲学分转换与累积体系由欧洲各大学在博洛尼亚宣言之后采用,规定全日制学年为 6060 学分,每学分对应 2525 至 3030 小时的学习量。智利可转换学分体系由智利各大学按类似的设计采用,同样规定学年为 6060 学分,每学分对应 2424 至 3131 小时的学习量。

然而,把估计的 137137 小时分别除以各区间的两端,本课程大约相当于 55 个欧洲学分(4.6 至 5.5),以及 44 至 66 个智利可转换学分(4.4 至 5.7)。以两个区间的中间值,即每学分 27.5 小时为参照,两种体系得到同一个数字 4.98,取整为 5。对欧洲学分而言,学分数 CC 的范围如下:

(13730)≤C≤(13725)\left( \frac{137}{30} \right) \leq C \leq \left( \frac{137}{25} \right)

因此,建议为本课程分配 55 个欧洲学分和 55 个智利可转换学分,即全日制学年的十二分之一,略少于一门普通的六学分一学期课程。

课程设计

学习形式

本课程是异步的、在线的、自定进度的:没有日期、直播课和截止期限,每个学生按照自己的基础和时间所允许的速度前进。课程以本站的十四种语言提供,各语言中的逻辑完全相同:公式、推演和证明的步骤在每个版本中都一样,只翻译正文。各课都说明最好先学哪些其他课,因此推荐的顺序是明确的。

一节课的结构

所有内容课都采用相同的结构。它们以摘要和一份本课学习目标的列表开始,这些目标表述为可观察的表现。接下来是理论,包括定义、精确陈述的结果及其证明,以及例子。证明以步骤播放器的形式呈现:每一步写出一行,突出显示发生变化的部分,当它依据先前的结果时,就回到那个结果。系统中的推演写成带编号的行,每行的依据写在右侧(一条公理、一个前提、modus ponens 及其所用的行,或一条派生规则),推进时被引用的行会突出显示。每课最后是五道例题,附有逐步解答,以及五道练习题,每道练习题都有一个折叠的提示,之后是最终答案;证明类的练习题还在答案之后附有一份折叠的详细解答,最好在写出自己的解答之后再打开。

此外,每一课都可以通过本站的朗读器听读,它用文字读出公式中的符号,包括圆圈、圆盘以及推演和语义后承的符号。

评估

本课程不评分:其评估是形成性的,以自我评估为基础。练习题用来检验各课目标的达成情况,挑战题用来检验各单元目标的达成情况。此外还有单元测评:入门测评位于导言的开头,用十一至十五道题测量起点,因为它在单元的题目之外,还加了几道关于单元所预设知识的题;结业测评位于总结课中、挑战题之前,用十二道题测量所达成的水平,并与入门测评作比较。两者都在浏览器中直接批改,每个答案都附有解释,并指引应当复习的那一课;结果只保存在作答者的浏览器中,最终回顾把每次结业测评的第一次作答汇集成按总体目标划分的概况。

如何学习本课程

本课程是按顺序学习而设计的。每个单元都以前面的单元为前提:演绎用第一个单元的语言来书写,语义赋予它的公式以值,元理论则比较第二个单元和第三个单元;跳过一节课,迟早都得回头再学。

在每一课中,最好先读摘要和目标;然后用纸笔学习理论,抄写圆圈与圆盘的符号串,分开其中的变元和圆盘,并在播放器写出推演的每一行之前先预想出来;在看例题的解答之前先自己尝试,独立解答练习题,只有在尝试已经穷尽时才打开提示。一道在尝试之前就查看了答案的题,不算解出,只算读过。

最后,应当始终分清每个断言属于哪个层次:它是在语言之内说了些什么,如一个公式,还是关于语言说了些什么,如 Γ⊢φ\Gamma \vdash \varphi 或 Γ⊨φ\Gamma \models \varphi。这一区分是本课程的第一个目标,也正是理解其中心结果的关键,而这个中心结果只能在元语言中陈述。