证明论和逻辑代数

第1章 相继式系统

在第1.1节给出预备评注和对于本书范围的简要解释之后, 我们将分别为古典逻辑和直觉主义逻辑引入两个相继式系统LK和LJ. 这两个相继式系统对于第I部分的证明论研究都是基础性的, 其最初由G. Gentzen在他的论文 (Gentzen 1935) 里引入. 基本的证明和可证明性的概念首先被引入. 然后对于LK的完备性和切消的初等证明被给出, 通过使用古典逻辑的一个可逆相继式系统LK*, 其是LK的一种替代. 这将会是展现证明论式论证如何进行的一个简明例子.

第1.1节 开篇

基本概念和记号

我们将会使用$\wedge$, $\vee$, $\to$, $\neg$分别表达基本的逻辑联结词合取, 析取, implication, 否定. {译注: 为了避免各种可能的混淆, implication就不翻译了.} 若有必要, 例如当我们讨论模态逻辑和亚结构逻辑的时候, 我们将会引入额外的逻辑联结词和逻辑常量. 我们从外部取一个固定的命题变量的可数集. 公式和通常情况一样通过归纳定义, 从命题变量和逻辑常量开始, 然后反复应用逻辑联结词. 括号会按照通常方式进行省略, 只要不至于引起误解. 为了简化表达式, 我们采取约定, $\neg$比其他逻辑联结词都结合得更紧密. 因此, 例如, 公式$p\vee \neg q$表示$p\vee (\neg q)$. 我们将会使用小写希腊字母表达公式. 当一个公式$\beta$出现在一个公式$\alpha$的归纳定义之中, 公式$\beta$被称为$\alpha$的一个子公式. 除开$\alpha$之外的$\alpha$的每个子公式被称为$\alpha$的一个真子公式. 例如, $p,q,\neg q,p\vee \neg q$都是$p\vee \neg q$的子公式, 而前三个则是$p\vee \neg q$的真子公式.

有时我们按照以下方式对于公式的构造施行归纳论证. 也就是说, 为了确保每个公式都具有某个给定的性质$P$, 我们要表明 (1) 每个命题变量 (以及每个常量) 都具有$P$ (2) 对于每个$\beta$, 若$\beta$的每个真子公式$\gamma$都具有$P$, 那么$\beta$也具有$P$. 这种形式的归纳也可以表达为对于公式的长度进行归纳. 这里某个给定公式$\alpha$的长度的含义是$\alpha$中的逻辑符号的总数目. 可能公式$\beta$在某个给定的$\alpha$中作为子公式出现不止一次, 但是在不同的地方出现. 例如, 公式$p$在公式$p\vee \neg p$里出现了两次. 如果我们需要进行区分, 那么我们会使用术语公式出现. 然后, 我们可以说$p\vee \neg p$拥有$p$的两次公式出现. 一般而言, 当我们不只是关心表达式本身也关心其出现的位置时, 我们就会使用词汇出现. 在本书中, 我们有时使用iff作为if and only if的缩写. {译注: 当然了, 我们都会将其翻译为当且仅当, 这是Paul Halmos所创制的表达.}

逻辑的句法方法和语义方法之比较

在以下内容里, 我们将简要介绍主题的背景, 特别是本教科书的第I部分和第II部分的区别和联系. 熟悉这部分内容的读者可以跳过.

引入一个逻辑的标准方式时将其描述为一个形式系统. 一个形式系统通常由公理和推理规则构成, 其确定了系统中的公式的可证明性. 一个给定公式$\alpha$在系统中是可证的, 如果$\alpha$可以在系统中被推导出来, 即通过从系统的公理开始, 反复应用系统的规则得到. 一个对于$\alpha$的证明 (或者推导) 是一个有限的figure, 其表明了$\alpha$在系统中是如何推导出来的. 证明和可证明性的概念由此是句法性的概念, 其由符号和机械过程构成.

作为形式系统的一个例子, 以下我们将给出古典逻辑的一个标准Hilbert风格系统HK. 其由作为单一规则的modus ponens和以下给出的公理模式构成. 这里的modus ponens是说一个公式$\beta$可以由$\alpha$和$\alpha \to \beta$共同推导出来. 另外, 每个公理模式不是单一的公式, 而是具有模式所表示的相同句法形式的所有公式. 因此, 一个公理模式的每个实例都可以视为一个公理. (出于简单性的考量, $\neg \alpha$在本节的剩余部分里将被视为$\alpha \to 0$的缩略, 其中$0$是一个逻辑常量, 其表达了一个矛盾.) {原注: 为了避免符号太过复杂, 我们使用相同的符号表达公式和公式模式.}

现在HK的公理模式列出如下, 其看上去和标准的有些许不同. 不过, 我们的选择是为了容易看出其与下一节要引入的古典逻辑的相继式系统LK之间的联系.

1. $\alpha \to (\beta \to \alpha )$ (左弱化公理)
2. $(\alpha \to (\alpha \to \gamma ))\to (\alpha \to \gamma )$ (收缩公理)
3. $(\alpha \to (\beta \to \gamma ))\to (\beta \to (\alpha \to \gamma ))$ (交换公理)
4. $0\to \alpha$
5. $(\alpha \to \beta )\to ((\gamma \to \alpha )\to (\gamma \to \beta ))$
6. $(\alpha \to \gamma )\to ((\beta \to \gamma )\to ((\alpha \vee \beta )\to \gamma ))$
7. $\alpha \to (\alpha \vee \beta )$
8. $\beta \to (\alpha \vee \beta )$
9. $(\gamma \to \alpha )\to ((\gamma \to \beta )\to (\gamma \to (\alpha \wedge \beta )))$
10. $(\alpha \wedge \beta )\to \alpha$
11. $(\alpha \wedge \beta )\to \beta$
12. $\neg \neg \alpha \to \alpha$ (双重否定律)

呈现Hilbert风格系统的另一种方式是取modus ponens和替换规则作为规则, 然后取公理而非公理模式. 通过这里的替换规则我们可以根据$\alpha$对于任意的一致替换$\sigma$推出$\sigma (\alpha )$. {原注: 这里的$\sigma$是一个从命题变量的有限集合$\{p_1,\dots ,p_m\}$到某个公式集合的映射, 而$\sigma (\alpha )$代表由$\alpha$通过将$\alpha$中的每个$p_i$同时替换为$\sigma (p_i)$得到的公式, 其中$i=1,\dots ,m$. 这样一个公式$\sigma (\alpha )$被称为$\alpha$的一个替换实例 (或者更简单地说, 实例).} 在这种情况下, 例如弱化公理就是通过一个单独的公理$p\to (q\to p)$给出的, 其中$p$和$q$是不同的命题变量. 其他的弱化公理则是通过这条公理应用替换规则得到的.

第1.2节 古典逻辑的相继式系统LK

我们将要引入古典逻辑的一个相继式系统LK. 与Hilbert风格系统不同的是, 相继式系统中的基本表达式是相继式. LK中的每个相继式都是具有以下形式的表达式, 其中每个${\alpha }_i$ ($i\le m$) 和每个${\beta }_j$ ($j\le n$) 都是公式, 而$m,n\ge 0$. 这里的逗号$,$和箭头$\Rightarrow$都是元逻辑符号.$${\alpha }_1,\dots ,{\alpha }_m\Rightarrow {\beta }_1,\dots ,{\beta }_n$$因此, 每个相继式都是由逗号分隔的公式的有限序列, 而相继式又由$\Rightarrow$划分为前件(antecedents)${\alpha }_1,\dots ,{\alpha }_m$和后件(succedents)${\beta }_1,\dots ,{\beta }_n$.

大致来说, 前件和后件可以分别理解为假设和结论. 但是, 这里我们必须要小心, 因为前件是合取式(conjunctive-like)理解而后件是析取式(disjunctive-like)理解. 也就是说, 上述的相继式从直觉上来理解即$({\beta }_1\vee \dots \vee {\beta }_n)$可由假设${\alpha }_1,\dots ,{\alpha }_m$推出, 或者等价地说, 可由假设$({\alpha }_1\wedge \dots \wedge {\alpha }_m)$推出. 当后件为空时, 相继式${\alpha }_1,\dots ,{\alpha }_m\Rightarrow$的含义是根据假设${\alpha }_1,\dots ,{\alpha }_m$可以推出一个矛盾. 从另一方面来说, 如果前件为空, 相继式$\Rightarrow {\beta }_1,\dots ,{\beta }_n$应该理解为(在没有任何假设的情况下)可以推出${\beta }_1\vee \dots \vee {\beta }_n$.

在相继式系统里, 我们讨论相继式的可证明性和有效性, 而非公式的, 它们分别代表了句法和语义的视角. 每个相继式系统都由初始相继式和规则构成. 前者对应于Hilbert风格系统中的公理模式. 一个给定的相继式系统的每条规则确定了一个相继式何时以及如何由其他已经推得的相继式推出 (通常来说, 是从有限数目的相继式推出). 在我们的系统LK中, 如下所示, 每条规则由一或两个上相继式(upper sequent)和一个下相继式(lower sequent)构成, 意即下相继式可由这些上相继式推出. 以下的大写希腊字母代表(可能为空的)公式的有限序列. LK具有以下三个种类的规则{原注: 切规则经常被视为一种结构规则, 但是本书将其从结构规则中分离出来, 因为接下来介绍亚结构逻辑的时候会更加方便.}:

1. 逻辑联结词$\vee ,\wedge ,\to ,\neg$的(左和右)规则,
2. 切规则,
3. (左和右)结构规则.

LK具有以下初始相继式和规则.

0. 初始相继式: LK的每个初始相继式都是一个具有形式$\alpha \Rightarrow \alpha$的相继式.

1. 逻辑联结词的规则:$$\frac{\alpha ,\Gamma \Rightarrow \Pi \beta ,\Gamma \Rightarrow \Pi }{\alpha \vee \beta ,\Gamma \Rightarrow \Pi }(\vee \Rightarrow )$$$$\frac{\Gamma \Rightarrow \Lambda ,\alpha }{\Gamma \Rightarrow \Lambda ,\alpha \vee \beta }(\Rightarrow \vee 1)\frac{\Gamma \Rightarrow \Lambda ,\beta }{\Gamma \Rightarrow \Lambda ,\alpha \vee \beta }(\Rightarrow \vee 2)$$$$\frac{\alpha ,\Gamma \Rightarrow \Pi }{\alpha \wedge \beta ,\Gamma \Rightarrow \Pi }(\wedge 1\Rightarrow )\frac{\beta ,\Gamma \Rightarrow \Pi }{\alpha \wedge \beta ,\Gamma \Rightarrow \Pi }(\wedge 2\Rightarrow )$$$$\frac{\Gamma \Rightarrow \Lambda ,\alpha \Gamma \Rightarrow \Lambda ,\beta }{\Gamma \Rightarrow \Lambda ,\alpha \wedge \beta }(\Rightarrow \wedge )$$$$\frac{\Gamma \Rightarrow \Lambda ,\alpha \beta ,\Delta \Rightarrow \Pi }{\alpha \to \beta ,\Gamma ,\Delta \Rightarrow \Lambda ,\Pi }(\to \Rightarrow )\frac{\alpha ,\Gamma \Rightarrow \Lambda ,\beta }{\Gamma \Rightarrow \Lambda ,\alpha \to \beta }(\Rightarrow \to )$$$$\frac{\Gamma \Rightarrow \Lambda ,\alpha }{\neg \alpha ,\Gamma \Rightarrow \Lambda }(\neg \Rightarrow )\frac{\alpha ,\Gamma \Rightarrow \Lambda }{\Gamma \Rightarrow \Lambda ,\neg \alpha }(\Rightarrow \neg )$$

2. 切规则$$\frac{\Gamma \Rightarrow \Lambda ,\alpha \alpha ,\Delta \Rightarrow \Pi }{\Gamma ,\Delta \Rightarrow \Lambda ,\Pi }(\mathrm{cut})$$

3. 结构规则

• 交换规则:$$\frac{\Gamma ,\alpha ,\beta ,\Delta \Rightarrow \Pi }{\Gamma ,\beta ,\alpha ,\Delta \Rightarrow \Pi }(e\Rightarrow )\frac{\Gamma \Rightarrow \Pi ,\alpha ,\beta ,\Lambda }{\Gamma \Rightarrow \Pi ,\beta ,\alpha ,\Lambda }(\Rightarrow e)$$
• 收缩规则:$$\frac{\alpha ,\alpha ,\Gamma \Rightarrow \Pi }{\alpha ,\Gamma \Rightarrow \Pi }(c\Rightarrow )\frac{\Gamma \Rightarrow \Pi ,\alpha ,\alpha }{\Gamma \Rightarrow \Pi ,\alpha }(\Rightarrow c)$$
• 弱化规则:$$\frac{\Gamma \Rightarrow \Pi }{\alpha ,\Gamma \Rightarrow \Pi }(w\Rightarrow )\frac{\Gamma \Rightarrow \Pi }{\Gamma \Rightarrow \Pi ,\alpha }(\Rightarrow w)$$

出于方便的考量, 我们为每条规则附加了一个诸如$(\vee \Rightarrow )$这样的名字. 在每条规则里, 使用小写希腊字母$\alpha$和$\beta$的公式被称为活跃(active)公式. 另外, 每条规则里的下相继式里显式呈现的使用小写希腊字母的公式被称为规则的主(principal)公式. 例如, $\alpha \vee \beta$是规则$(\vee \Rightarrow )$的主公式, 而$\alpha$是规则$(w\Rightarrow )$的主公式. 其他的公式都被称为副(side)公式. 切规则的活跃公式被称为切公式. 对于逻辑联结词的规则而言, 主公式出现在前件里的是左规则. 对于结构规则, 活跃公式都出现在前件里的是左规则. 将前件替换为后件, 可以得到右规则的定义. 左规则的名字具有形式$(♯\Rightarrow )$, 右规则的名字具有形式$(\Rightarrow ♯)$.

每条规则都是说当上相继式可证明时, 其下相继式也是可证明的. 例如, 规则$(\wedge 1\Rightarrow )$是说每当相继式$\alpha ,\Gamma \Rightarrow \Pi$可证明时, 相继式$\alpha \wedge \beta ,\Gamma \Rightarrow \Pi$也是可证明的. 类似地, 规则$(\Rightarrow \wedge )$是说 (为了简洁, 假定$\Lambda$为空) 每当$\Gamma \Rightarrow \alpha$和$\Gamma \Rightarrow \beta$都是可证的, 那么$\Gamma \Rightarrow \alpha \wedge \beta$也是可证的. 以这种方式, 每个逻辑联结词的公式精确地描述了这个联结词的功能.

切规则表达了演绎推理的一种基础原则. 实际上, 其是在说 (又一次为了简洁, 假定$\Lambda$为空) 如果$\Gamma \Rightarrow \alpha$是可证明的, 并且$\alpha ,\Delta \Rightarrow \Pi$是可证明的, 那么$\Gamma ,\Delta \Rightarrow \Pi$也是可证明的. 所有的结构规则作为一个整体控制了给定相继式里的前件和后件里的公式的顺序, 重复和省略. 特别地, 每条左结构规则从直觉上来说含义如下:

• 交换规则允许我们使用前件里的公式, 不论它们以何种顺序排列.
• 收缩规则表达了前件里的公式出现在推理结论时可以使用不止一次.
• 左弱化规则允许我们将任意的公式放在前件里, 即便其在推理结论时没有用到.

我们注意到一个相继式在可证明时或许拥有数个不同的证明. 对于某个相继式$\Gamma \Rightarrow \Delta$的一个给定证明$\mathsf{P}$, 设$\Sigma \Rightarrow \Theta$是出现在$\mathsf{P}$中的一个相继式. 那么, 证明$\mathsf{P}$中相继式$\Sigma \Rightarrow \Theta$之上 (也包括自身) 的子图形$\mathsf{Q}$构成了一个终相继式为$\Sigma \Rightarrow \Theta$的证明. 作为$\mathsf{Q}$这样的一个证明被称为$\mathsf{P}$的一个子证明.

在给出证明的具体例子之前, 我们给出为了简化对于证明的描述的约定. 我们注意到在我们所列出的LK的规则里, 上相继式里的活跃公式总是置于前件的最左边或者后件的最右边, 除了交换规则. 理由只是为了简化规则的呈现, 因而这些限制不是本质性的. 实际上, 只要活跃公式出现在相应的前件或者后件的任何位置, 规则就可以应用. 这是因为, 我们可以首先对于上相继式应用交换规则, 将活跃公式移至前件的最左边或者后件的最右边, 然后应用所牵涉的规则, 最后再用交换规则将活跃公式移回去. 为了解释这种调整, 让我们考虑以下形式的规则$(\wedge 1\Rightarrow )$:$$\frac{\Sigma ,\alpha ,\Gamma \Rightarrow \Delta }{\Sigma ,\alpha \wedge \beta ,\Gamma \Rightarrow \Delta }$$以下是从这上相继式得到下相继式的方式.$$\frac{\frac{\frac{\frac{\frac{\Sigma ,\alpha ,\Gamma \Rightarrow \Delta }{\cdots }}{\alpha ,\Sigma ,\Gamma \Rightarrow \Delta }}{\alpha \wedge \beta ,\Sigma ,\Gamma \Rightarrow \Delta }(\wedge 1\Rightarrow )}{\cdots }}{\Sigma ,\alpha \wedge \beta ,\Gamma \Rightarrow \Delta }$$这里的点$\dots$代表对于交换规则的数次应用. 以这种方法, 我们将允许应用每条规则而不管其活跃公式出现在哪里.

使用公式的多重集的一个对于LK的改进呈现

在给定证明的长度上进行归纳

可逆系统LK*

第2章 相继式系统的切消

第3章 逻辑性质的证明论式分析

第4章 模态逻辑和亚结构逻辑

第5章

第6章 从代数到逻辑

逻辑的句法或者说符号方法起源于19世纪中叶. G. Boole在他的书 (Boole 1854) 中试图将逻辑推理表达为代数计算. 又过了几十年我们才有了Hilbert风格的系统.

第6.1节 格与布尔代数

以下我们 先引入一些代数结构的基本概念, 然后呈现其性质.

第6.2节 子代数, 同态和直积

第6.3节 布尔代数的表示

第6.4节 古典逻辑的代数完备性

第6.5节 Many-Valued Chains and the Law of Residuation

第7章 代数逻辑的基本

第7.1节 Heyting代数

每个Heyting代数也(一定)有最大元素$1$, 并且对于每个元素$a$都有$1$等于$a\to a$. 另外, $\neg a$被定义为$a\to 0$. 显然, 每个布尔代数都是一个Heyting代数.

第7.2节 Lindenbaum-Tarski代数

第7.3节 局部有限代数

第7.4节 有限可嵌入性质和有限模型性质

第7.5节 Heyting代数的canonical扩张

第8章 Logics and Varieties

第8.1节 超直觉主义逻辑的格结构

第8.2节 由所有Heyting代数构成的variety HA

第9章 Residuated Structures

第10章 模态代数

对于模态逻辑的语义研究已经藉由使用Kripke语义而发展得相当成功.

第10.1节 模态代数