证明论和逻辑代数

第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风格的系统. 尽管并非以其完备形式, Boole通过引入一些代数等式 (作为逻辑公理) 和一些用于从代数等式推导其他代数等式的规则 (作为推理规则) 建立了代数逻辑的公理基础. 我们应该注意到大约在那个时期, 诸如群, 环, 域这样的抽象代数结构得到了引入, 而对于这些结构的研究开始了. 尽管如此, 那时数学家主要关注具体的代数结构, 例如整数集, 有理数集, 实数集, 等等. 本章所介绍的布尔代数是一种抽象代数结构, 其基本上是由Boole引入的. 显然, 布尔代数的定义来源于对于古典逻辑的行为的代数描述.

在给出包括格与布尔代数等的一些基本代数结构之后, 我们将会在第6.2节引入三个代数概念, 其基本上贯穿了我们整个第二部分的讨论. 本章的最后两节我们给出了逻辑与代数的联系的一些例子, 这是第二部分的主题.

第6.1节 格与布尔代数

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

一个偏序集$⟨A,\le ⟩$是由一个集合$A$和一个其上的偏序$\le$构成的序对. 一个集合上的一个偏序$\le$是一个全序 (或者说线序), 如果对于所有的$x,y\in A$, $x\le y$或者$y\le x$总是成立. 在这种情况下, $⟨A,\le ⟩$被称为是一个全序集, 或者说链. 关系$x<y$由条件$x\le y$但不$y\le x$定义, 其被称为(由偏序$\le$导出的)严格序. 显然, $x\le y$当且仅当$x<y$或$x=y$成立. 以下每张图 (Hasse图) 都表示了一个偏序集, 只有最左边的是一个链.

格

我们将给出格的基本等式.

根据定义, $\bigvee \varnothing$和$\bigwedge \varnothing$分别是$A$的最小元素$\perp$和最大元素$\top$. 因此, 完备格必然是有界的.

布尔代数

让我们回忆一下古典逻辑的逻辑联结词$\vee$, $\wedge$, $\to$的真值表, 其中$0$和$1$分别代表falsehood和truth.$$\begin{array}{ccc}a\backslash b& 1& 0\\ 1& 1& 1\\ 0& 1& 0\end{array}\begin{array}{ccc}a\backslash b& 1& 0\\ 1& 1& 0\\ 0& 0& 0\end{array}\begin{array}{ccc}a\backslash b& 1& 0\\ 1& 1& 0\\ 0& 1& 1\end{array}$$现在我们在集合$\{0,1\}$上定义一个自然的偏序, 即$0<1$. 那么, 左边和中间的真值表是说析取$a\vee b$与合取$a\wedge b$分别是相对于该偏序的join和meet. 当然, 我们注意到这种情况下join和meet也可以表达为$a\vee b=\max \{a,b\}$和$a\wedge b=\min \{a,b\}$.

运用代数的术语, 我们可以说$⟨\{0,1\},\vee ,\wedge ,\to ,0⟩$是一个代数, 其中$⟨\{0,1\},\vee ,\wedge ,0⟩$是一个带有最小元素$0$的格, 并且这个代数还有一个额外的运算$\to$, 其满足如果$a\le b$则$a\to b=1$, 不然的话$a\to b=0$. 藉由最小元素$0$, 我们定义$\neg a=a\to 0$. 显然, $\neg a=1$当且仅当$a=0$. 并且, 很容易看出来对于$a\in \{0,1\}$我们有$\neg \neg a=a$. 通过泛化, 我们按照以下方式引入了古典逻辑的代数.

由以上真值表所确定的代数$⟨\{0,1\},\vee ,\wedge ,\to ,0⟩$是一个布尔代数. 为了确认这点, 只需表明剩余律成立. 实际上, 我们可以看到$1\le b\to c$当且仅当$b\le c$当且仅当$1\wedge b\le c$, 也就是当$a=1$时的剩余律成立, 另外$a=0$时$0\le b\to c$和$0\wedge b\le c$总是都成立的. 这个由$0$和$1$构成的布尔代数被称为二值的, 记作$\mathbf{2}$.

剩余律是说对于每个$b,c$而言集合$U=\{x|x\wedge b\le c\}$中的最大元素总是存在且就等于$b\to c$. 实际上, 根据剩余律, 对于每个$x$而言, 如果$x\wedge b\le c$, 那么$x\le b\to c$. 这意味着$b\to c$是$U$的一个上界. 另一方面, 鉴于$b\to c\le b\to c$, 我们有$(b\to c)\wedge b\le c$, 通过使用剩余律的另一方向. 这意味着$b\to c\in U$, 故$b\to c=\max \{x\in A|x\wedge b\le c\}$. 现在考虑$b=c$这一特定情形. 鉴于$x\wedge b\le b$总是成立, 具有形式$b\to b$必然都是$A$的最大元素, 记作$1$. 这就推出了每个布尔代数既有最小元素$0$也有最大元素$1$. 布尔代数的一个病态例子是满足$0=1$的布尔代数. 这种布尔代数由单独一个元素$0$构成, 其被称为退化布尔代数. 之后的文本里我们提及布尔代数时, 除非另有说明, 不然我们总指的是一个非退化布尔代数. 以下的图片展示一个$8$-值布尔代数.

我们可以证明以下的引理6.2对于布尔代数成立, 但不需要使用双重否定律. 因此, 实际上这些结果对于Heyting代数也成立, 而Heyting代数的定义不过就是从布尔代数的定义里去掉双重否定律. Heyting代数将会在第7章详细讨论.

我们注意到引理6.3中出现的等式$x\vee \neg x=1$表达了排中律 (见第1.1节) 的某种代数类比. 另外, 以上的引理6.3是说$\vee$和$\to$可以基于$\wedge$和$\neg$定义, 也就是说$\vee$和$\to$在任何布尔代数之中都是冗余的. 另一方面, 为了使得布尔代数和之后章节将要引入的其他代数之间的比较更加清晰, 我们保留了将布尔代数定义为具有形式$⟨A,\vee ,\wedge ,\to ,0⟩$的五元组.

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

为了进一步发展我们的代数研究, 我们要引入三个基本的代数概念. 鉴于这些概念可以对于多种代数进行定义, 我们要在一般的上下文中进行定义. 代数的一个语言$\mathcal{L}$是一个运算符号的集合, 每个运算符号都有一个固定的元数, 元数是一个非负整数. 具有元数$0$的运算符号被称为常量符号. 以下我们假定$\mathcal{L}$是一个有限有序集$⟨f_1,f_2,\dots ,f_m⟩$, 遵循约定$n_1\ge n_2\ge \cdots \ge n_m$, 其中$n_i$是$f_i$的元数. 一个类型为$\mathcal{L}$的代数$\mathbf{A}$是一个具有形式$(A,{f_1}^{\mathbf{A}},{f_2}^{\mathbf{A}},\dots ,{f_m}^{\mathbf{A}})$的结构, 其中$A$是一个非空集合, 被称为$\mathbf{A}$的宇宙或者潜在集合, 而${f_i}^{\mathbf{A}}$是$A$上的一个$n_i$元运算, 其中$1\le i\le m$. 每个${f_i}^{\mathbf{A}}$都应该理解为$\mathcal{L}$的运算符号$f_i$在$\mathbf{A}$中的解释. 出于简洁性的考量, 有时我们会省略${f_i}^{\mathbf{A}}$的角标${}^{\mathbf{A}}$, 如果不至于引起误解.

举个例子, 前一节我们取了一个语言$⟨\vee ,\wedge ,\to ,0⟩$来描述所有布尔代数的类, 其元数分别为$2,2,2,0$. 以下的三个定义里, 我们将假定代数$\mathbf{A}$和$\mathbf{B}$具有相同的类型.

在由所有布尔代数构成的类这一情形下, $\mathbf{B}$是一个布尔代数$\mathbf{A}$的一个子代数当且仅当$B$是$A$的一个子集, 其包含$0^{\mathbf{A}}$且在$\vee ,\wedge ,\to$下封闭. 显然每个非退化的布尔代数都有一个同构于二值布尔代数$\mathbf{2}$的子代数. 当$\mathbf{A}$和$\mathbf{B}$都是布尔代数时, 一个映射$h:A\to B$是一个从$\mathbf{A}$到$\mathbf{B}$的同态当且仅当对于每个$⁎\in \{\vee ,\wedge ,\to \}$有$h(a{⁎}^{\mathbf{A}}{a}^{\prime })=h(a){⁎}^{\mathbf{B}}h(a^{\prime })$, 而且$h(0^{\mathbf{A}})=0^{\mathbf{B}}$.

对于任意的布尔代数$\mathbf{A}$, $\mathbf{A}$的每个子代数也是一个布尔代数. 另外, 如果$\mathbf{B}$是$\mathbf{A}$藉由某个同态$h$的一个同态像, 那么$\mathbf{B}$也是一个布尔代数. 为了证明后者, 我们验证$\mathbf{B}$满足布尔代数的三个条件. 对于第三个条件, 取任意元素$a^{\prime }\in B$. 然后, 对于某个元素$a\in A$而言$a^{\prime }$具有形式$h(a)$. 那么, $\neg \neg a^{\prime }=\neg \neg h(a)=h(\neg \neg a)=h(a)=a^{\prime }$, 鉴于$\mathbf{A}$是一个布尔代数. 至于剩余律, 对于给定的$a^{\prime },b^{\prime },c^{\prime }\in B$, 取$a,b,c\in A$使得$a^{\prime }=h(a)$, $b^{\prime }=h(b)$, $c^{\prime }=h(c)$, 因为$\mathbf{B}$是$\mathbf{A}$的一个同态像. 首先设$a^{\prime }\wedge b^{\prime }\le c^{\prime }$, 这等价于条件$h(a\wedge b)\le h(c)$. 既然$b\le a\to (a\wedge b)$在$\mathbf{A}$之中成立, 不等式$h(b)\le h(a)\to h(a\wedge b)\le h(a)\to h(c)$成立, 鉴于$h$是保序的. 因此, $b^{\prime }\le a^{\prime }\to c^{\prime }$. 反过来, 设$b^{\prime }\le a^{\prime }\to c^{\prime }$. 然后, $h(b)\le h(a\to c)$. 那么, 我们有$h(a)\wedge h(b)\le h(a)\wedge h(a\to c)\le h(c)$, 鉴于$a\wedge (a\to c)\le c$在$\mathbf{A}$中成立. 因此, $a^{\prime }\wedge b^{\prime }\le c^{\prime }$成立.

如果$\mathbf{B}$是布尔代数${\mathbf{A}}_j$ ($j\in J$) 的一个直积$\prod _{j\in J}{\mathbf{A}}_j$, 那么$\mathbf{B}$也是一个布尔代数, 这是因为$\mathbf{B}$的每个运算都是逐分量定义的. {译注: 并且, 布尔代数的定义也只是用到等式和等式之间的关系.} 为了总结, 我们按照以下方式陈述这些结果. 这个主题将会在第8.2节里以更泛化的方式进行讨论.

第6.3节 布尔代数的表示

在例子6.5和练习6.6中, 我们表明了任意一个集合$C$的幂集$\mathcal{P}(C)$相对于并$\cup$和交$\cap$构成了一个分配格$⟨\mathcal{P}(C),\cup ,\cap ⟩$, 其中$\varnothing$是最小元. 对于$C$的每个子集$X$, 令$-X$是$X$的补. 对于$X,Y\subseteq C$, 定义$X\to Y=-X\cup Y$. 那么, $\mathcal{P}(\mathbf{C})=⟨\mathcal{P}(C),\cup ,\cap ,\to ,\varnothing ⟩$形成了一个布尔代数. 具有这种形式的布尔代数被称为幂集布尔代数.

有限布尔代数

令$C$是任意一个具有$m$个元素的有限集合, 例如$\{a_k|1\le k\le m\}$. {译注: 这默认了当$i\ne j$时, $a_i\ne a_j$.} 那么, 幂集布尔代数$\mathcal{P}(\mathbf{C})$是一个$2^m$-值布尔代数. 如果$D$是另一个具有$m$个元素的集合, 那么显然$\mathcal{P}(\mathcal{D})$同构于$\mathcal{P}(\mathbf{C})$. 我们注意到

无限布尔代数

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

第1.1节所讨论的二值语义的每个赋值都确定了一种对于公式的解释. 赋值和有效性的概念可以自然地扩展至任意的布尔代数. 令$\mathbf{A}$是一个布尔代数. 一个$\mathbf{A}$上的赋值$h$是从所有命题变量的集合到$A$的任意映射. 赋值$h$可以自然地延拓成一个从所有公式的集合到集合$A$的映射, 通过定义$h(\alpha \vee \beta )=h(\alpha ){\vee }_{A}h(\beta )$, $h(\alpha \wedge \beta )=h(\alpha ){\wedge }_{A}h(\beta )$, $h(\alpha \to \beta )=h(\alpha ){\to }_{A}h(\beta )$, 以及$h(0)=0_A$. (藉由符号滥用, 对于这个延拓的映射我们也使用符号$h$. 以上的符号$\vee$, $\wedge$, $\to$, $0$代表逻辑联结词和常量, 而${\vee }_A$, ${\wedge }_A$, ${\to }_A$, $0_A$则代表相应的$\mathbf{A}$的代数运算以及$A$的最小元素, 以避免歧义.) 一个公式$\phi$在某个布尔代数$\mathbf{A}$中是有效的, 如果其总是取值$1_A$, 即对于每个$\mathbf{A}$上的赋值$h$总有$h(\phi )=1_A$. 公式有效性的概念也可以自然地扩展至相继式的有效性. 显然, 第1章所讨论的重言式不过就是在二值布尔代数$\mathbf{2}$中有效的公式和相继式.

第6.5节 多值链和剩余律

从代数角度而言, 询问如何将我们的二值语义 (即基于二值布尔代数的代数语义) 推广为多值语义是自然的. 本节我们将会考虑将二值语义扩展至多值语义的两种可能方式, 其将会取决于我们维持何种形式的剩余律. 我们将会引入两种类型的多值链, 即定义在全序集上的带有剩余律的代数. 它们分别是Gödel链和Łukasiewicz链. 之前章节引入的代数方法也可应用于这两种代数, 而两类不同的多值逻辑的基本结果也将呈现. 之后的章节我们将会进一步将这种想法推广至定义在格上的剩余代数, 并最终将我们引向Heyting代数和剩余格的概念.

作为对于二值语义的一种推广, 我们考虑如何为和古典逻辑相同的语言引入多值语义. 我们将我们这里的注意力限制于真值集合$A$为全序集的情况 (但可能无限), 即一个链, 并且带有最小元素$0$和最大元素$1$. 例如, 如果是三值语义, 我们可以取$A$为$\{0,1/2,1\}$. 在这种情形下, $1/2$会被视为halfway truth, 如果我们将真值理解为degree of truth. 因为我们假定了$A$为全序集, 那么$a\vee b$和$a\wedge b$分别可以表达为$\max \{a,b\}$和$\min \{a,b\}$. 因此, 主要的问题在于如何在这个集合上定义implication $\to$. 一种想法不过就是保持合取与implication之间的剩余律. {译注: 虽然这里的用辞是conjunction和implication, 但是实际上它们指的是代数运算而不是逻辑联结词, 只不过一般其会使用相同的符号罢了.}

首先设$\to$满足剩余律, 那么$\to$的定义必然要满足对于给定的$a,b\in A$, 对于所有的$d\in A$都有$d\wedge a\le b$当且仅当$d\le a\to b$. 这等价于说对于所有的$d\in A$都有$\min \{d,a\}\le b$当且仅当$d\le a\to b$. 若是的确如此 {译注: 指剩余律成立}, 我们可以表明如果$a\le b$就有$a\to b=1$, 否则的话$a\to b=b$. 这里我们注意到如果$a\le b$不成立, 那么$a>b$成立, 因为$\le$是全序的. 现在, 如果$a\le b$, 那么$\min \{d,a\}\le b$对于任意的$d$总是成立, 因而$d\le a\to b$必然对于任意的$d$成立. 这意味着$a\to b=1$. 接着, 如果$a>b$, 那么$\min \{b,a\}=b$, 而对于所有满足$d>b$的$d$都有$\min \{d,a\}>b$. 因此, $a\to b$必然等于$b$. {译注: 这里的讨论和布尔代数定义下面的讨论是如出一辙的.} 反过来, 设运算$\to$满足 (1) 当$a\le b$时有$a\to b=1$ (2) 否则的话, $a\to b=b$. 那么, 我们可以表明剩余律成立. 这是因为, 如果$a\le b$, 那么一边不等式$\min \{d,a\}\le a\le b$对于任意的$d$总是成立, 另一边不等式$d\le 1=a\to b$也对于任意的$d$总是成立. 当$a>b$时, 根据我们的假设有$\min \{d,a\}\le b$当且仅当$d\le b$当且仅当$d\le a\to b$. 最终, 我们也就是证明了以下结论.

Gödel链和Gödel逻辑

引理6.7暗示了以下定义. 现在设$A$是任意的链且具有最小元素$0$和最大元素$1$. 按照以下方式定义$A$上的三个运算$\vee$, $\wedge$, $\to$:

• $a\vee b=\max \{a,b\}$;
• $a\wedge b=\min \{a,b\}$;
• $a\to b=\{\begin{array}{cc}1& (a\le b)\hfill \\ b& (\text{否则的话})\hfill \end{array}$.

令$\mathbf{A}$是任意的Gödel链. 我们可以按照和布尔代数相同的方式定义$\mathbf{A}$上的赋值. 我们称一个公式$\alpha$在$\mathbf{A}$中是有效的当且仅当对于$\mathbf{A}$上的每个赋值$f$都有$f(\alpha )=1$. $\mathbf{A}$中所有有效公式的集合记作$\mathsf{L}(\mathbf{A})$. 如果对于某个数字$m$, $\mathbf{A}$同构于${\mathbf{G}}_m$, 那么集合$\mathsf{L}(\mathbf{A})$被称为$m$-值Gödel逻辑, 当$\mathbf{A}$无限时则称其为一个无限Gödel逻辑 (其由链$A$确定). 显然$\mathsf{L}({\mathbf{G}}_2)$等于经典逻辑Cl. 这些Gödel逻辑实际上在第5.4节的意义下是超直觉主义逻辑.

Łukasiewicz链

J. Łukasiewicz在他的论文 (Łukasiewicz, 1920) 中引入了一种链上的多值语义, 其和前一小节的并不相同. 他先引入了三值语义, 之后这被扩展为多值语义. 这一次, 三值情形里$0$和$1$之间的第三个值$1/2$被理解为了undeterminded或者说indeterminate.

第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)

本章我们将会给出对于剩余结构的简短引论, 其是亚结构逻辑的代数结构. 布尔代数和Heyting代数被定义为是带有二元运算$\to$的格结构, 其满足$\wedge$和$\to$之间的剩余律, 即$a\wedge b\le c$当且仅当$a\le b\to c$对于任意的$a,b,c$成立. 从另一方面来说, 第6章引入的Łukasiewicz推出并不总是满足此律. 但是, 其仍然满足融合运算$\cdot$和$\to$之间的剩余律.

本章我们将会讨论一般形式的剩余律成立的代数结构, 并且将注意力主要集中于剩余格. 这个概念是从代数角度理解亚结构逻辑的关键所在.

第9.1节 剩余格和FL-代数

第10章 模态代数

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

第10.1节 模态代数