构造性逻辑讲义

这基本上是对于Frank Pfenning的构造性逻辑课程的讲义的翻译.

第1章 何为(构造性)逻辑?

第1.1节 引论

根据维基百科, 逻辑学是研究有效推理和论证的学科. 从这个定义的广度可以立即看出, 逻辑学在哲学和数学领域构成了一个重要的研究方向. 逻辑工具和方法在计算机硬件和软件的设计, 描述和验证中也发挥着至关重要的作用. 本课程将重点关注逻辑学在计算机科学中的这些应用. 为了正确理解逻辑学及其与计算机科学的相关性, 我们需要大量借鉴哲学和数学中更为古老的逻辑学传统. 我们将在这些讲义中讨论逻辑学的一些相关历史, 并提供进一步阅读的指引. 在这次的介绍里, 我们只是给出了一个简要的引论. 至于深入的一般性阅读材料, 我们推荐Troelstra and van Dalen [1988]的引论部分, 以及斯坦福哲学百科全书 (Stanford Encyclopedia of Philosophy) 中的直觉主义逻辑和数学哲学中的直觉主义词条.

第1.2节 Russell悖论

在19世纪末期和20世纪初期, 数学处于一种可以称之为基础危机的状态, 这场危机是由日益抽象的数学所引发的. 逻辑悖论的发现加深了这场危机. Russell悖论 (发现于1901年) 尤其沉重打击了Frege试图发展一种可以用来进行所有数学推理的通用逻辑的努力 [Frege, 1879]. 以现代语言, Russell悖论或许最容易通过集合来理解. Russell将$R$定义为由所有不包含自身的集合构成的集合.$$R=\{x|x\notin x\}$$那么, $R$是$R$的一个元素吗? 如果是的话, 那么根据$R$的定义必然有$R\notin R$. 如果不是的话, 那么又一次根据$R$的定义必然有$R\in R$. 于是, 我们发现$$R\in R\leftrightarrow R\notin R$$因而我们有了一个悖论性的命题, 这个命题为真当且仅当其为假. Russell的解决方案是引入类型以使得集合$R$因为一个集合不能是其自身的元素而不能被构造出来. Whitehead和Russell的分歧类型论 (ramified type theory) Whitehead and Russell [1910–13], 之后由Church [1940]演化成为他的简单类型论, 解决了这个特定的问题. {译注: 从历史上来看, 英年早逝的Frank Ramsey也对于简单类型论有重要的贡献.} 其他的解决方案存在于集合论之中.

第1.3节 直觉主义

除了对于某个特定的系统中的某个问题进行提问, 我们还可以进行更为一般的提问: 当我们做数学的时候, 我们是在做什么呢? 从柏拉图主义的角度来看, 诸如整数, 有理数, 或者实数这样的数学对象具有客观的存在, 而数学家只是试图理解这种真实性 (reality). Brouwer [1907], 作为直觉主义的创立者, 转而将数学考虑为施行心智中的构造. 由此数学更多与构造和知识有关, 而非(一些难以捉摸的)绝对真性 (truth). 从Brouwer的观念来看, 仅当我们知道$A$为真或者$B$为真的时候才能断言$A\vee B$. 特别地, 在一般情况下我们不能必然断言排中律$A\vee \neg A$, 因为我们可能既不知道$A$的一个证明, 也不知道$A$的一个反驳. 一个例子是哥德巴赫猜想 (让我们称其为$G$), 即每个大于二的偶数都是两个素数之和. 既然哥德巴赫猜想已经悬而未决将近三百年了, 我们并不知道其一个证明, 也不知道其一个反例. 因此, 我们无法言称$G\vee \neg G$为真. 但是, 我们也不能排除之后或许我们就可以知道的可能性. {译注: 这句话让人想到Kripke语义.}

我们将不会纠结于Brouwer关于直觉主义的特定形式的细节, 但是我们可以从中提取出以下直觉主义的真性定义 (这个定义有些刻意地非形式化) [Troelstra and van Dalen, 1988]:

• 一个对于$A\wedge B$的证明是通过呈现一个对于$A$的证明和一个对于$B$的证明而给出的.
• 一个对于$A\vee B$的证明是通过呈现一个对于$A$的证明或一个对于$B$的证明而给出的.
• 一个对于$A\supset B$的证明是一个构造, 其允许我们将一个对于$A$的证明转换为一个对于$B$的证明.
• 不存在对于$\perp$的证明. 另外, 一个对于$\neg A$的证明是一个构造, 其将一个(假想的)对于$A$的证明转换为一个矛盾.
• 一个对于$\exists x.A$的证明是通过提供一个量化的论域里的见证者 (witness) $d$和一个对于$[d/x]A$的证明给出的.
• 一个对于$\forall x.A$的证明是一个构造, 其取量化的论域里的任意一个元素$d$, 然后给出对于$[d/x]A$的一个证明. {译注: 也就是说, 对于论域的每个元素都需要给出证明. 这其实和对于推出$A\to B$的证明有些类似, 在类型论中这将会更加明显.}

第1.4节 第一个例子

我们称一个接受排中律的逻辑为古典的(classical). 作为古典证明和直觉主义证明的区别的例子, 我们考虑下列定理和证明.

在这个点, 古典数学家相当 (profoundly) 高兴, 因为这是对于一个看起来非平凡的定理的一个极其简短而优雅的证明. 直觉主义者相当不高兴, 因为它并没有实际披露满足$a^b$为有理数的无理数见证者$a$和$b$. 这样的见证者可能是$a=b=\sqrt{2}$, 也可能是$a={\sqrt{2}}^{\sqrt{2}}$和$b=\sqrt{2}$. 因此, 直觉主义者拒斥这个证明.

这里实际上并不正确的步骤是假定存在两种情形 (要么${\sqrt{2}}^{\sqrt{2}}$是有理数, 要么${\sqrt{2}}^{\sqrt{2}}$不是有理数) 而不知道哪一种情形成立, 这是(被直觉主义者拒斥的)排中律的一个实例.

然而, 并无所失! 作为一个直觉主义者, 我看了看上面的证明, 然后说

啊, 我理解了你的证明, 但是它所证明的是另外一个不同的定理! 实际上你证明的是:

定理. 如果${\sqrt{2}}^{\sqrt{2}}$是有理数或者不是有理数, 那么存在两个无理数$a$和$b$使得$a^b$是有理数.

第1.5节 另一个悖论

或许超越了直觉主义, 我们称某个逻辑是构造性的, 如果其证明描述了有效的构造. 这里所强调的是有效, 其是在说由证明所传达的构造可以实际被机械化地执行. 换言之, 构造性证明描述了算法. 第一眼看上去似乎所有描述了构造的证明都具有这种形式, 而从历史来说很长一段时间的确如此. 在19世纪的某个时间点似乎我们失去了这种数学和计算的直接联系, 这导致了直觉主义和其他更为严格的数学推理形式的诞生. 尽管如此, 时至今日绝大多数数学家仍然接受排中律, 是计算机科学复兴了人们对于构造性逻辑和数学的兴趣.

为了更好地理解这种区分, 我们考虑以下所谓的Banach-Tarski悖论.

这被认为是悖论性的, 因为显然我们不能施行这种分解. 中间的碎片实际上是不可测的点的无限散落. 这种分解依赖于集合论中的选择公理, 其是高度非构造性的.

第1.6节 关于证明和程序之间的联系

现在我们给出一个关于算术中的直觉主义证明和程序之间的联系的具体例子. 我们定义$$\begin{array}{rcl}\mathsf{even}(x)& \stackrel{\mathrm{\Delta }}{=}& \exists y.x=2y\\ \mathsf{odd}(x)& \stackrel{\mathrm{\Delta }}{=}& \exists y.x=2y+1\end{array}$$

现在让我们从这个证明中提取出一个函数. 根据真性的直觉主义解释, 这应该是一个从自然数到该数字为奇为偶的指示的函数. 我们可以使用布尔值, 不过为了清晰起见, 我们为此定义了一个特定的类型. 我们在ML中编写我们的函数, 但是当前其可以转写为任意的函数式语言. 鉴于ML内置的只有整数, 让我们像Peano一样由零和后继函数定义自然数 (类型nat).

datatype nat = zero | succ of nat
datatype eo = ev | od

(* even_or_odd : nat -> eo *)
fun even_or_odd x = case x of
    zero => ev
  | succ(x') => case even_or_odd x'
                  of ev => od
                   | od => ev

直觉主义者应该将归纳接纳为有效的推理原则吗? 或者说, 另一个相关的问题是, 直觉主义者应该接纳even_or_odd函数为一个有效的构造吗? 答案是肯定的, 因为显然这个函数对于每个自然数都是良定的, 因为 (a) 其对于$0$提供了一个情形, 且 (b) 其在递归调用中将参数从$x^{\prime }+1$归约为了$x^{\prime }$. 这是自然数上的原始递归的一般模式的一个例子. 我们称一个函数$f$由原始递归定义, 如果其定义具有形式$$\begin{array}{rcl}f(0)& =& c\\ f(x^{\prime }+1)& =& g(x^{\prime },f(x^{\prime }))\end{array}$$这意味着任何$f$的递归调用都必然在$x^{\prime }$上. 一般而言, 由使用归纳的直觉主义证明所提取出来的函数都会具有原始递归的形式.

回看原本的证明, 我们发现我们沿途丢失了一些信息. 如果我们展开$\mathsf{even}$和$\mathsf{odd}$的定义, 我们会看到一个存在量化子. 并且, 原本的证明给出了关于存在量化的见证者的信息. 在$x^{\prime }$为偶数的情形 (见证者为$y^{\prime }$), 对于$x^{\prime }+1$为奇数这一事实的见证者是相同的$y^{\prime }$. 在$x^{\prime }$为奇数的情形 (见证者为$y^{\prime }$), 对于$x^{\prime }+1$为偶数这一事实的见证者是$y^{\prime }+1$. 为了将这样的信息容纳于函数之中, 我们需要修改eo数据类型来携带见证者.

datatype nat = zero | succ of nat
datatype eo = ev of nat | od of nat

(* even_or_odd : nat -> eo *)
fun even_or_odd x = case x of
    zero => ev(zero)
  | succ(x') => case even_or_odd x'
                  of ev(y') => od(y')
                   | od(y') => ev(succ(y'))

我们想要强调一下, 我们并不是写了一个程序然后证明了其正确性 (虽然当然我们也可以这么做), 而是提供了一个构造性证明, 然后从中提取出了一个程序. 实际上也可以按照相反方向进行: 给定一个程序, 我们或许可以从中读出其所表示的证明. 这种证明和程序之间的联系还会在本课程的第一阶段占据相当长的时间.

第1.7节 隐藏计算性内容

通常 (尽管并不绝对必要, 这我们会在之后的作业里进行探索) 我们通过推出和谬 (falsehood) 来定义否定:$$\neg A\stackrel{\mathrm{\Delta }}{=}A\supset \perp$$现在从直觉主义来说, 一个对于$A\supset \perp$的证明是一个函数, 其接受一个对于$A$的证明, 返回一个对于$\perp$的证明. 然而, 既然我们有了对于$A$的一个反驳, 并不存在对于$A$的证明, 所以说这样的一个函数永远也不可能应用. 非正式的结论是对于$\neg A$的证明没有计算性内容. 这意味着我们可以通过将$A$替换为$\neg \neg A$来隐藏计算性内容. 例如, 如果我们并不想要见证者而只是想要知道某个数字$x$是奇是偶, 我们或许可以描述:$$\forall x.\neg \neg \mathsf{even}(x)\vee \neg \neg \mathsf{odd}(x)$$但是我们不得不非常小心, 因为这可能从根本上改变证明的结构. 特别地, 如果我们试图直接通过归纳来证明这个陈述, 归纳假设立即就会变得弱得多.

以下是两个类似的(非正式的)例子, 这个课程之后我们还要回到这些例子上来.$$\forall u,v.(\exists p.\mathsf{path}(p,u,v))\vee \neg \exists p.\mathsf{path}(p,u,v)$$假如量化的论域得当, 并且图中路径$p$连接的$u$和$v$时谓词$\mathsf{path}(p,u,v)$为真, 那么这个命题可以充当对于图可达性的刻画. 我们的意思是对于这个命题的一个构造性证明必然包含一个算法, 其确定了给定的顶点$u$和$v$之间是否存在一条路径, 并且若是存在则要返回某条路径. 我们可以使用诸多方式证明这个命题, 这将会导致诸多不同的算法 (通过路径长度上的归纳, 通过未访问结点集合上的归纳, 通过路径的边集上的归纳, 等等). 如果我们不想要路径本身, 只需要对于路径是否存在的指示, 那么我们可以在第一个存在量化子之前加上一个双重否定.

另一个角度是, 从古典逻辑来说, 这是一个全然平凡的陈述, 因为其有着$\forall u,v.A(u,v)\vee \neg A(u,v)$的形式, 故其是排中律的一个实例.

最后, 在编程语言领域我们可以将一个类型检查器描述为$$\forall e,\tau .\mathsf{type}(e,\tau )\vee \neg \mathsf{type}(e,\tau )$$其中若表达式$e$具有类型$\tau$则谓词$\mathsf{type}(e,\tau )$成立. 这个主题的一个变种是类型推导:$$\forall e.(\exists \tau .\mathsf{type}(e,\tau ))\vee \neg \exists \tau .\mathsf{type}(e,\tau )$$从实现的角度来说, 这两个刻画都不那么尽如人意, 因为当程序并非良类型时我们不能获得任何信息. 为了解决这个问题, 我们可以定义另外一个谓词$\mathsf{not\_type}(e,\tau )$使得其证明携带了所需的信息. 这有点类似于我们的奇数/偶数例子的逆, 因为我们本可以说$\forall x.\mathsf{even}(x)\vee \neg \mathsf{even}(x)$, 但是我们转而选择了使用$\mathsf{odd}$的一个显式定义.

第1.8节 一些命题的地位 (status)

讲座里有一些关于特定的命题是否拥有直觉主义逻辑中的证明的讨论. 在下次讲座之后, 我们会有些工具来证明其中一些命题, 但是直到数次讲座之后我们才能证明其中一些命题不是直觉主义可证的. 以下是一些我所能回忆起来的命题:

我们有$A\supset \neg \neg A$: 如果$A$为真, 那么$A$一定不为假. 从另一个方向来说, $\neg \neg A$在一般情况下不能推出$A$, 因为在$\neg \neg A$的证明中我们或许没有足够的信息. 不过, 我们有$\neg A\leftrightarrow \neg \neg \neg A$, 对于更深的否定迭代也是类似的. 从直觉上来说, 这是因为对于$\neg A$的证明没有计算性内容.

正如我们之前所言, 直觉主义者并不接受排中律$A\vee \neg A$, 但是我们可以证明其并不为假: $\neg \neg (A\vee \neg A)$是直觉主义为真的.

排中律和非直接证明的规则有些联系, 后者也是直觉主义所拒斥的. 非直接证明允许通过假定$\neg A$然后推导出一个矛盾来证明$A$. 但是, 我们要小心! 通过假定$A$然后推导出一个矛盾来证明$\neg A$本质上是直觉主义的. 从古典逻辑的角度来说, 这两种形式的证明在某种意义上是不可区分的, 但是从直觉主义来说它们是截然不同的 (一个有效, 另一个无效).

这是一种常见的现象: 在进行构造性推理时, 我们不得不对于留心于对于定理进行精确的表述, 因为许多古典等价的命题并非直觉主义等价的.

参考文献

第2章 自然演绎

第2.1节 引论

这一章的目的在于建立逻辑学的两种概念, 即命题和证明. 关于这些概念的正确基础并无统一的意见. 其中一种在计算机科学应用中取得巨大成功的方法, 在于藉由命题的证明来理解命题的意义. 用Martin-Löf [1983, 第27页]的话来说:

命题的意义是由[...]什么算作对其的验证而确定的.

一个验证或许可以理解为一种特定的证明, 其只会检视一个命题的组成部分. 这在Dummett [1991]中得到了远为细致的分析, 尽管其和计算机科学的联系更不那么直接了. 这种观念所导致的推理规则系统是自然演绎, 其由Gentzen [1935]提出而由Prawitz [1965]深入研究.

本章我们将会应用Martin-Löf的方法来解释基本的命题联结词, 这种方法遵循着丰富的哲学传统. 之后我们将会看到, 全称和存在量化子与诸如自然数, 列表, 或者树这样的类型能够自然地融入相同的框架之中.

我们将会藉由规则来定义命题逻辑的通常联结词 (合取, 推出, 析取) 的意义, 这些规则允许我们推理它们何时应该为真, 即所谓的引入规则. 根据这些规则, 我们可以推导出使用这些命题的规则, 即所谓的消去规则. 我们所得到的系统是自然演绎, 其是直觉主义逻辑的基础, 与函数式编程和逻辑编程有着直接的联系.

第2.2节 判断和命题

逻辑的Martin-Löf基础的基石是对于判断和命题的清晰区分. 一个判断是某种我们或许知道的东西, 也就是某种知识对象. 如果我们实际知道某个判断, 那么这个判断是显然的(evident).

我们之所以作出诸如天正在下雨的判断, 是因为我们有其证据. 在日常生活中, 这样的证据往往是直接的: 我们可以向窗外看看, 发现的确正在下雨. 在逻辑学中, 我们关心的是证据间接的情况: 我们根据其他显然的判断通过作出正确推理来推演出这判断.

逻辑学中最重要的判断形式是$A$为真, 其中$A$是一个命题. 当然也有其他许多得到仔细研究的判断形式, 例如$A$为假, $A$于时刻$t$为真 (来源于时态逻辑), $A$必然为真 (来源于模态逻辑), 程序$M$具有类型$\tau$ (来源于编程语言), 等等.

回到(前一段的)最后一个判断上来, 让我们试着解释合取的含义. 对于判断$A$为真 (预设$A$为一个命题) 我们记$A\mathit{true}$. 对于命题$A$和$B$, 我们可以构成复合命题$A$且$B$, 更形式化地记作$A\wedge B$. 但是, 我们尚未刻画合取的含义, 也就是什么算作对于$A\wedge B$的一个验证. 这是由以下的推理规则所完成的:$$\frac{A\mathit{true}B\mathit{true}}{A\wedge B\mathit{true}}\wedge I$$这里的名字$\wedge I$代表合取引入 (conjunction introduction), 鉴于合取的确在结论里被引入了.

这条规则规则允许我们在已经知道$A\mathit{true}$和$B\mathit{true}$的情况下断言$A\wedge B\mathit{true}$. 在这条推理规则之中, $A$和$B$是模式变量(schematic variable), 而$\wedge I$是规则的名字.

从直觉上来说, $\wedge I$规则是说对于$A\wedge B\mathit{true}$的一个证明由对于$A\mathit{true}$的一个证明连带着对于$B\mathit{true}$的一个证明构成. 这恰是我们在将第一次讲座里所提及的合取的直觉主义意义.

推理规则的一般形式为$$\frac{J_1\dots J_n}{J}\mathit{name}$$其中判断$J_1,\dots ,J_n$被称为前提(premise), 判断$J$被称为结论(conclusion). 一般而言, 我们将会使用字母$J$代表判断, 而$A,B,C$留给命题使用.

我们将合取引入视为完整地描述了$A\wedge B$的意义. 那么, 如果我们知道$A\wedge B$为真, 什么可以推演 (deduce) 呢? 根据以上的规则, 拥有对于$A\wedge B$的一个验证意味着拥有对于$A$和$B$的验证. 因此, 以下两条规则得到了澄清:$$\frac{A\wedge B\mathit{true}}{A\mathit{true}}\wedge E_1\frac{A\wedge B\mathit{true}}{B\mathit{true}}\wedge E_2$$名字$\wedge E_1$代表第一合取消去 (first conjunction elimination), 因为前提中的合取在结论中已被消去. 类似地, $\wedge E_2$代表第二合取消去.

之后我们将会看到为了保证一个联结词的构成, 引入, 消去能够正确适配到一起所必要的精确条件. 暂时我们将只能非形式化地论述消去规则的正确性, 如我们刚才对于合取消去规则所做的.

作为第二个例子, 我们考虑记作$\top$的命题真 (truth). 命题真应该永远为真, 这意味着其引入规则没有前提.$$\frac{}{\top \mathit{true}}\top I$$因此, 当我们知道$\top \mathit{true}$时, 我们并不拥有什么信息, 所以这里没有消去规则.

两个命题的合取是由带有两个前提的引入规则和两条相对应的消去规则所刻画的. 我们可以将(命题)真想成是零个命题的合取. 根据类比, 它应该具有一条带有零个前提的引入规则, 以及零条消去规则. 这恰是我们上面所写下的内容.

第2.3节 假言判断

考虑以下演绎, 对于任意的命题$A,B,C$:$$\frac{\frac{A\wedge (B\wedge C)\mathit{true}}{B\wedge C\mathit{true}}\wedge E_2}{B\mathit{true}}\wedge E_1$$这里我们实际证明了任何东西吗? 乍看上去似乎不是这么回事: $B$是一个任意的命题; 显然我们不应该能够证明其为真. 再仔细检视一遍我们发现所有的推理都是正确的, 但是第一个判断$A\wedge (B\wedge C)\mathit{true}$没有得到澄清. 我们可以从这个演绎中提取出如下知识:

根据$A\wedge (B\wedge C)$为真的假设, 我们可以推演出$B$必然为真.

这是假言判断(hypothetical judgment)的一个例子, 而以上的图形是一个假言演绎(hypothetical deduction). 一般而言, 我们可以拥有多于一个假设, 所以一个假言演绎具有形式$$\begin{array}{c}\begin{array}{ccc}{J}_1& \cdots & J_n\end{array}\\ ⋮\\ J\end{array}$$其中判断$J_1,\dots ,J_n$是未经证明的判断, 而判断$J$是结论. 推理规则的所有实例也都是假言判断, 即便在推理规则没有前提的情况下可能只有$0$个假设. {译注: 译者的一个疑问是, 推理规则本身算作假言判断吗? 尽管推理规则总是模式性的, 或者说含有元变量, 但是实际上推理规则的实例也总是含有元变量. 译者认为显然应该是算的.}

推理的许多错误都是由于忽略了对某些隐藏假设的依赖而导致的. 当我们需要显式化时, 我们会将其上由假言演绎所建立的假言判断写成$J_1,\dots ,J_n⊢J$. 我们可以将$J_1,\dots ,J_n$称为假言判断的前件, 而$J$称为假言判断的后件. 例如, 假言判断$A\wedge (B\wedge C)\mathit{true}⊢B\mathit{true}$是由之前的假言演绎所证明的, 即$B\mathit{true}$的确可由假设$A\wedge (B\wedge C)\mathit{true}$通过推理规则推出.

假言判断的关键性质, 或者说定义性质(defining property), 是我们总是可以将对于某个假设$A\mathit{true}$的所有使用替换为对于$A$的一个证明. 形式化证明替换这个概念并不全然是直接的, 但是它应该是相当直觉性的, 以至于现在我们将其作为一种原始概念. {译注: 这让译者想到内化 (internalization).}

根据假言判断, 我们现在可以解释推出 (implication) $A$推出$B$或者如果$A$那么$B$ (更形式化地, $A\supset B$) 的意义了. 其引入规则读作: $A\supset B$为真, 如果在$A$为真的假设下$B$为真.$$\frac{\begin{array}{c}\frac{}{A\mathit{true}}u\\ ⋮\\ B\mathit{true}\end{array}}{A\supset B\mathit{true}}\supset I^u$$这条规则的微妙之处在于标签$u$和那条横杠. 如果我们省略这个注解 (annotation), 那么这个规则将会变成$$\frac{\begin{array}{c}A\mathit{true}\\ ⋮\\ B\mathit{true}\end{array}}{A\supset B\mathit{true}}\supset I$$这是不正确的: 这看起来像是根据$A\mathit{true}$的假设对于$A\supset B\mathit{true}$的推导. 但是, 假设$A\mathit{true}$是在证明$A\supset B\mathit{true}$的过程之中引入的, 结论不应该依赖于它! {译注: 也就是不依赖于$A\mathit{true}$这个假设.}

推出$A\supset B$是否为真当然是独立于$A$自身是否实际为真的问题的. 因此, 我们以一个新的名字$u$标记了假设的使用, 并且对于将这个假设引入推导的推理, 我们标记以相同的名字$u$.

我们应该注意到证明中以$u$标记的假设只在推理$\supset I^u$的上方可用. 我们很快就会发现, 如果我们允许违反标签$u$的作用域, 那么自然演绎会变成不一致的. 另外, 一个证明中的标签应该是不同的, 这是为了我们能够毫无歧义地指出一个假设引入的位置. {译注: 实际上译者认为其实标签是可以重复的, 但是终归标签的目的是为了无误指明哪些假设要解除 (discharge).}

在我们施行一些示例证明之前, 我们考虑一下推出的消去规则应该要说什么. 根据其唯一的引入规则, 拥有对于$A\supset B\mathit{true}$的一个证明意味着我们根据$A\mathit{true}$有了一个对于$B\mathit{true}$的假言性证明. 通过替换原理, 如果我们有了对于$A\mathit{true}$的一个证明, 那么我们就得到了对于$B\mathit{true}$的一个证明.$$\frac{A\supset B\mathit{true}A\mathit{true}}{B\mathit{true}}\supset E$$这就完成了和推出相关的规则. {译注: 这里所谓的替换原理本质上来说就是第一次讲座的对于推出的直觉主义解释, 虽然假言判断是外部性的, 推出是内部性的.}

第2.4节 构造证明

在移至其他联结词之前, 让我们构造一些(直觉主义)自然演绎中的示例证明. 和通常数学一样, 往往是证明构造的过程而非最终产物提供了更多的洞察. 尽管在纸面上很难呈现这种传达直觉的随时间变化方面, 但我们会尽力为之.

我们从对于推出的最简单使用开始, 即$A\supset A\mathit{true}$. 在呈现里, 我们用竖着的点来指出我们正在试图填充一个缺失的证明. 假设 (若是存在的话) 则在更之上出现.$$\begin{array}{c}⋮\\ A\supset A\mathit{true}\end{array}$$既然我们没有可用的假设, 我们从一个推出引入开始.$$\frac{\begin{array}{c}\frac{}{A\mathit{true}}u\\ ⋮\\ A\mathit{true}\end{array}}{A\supset A\mathit{true}}\supset I^u$$在这个时间点我们看到我们唯一的假设和我们试图证明的东西是匹配的, 所以说我们就将gap闭合了.$$\frac{\frac{}{A\mathit{true}}u}{A\supset A\mathit{true}}\supset I^u$$合法性检查: $u$只在$\supset I^u$推理(线)的上方用到, 所以作用域是正确的.

接着, 我们试着证明稍微复杂一些的东西, 即$A\supset (B\supset A)\mathit{true}$. 从直觉上来说, 这之所以是真的是因为我们可以从第一个假设$A$就可以得到结论$A$, 而并不需要第二个假设$B$. 以下是怎么将证明写出来的过程.$$\begin{array}{c}⋮\\ A\supset (B\supset A)\mathit{true}\end{array}$$我们又一次从推出引入开始.$$\frac{\begin{array}{c}\frac{}{A\mathit{true}}u\\ ⋮\\ B\supset A\mathit{true}\end{array}}{A\supset (B\supset A)\mathit{true}}\supset I^u$$我们再一次使用推出引入, 以一个新的标签$w$.$$\frac{\frac{\begin{array}{c}\begin{array}{cc}\frac{}{A\mathit{true}}u& \frac{}{B\mathit{true}}w\end{array}\\ ⋮\\ A\mathit{true}\end{array}}{B\supset A\mathit{true}}\supset I^w}{A\supset (B\supset A)\mathit{true}}\supset I^u$$这里我们有两个可用的假设, 但是我们只需要用第一个以$u$标记的假设来闭合gap和完成证明.$$\frac{\frac{\frac{}{A\mathit{true}}u}{B\supset A\mathit{true}}\supset I^w}{A\supset (B\supset A)\mathit{true}}\supset I^u$$这是对于我们并不一定需要使用假设这个事实的刻画, 如果一个假设并不需要, 那么其就不用出现在最终证明里.

然后, 让我们展示一个需要使用假设不止一次的例子, 并且其也需要使用消去规则进行推理.$$\begin{array}{c}⋮\\ (A\wedge B)\supset (B\wedge A)\mathit{true}\end{array}$$和之前一样, 我们从推出引入开始.$$\frac{\begin{array}{c}\frac{}{A\wedge B\mathit{true}}u\\ ⋮\\ B\wedge A\mathit{true}\end{array}}{(A\wedge B)\supset (B\wedge A)\mathit{true}}\supset I^u$$鉴于我们要证明一个合取, 所以说我们可以将其归约为证明其两个合取分量 (conjunct).$$\frac{\frac{\begin{array}{c}\frac{}{A\wedge B\mathit{true}}u\\ ⋮\\ B\mathit{true}\end{array}\begin{array}{c}\frac{}{A\wedge B\mathit{true}}u\\ ⋮\\ A\mathit{true}\end{array}}{B\wedge A\mathit{true}}\wedge I}{(A\wedge B)\supset (B\wedge A)\mathit{true}}\supset I^u$$这里我们将假设$u$写了两次, 因为其在两个子证明中都是可用的. 在讲座里我们使用了稍微不同的形式, 其中我们有一块草稿区域用于记录假设, 所以那时记录一次就够了.

让我们来看第一个子目标, 即由$A\wedge B\mathit{true}$证明$B\mathit{true}$. 这里我们无法使用引入规则来处理 (因为$B$是任意的), 但是我们通过消去规则以利用$A\wedge B\mathit{true}$这个知识.$$\frac{\frac{\begin{array}{c}\frac{\frac{}{A\wedge B\mathit{true}}u}{B\mathit{true}}\wedge E_2\\ ⋮\\ B\mathit{true}\end{array}\begin{array}{c}\frac{}{A\wedge B\mathit{true}}u\\ ⋮\\ A\mathit{true}\end{array}}{B\wedge A\mathit{true}}\wedge I}{(A\wedge B)\supset (B\wedge A)\mathit{true}}\supset I^u$$现在我们可以闭合这gap, 因为我们有了一个对于$B\mathit{true}$的证明, 由消去规则所构造.$$\frac{\frac{\frac{\frac{}{A\wedge B\mathit{true}}u}{B\mathit{true}}\wedge E_2\begin{array}{c}\frac{}{A\wedge B\mathit{true}}u\\ ⋮\\ A\mathit{true}\end{array}}{B\wedge A\mathit{true}}\wedge I}{(A\wedge B)\supset (B\wedge A)\mathit{true}}\supset I^u$$对于$\wedge I$的第二个前提的证明完全是对称的, 所以说我们不必细致写下每一个单独步骤.$$\frac{\frac{\frac{\frac{}{A\wedge B\mathit{true}}u}{B\mathit{true}}\wedge E_2\frac{\frac{}{A\wedge B\mathit{true}}u}{A\mathit{true}}\wedge E_1}{B\wedge A\mathit{true}}\wedge I}{(A\wedge B)\supset (B\wedge A)\mathit{true}}\supset I^u$$

第2.5节 析取和谬

到目前为止, 我们已经解释了合取, (命题)真, 推出的意义. 析取$A$或$B$ (记作$A\vee B$) 更为复杂, 但并不需要新的判断形式. 析取是由两条引入规则刻画的: $A\vee B$为真, 如果$A$或者$B$为真.$$\frac{A\mathit{true}}{A\vee B\mathit{true}}\vee I_1\frac{B\mathit{true}}{A\vee B\mathit{true}}\vee I_2$$诸如以下的消去规则是不正确的$$\frac{A\vee B\mathit{true}}{A\mathit{true}}\vee E_1?$$因为即便我们知道$A\vee B$为真, 我们也不知道到底$A$和$B$哪一个析取分量 (disjunct) 为真. 从具体方面来说, 使用这一规则按照以下方式推导出任意的命题$A$为真:$$\frac{\frac{\frac{\frac{}{B\mathit{true}}u}{B\supset B\mathit{true}}\supset I^u}{A\vee (B\supset B)\mathit{true}}\vee I_2}{A\mathit{true}}\vee E_1?$$

因此, 我们需要换种不同的方法. 如果我们知道$A\vee B$为真, 我们必须要考虑两种情形: $A\mathit{true}$和$B\mathit{true}$. 如果我们可以在两种情形下都证明结论$C\mathit{true}$, 那么$C$必然为真! 我们将其写成一条推理规则:$$\frac{A\vee B\mathit{true}\begin{array}{c}\frac{}{A\mathit{true}}u\\ ⋮\\ C\mathit{true}\end{array}\begin{array}{c}\frac{}{B\mathit{true}}w\\ ⋮\\ C\mathit{true}\end{array}}{C\mathit{true}}\vee E^{u,w}$$如果在$A\vee B\mathit{true}$是因为$A$为真和$A\vee B\mathit{true}$是因为$B$为真这两种情形下我们都能推出$C\mathit{true}$, 那么若我们知道了$A\vee B\mathit{true}$也就知道了$C\mathit{true}$. 注意到我们又使用了假言判断的机制. 在第二个前提的证明里我们可以使用标记了$u$的假设$A\mathit{true}$, 在第三个前提的证明里我们可以使用标记了$w$的假设$B\mathit{true}$. 这两个假设都在析取消去时被解除了.

让我们更为显式地澄清这条规则的结论. 根据第一个前提我们知道$A\vee B\mathit{true}$. 其两个引入规则的前提分别是$A\mathit{true}$和$B\mathit{true}$. 在$A\mathit{true}$情形下我们根据替换原理和第二个前提作出了结论$C\mathit{true}$: 我们将假言推导中对于标记了$u$的假设的所有使用替换为了对于$A\mathit{true}$的证明. $B\mathit{true}$的情形是对称的, 使用的是第三个前提的假言推导.

在讲座里我们原本所提出的是如下规则:$$\frac{A\vee B\mathit{true}A\supset C\mathit{true}B\supset C\mathit{true}}{C\mathit{true}}\vee E?$$这与我们所选择的规则紧密关联, 并且实际上是可推导的(derivable), 因而是正确的. 但是它有着一个缺陷:

第2.6节 总结: 自然演绎

第2.7节 记号性定义

第2.8节 更多的例子

第3章 和谐

Rec 1: Dcheck与和谐

第4章 证明作为程序

第5章 验证

Rec 2: 验证和证明项

第6章 规则作为算法

第7章 相继式演算

Rec 3: 相继式演算

第8章 切消

第9章 证明和验证

Rec4: 规则归纳

第10章 从证明系统到编程语言

第11章 自然数

Rec 5: 编程语言的动态语义

第12章 延续

第13章 谓词演算

期中考试

第14章 命题定理证明

Rec6: 古典逻辑和谓词演算

第15章 逆转

第16章 certification

Rec 7: 逆转

第17章 聚焦

第18章 逻辑编程

Rec8: Prolog

第19章 一个元循环解释器

第20章 目标栈

Rec9: 无收缩相继式演算

第21章 合一 (unification)

第22章 逆转方法

Rec 10: 逆转方法的例子

第23章 运行时代码生成

这次没有现成的讲义, 但是有推荐的阅读材料. 第一个阅读材料是作者的论文Modal Types as Staging Specifications for Run-time Code Generation (模态类型作为运行时代码生成的阶段化描述). 这篇论文探索和讨论了模态逻辑和多阶段编程之间的联系.

Rec11: lambda盒子

第24章 线性逻辑

第25章 同步消息传递

Rec12: 线性逻辑