本 Wiki 开启了 HTTPS。但由于同 IP 的 Blog 也开启了 HTTPS,因此本站必须要支持 SNI 的浏览器才能浏览。为了兼容一部分浏览器,本站保留了 HTTP 作为兼容。如果您的浏览器支持 SNI,请尽量通过 HTTPS 访问本站,谢谢!
Coursera 离散数学概论笔记:第二周
我的笔记均包含大量个人理解内容,存在一定偏差。如果您发现错误,请留言提出,谢谢!
命题公式如果按照真值的角度来分类的话,可以分为:重言式(Tautology)、矛盾式(Contradiction)与可满足式(Contingency)。这几种命题公式的特点如下:
几点需要注意的是:
重言式可以使用真值表证明。只要命题公式的真值表的最后一列(真值列)所有值都为 $1$,那么该命题公式一定是重言式。
命题公式之间有两种比较重要的关系:逻辑等价(Logical equivalent)和逻辑蕴含 (Logical implication)。
如果命题公式 $A↔B$ 是重言式时,则称 $A$ 逻辑等价于 $B$,记做 $A╞╡B$;该命题公式称为逻辑等价式。逻辑等价式反映了一种情况:任意的赋值下,逻辑等价的两个公式都等值。
E1.双重否定律
理解:双重否定等于肯定。
E1. ¬¬A╞╡A
E2.幂等律
E2. A∨A╞╡A,A∧A╞╡A
E3.E4.E5:交换律、结合律、分配律
E3. A∨B╞╡B∨A, A∧B╞╡B∧A //交换律
E4. (A∨B)∨C╞╡A∨(B∨C),(A∧B)∧C╞╡A∧(B∧C) //结合律
E5. A∧(B∨C)╞╡(A∧B)∨(A∧C),A∨(B∧C)╞╡(A∨B)∧(A∨C) //分配律
E6.德摩根律
记住只要打开括号合取 / 析取会翻转就可以。
E6. ¬(A∨B)╞╡¬A∧¬B, ¬(A∧B)╞╡¬A∨¬B
E7. 吸收律
E7. A∨(A∧B)╞╡A, A∧(A∨B)╞╡A
E8. 蕴含等值式
E8. A→B╞╡¬A∨B
E9. 等价等值式
E9. A↔B╞╡(A→B)∧(B→A)
E10.E11.E12.E13. 零律、同一律、排中律与矛盾律、非真既假
E10. A∨t╞╡t,A∧f╞╡f //零律
E11. A∨f╞╡A,A∧t╞╡A //同一律
E12. A∨¬A╞╡t, A∧¬A╞╡f //排中律和矛盾律
E13. ¬t╞╡f,¬f╞╡t //非真既假
E14. 级联加蕴含
E14. A∧B→C╞╡A→(B→C)
/* 推导过程:使用蕴涵等值式 、德摩根律 */
A∧B→C╞╡¬(A∧B)∨C ╞╡ (¬A∨¬B)∨C ╞╡ ¬A∨(¬B∨C) ╞╡ A→(¬B∨C) ╞╡ A→(B→C)
E15.假言易位
E15. A→B╞╡¬B→¬A
E16.归谬论
E16. (A→B)∧(A→¬B)╞╡¬A
E17.等价等值式II
E17. A↔B╞╡(A∧B)∨(¬A∧¬B)
命题公式还有一种很重要的关系:逻辑蕴涵。这种命题表现为蕴涵,即 $A→B$。如果这个命题是重言式,那么我们就称 $A$ 逻辑蕴涵 $B$,记做 $A╞B$。
关于逻辑蕴涵式,有几点需要注意的是:
I1: $A╞ A∨B$
理解:只要一个命题公式为真,那么它与任何公式合取都为真。
I2: $A∧B╞ A$ 和 $A∧B╞ B$
理解:如果$A$ 和 $B$ 合取成立,那么肯定能推出命题公式 $A$ 和 $B$ 都成立。
I3: $A∧(A→B)╞ B$
理解:一个命题公式成立,而且它可以推导出另外一个命题公式,那么另外一个命题公式也成立。该蕴涵式被称为分离规则,是非常重要的一个蕴涵式。
I4 : $(A→B)∧¬B╞ ¬A$
理解:命题公式 $A$ 可以推出 $B$,如果 $B$ 不成立,那么 $A$ 一定不成立。
I5: $¬A∧(A∨B)╞ B$
理解:命题公式 $A$ 不成立,如果命题 $A$ 和 $B$ 至少有一个成立,那么成立的肯定是 $B$。
I6: $(A→B)∧(B→C)╞ A→C$
理解:如果命题公式 $A$ 能推出 $B$,且 $B$ 能推出 $C$,那么 $A$ 一定能推出 $C$(蕴涵的可传递性)。
I7: $(A→B)∧(C→D)╞ (A∧C)→(B∧D)$
理解:命题公式 $A$、$C$ 如果能分别推出 $B$、$D$,那么$A$、$C$ 的合取也一定能推出 $B$、$D$ 的合取。
I8: $(A↔B)∧(B↔C)╞ A↔C$
理解:命题公式$A$、$B$ 等价,且命题公式 $B$、$C$ 等价,那么 $A$、$C$ 也等价(等价的可传递性) 。
逻辑蕴涵式往往被作为推理的公式使用,因此它经常被推广为条件加上结果的的形式,即:
$$Γ╞B$$
公式中的 $Γ$ (读作 Gamma) 代表了一系列的公式,(可以理解为前提条件公式的序列),而 $B$ 则是 $Γ$ 的逻辑结果。
很显然的是,该公式有几个特点:
逻辑等价式和逻辑蕴涵式都有其自身的特性,并在某种情况下可以转换。常见的特性有:自反、对称、传递。参考逻辑等价式和逻辑蕴涵式的定义和上述特性,我们可以总结出一些性质:
定义
自反性(显然的)
对称性
可传递性
其他
命题公式有两个比较重要的原理:代入原理和替换原理。
代入原理又称重言式代入原理。该原理定义如下:
将重言式 $A$ 中的某个命题变元 $p$ 的所有出现都代换为命题公式 $B$ , 得到的命题公式记作 $A(B/p)$,则 $A(B/p)$ 也是重言式。
因为重言式的真值恒为真,与 $p$ 的取值没有关系。因此,将所有的 $p$ 替换成 $B$ 以后得到的公式 $A(B/p)$ 也是重言式。 需要注意的是:
替换原理的定义如下:
将命题公式 $A$ 中的子公式 $C$ 的部分出现替换为和 $C $逻辑等价的 公式 $D$(即 $C╞╡D$),得到命题公式记做 $B$,可得:$A╞╡B$。
替换原理生效的原理是:$C$ 和 $D$ 在任何复制下都等值,因此用 $D$ 替换 $C$ 并不会影响 $A$ 的真值。
代入原理 | 替换原理 | |
---|---|---|
使用对象 | 永真式 | 命题公式 |
被代换对象 | 命题变元 | 子公式 |
代换对象 | 命题公式 | 与代换对象等价的命题公式 |
代换方式 | 代换同一命题变元的所有出现 | 代换子公式的某些出现 |
代换后结果 | 永真式 | 与原公式等价 |
常用的证明逻辑蕴涵式和逻辑等价式的方法有三种:真值表法、对赋值进行讨论、推演法。
真值表法:
对赋值进行讨论:
推演法:
证明:(A∨B)→C╞╡(A→C)∧(B→C)
/*先证明 (A∨B)→C╞ A→C)∧(B→C) */
/*证明 (A∨B)→C 为真,那么 (A∨B) 有两种情况,分别证明即可。*/
假设 a 为 (A∨B)→C 的成真赋值,那么有如下两种情况:
/*第一种情况*/
如果 a(A∨B) = F,那么显然有 a(A) = F,a(B) = F //析取为F, 那么元素应全为F
那么显然有 a(A→C) = T、a((B→C) =T //蕴涵在前提为假的情况下恒为真
因此在 a(A∨B) = F 的假设下, (A→C)∧(B→C) 为真。
/*第二种情况*/
如果 a(A∨B) = T,那么显然有 a(C) = T //蕴涵前提为真,那么结果必须为真才能保证命题为真
那么显然有 a(A→C) = T,a(B→C) =T
因此在 a(A∨B) = T下, (A→C)∧(B→C) 也为真。
得证。
/*再证明(A→C)∧(B→C)╞ (A∨B)→C */
假设 a 是 (A∨B)→C 的成假赋值,那么只有如下一种情况:
a(A∨B) = T,a(C) = F。
当 a(A) = T, a(C) = F,a(A→C) = F;
当 a(B) = T, a(C) = F,a(B→C) = F;
因此 当(A∨B)→C 为假,(A→C)∧(B→C) 恒为假。
得证。
证明:(A∨B)→C╞╡(A→C)∧(B→C)
(A∨B)→C ╞╡ ¬(A∨B) ∨C //蕴涵等值式,代入
¬(A∨B) ∨C ╞╡(¬A∧¬B)∨C //德摩根律。替换
(¬A∧¬B)∨C ╞╡(¬A∨C)∧(¬B∨C) //分配律,代入
(¬A∨C)∧(¬B∨C)╞╡(A→C)∧(B→C) //蕴涵等值式,替换
证明 A∧B╞¬A→(C→B)
A∧B
╞B //I2:A∧B╞A
╞¬C∨B //I1:A╞A∨B,代入
╞C→B //蕴涵等值式,代入
╞A∨(C→B) //I1:A╞A∨B,代入
╞¬A→(C→B) //蕴涵等值式,代入
我们知道一个命题公式有很多与其等价的公式。也就是说,某一个命题有很多种的表示方法。为了用规范的形式来描述命题,人们提出了一个概念范式。也就是说,在命题公式的多个逻辑等价的形式中,按照一定的规则找出较为符合标准或者规范的形式。
为了描述范式,人们制定了一个命题的范式应该具有的基本元素:
析取范式 (Disjunctive normal form)的定义如下:
公式 $A’$ 称作公式 $A$ 的析取范式,如果:
1. $A’╞╡A$
2. $A’$ 为合取子句或者若干合取子句的析取
一些例子如下:
合取范式(Conjunctive normal form)的定义如下:
公式 $A’$ 称作公式 $A$ 的合取范式,如果:
1. $A’╞╡A$
2. $A’$ 为析取子句或者若干析取子句的合取
一些合取范式的例子如下:
范式和组成它的元素一定是“相反”的;但是如果元素是命题公式,那么元素内部的关系一定和范式“相同”。
范式的求取主要利用逻辑等价式和代入 / 替换原理。主要的步骤如下:
¬p→¬(p→q)
╞╡¬p→¬(¬p∨q) //蕴涵等价式
╞╡p∨¬(¬p∨q) //蕴含等价式
╞╡p∨(p∧¬q) // 德摩根律:析取范式
╞╡(p∨p)∧(p∨¬q) //分配律
╞╡p∧(p∨¬q) // 合取范式
╞╡p
范式的一个重要的作用就是可以识别重言式和矛盾式。我们一般使用合取范式识别重言式,用析取范式识别矛盾式。
尽管我们制定了一些规则来撰写命题公式的规范公式,但实际上范式自身也有很多种等价的形式,只要满足规则的形式,都可以称作范式。换句话说,一个公式的范式都不是唯一的。比如如下的例子:
而甚至在某些情况下,合取范式和析取范式可以相同,比如:
由上一节的范式的唯一性可知,范式不是唯一的。因此,为了更好的规范化我们的命题公式的写法,我们需要一种具有唯一性的范式。这种范式,我们称为主范式。
根据组合关系的不同,主范式也同样分为主合取范式和主析取范式。
前面说过,主析取范式和主合取范式最大的优势就是其唯一性。为了精确的表达这个唯一性,我们需要引进两个概念:极小项和极大项。
极小项(Min term)可以通俗的描述如下:
前面的析取范式中主要存在两个问题导致了析取范式的不唯一性:互补文字对与文字的重复。而极小项通过对命题变元的排序,和限制命题变元的出现改善了上述的两个问题。总的说来,就是控制了析取元素的长度与顺序。
我们还注意到极小项记做 $M_i$。这里的下标 $i$ 也是有含义的:
具体的例子如下图:
<html>
<img src=“/_media/math/math_note/gen_discrete_math/minterm.svg” width=“300”>
</html>
上图中,我们的 $i$ 值的二进制就是 $100$,转化成十进制就是 $4$。因此,转化成对应的极小项表示,就是 $M_4$。
需要注意的是:
极大项与极小项非常相似。相对于极小项使用合取的方式来产生字符串,极大项使用了析取的方式来产生字符串。根据上面对极小项的分析,对于一个 $n$ 项的合取范式(必须经过排序和长度控制),它所拥有的极大项也拥有 $2^n$ 种。而正是因为极大项使用析取,因此对于极大项的真值为假的情况是唯一的;也就是说,对于极大项的编码,其值是针对于假的情况来进行编码的。
需要注意的几个性质:
主析取范式(Major disjunctive form)的定义如下:
公式$A’$ 称作公式 $A(p_1,p_2,…p_n)$ 的主析取范式,如果:
1. $A’$ 是 $A$ 的析取范式
2. $A’$ 中每一个合取子句里 $p_1,p_2,…p_n$ 均恰出现一次
主合取范式(Major conjunctive form)的定义如下:
公式 $A'$ 称作公式 $A(p_1, p_2, …p_n)$ 的主合取范式,如果:
1. $A'$ 是 $A$ 的合取范式
2. $A'$ 中每一个析取子句里 $p_1, p_2, …p_n$ 均恰出现一次
以主析取范式为例。前面说到,主析取范式实际上由极小项合取而成。显而易见的而是:
如果我们需要用到主范式来代表一个命题公式,那么我们必须证明主范式是存在的,并且是唯一的,即:
任何命题公式 $A(p_1, p_2, …p_n)$ 的主析取范式都是存在的,并且是唯一的。
以主析取范式为例子,先来看看存在性的证明。
存在性的证明非常简单,只要证明从一般的析取范式的形式通过已有的定理可以推导出主析取范式的形式就行了。下面是证明的过程:
再来看看唯一性的证明(反证法):
确定了的主范式的存在性与与唯一性以后,我们可以按照主范式对命题公式进行分类。同样以主析取范式为例,我们可以声明如下的分类规则:
凡是具有相同主析取范式的命题公式都是等值的,它们属于同一个等值类。
我们知道,一个包含 $n$ 个命题变元的命题公式的的极小项有 $2^n$ 种情况;因为主析取范式由极小项组成,因此,主析取范式的组合情况有 $2^{2^n}$ 种可能。很显然的是,等值类的数量与主析取范式的数量是相同的。
主合取范式与主析取范式是对称的。它由极大项析取而来,下标的二进制的 $1$ 表示该位对应的命题变元是负文字。
看完了主范式的介绍,我们有一个问题:为什么主范式只用三个联结词就能表示所有的命题公式?为了解决这个疑惑,我们需要讨论一下联结词的完备性。
真值函数的概念在第一章介绍过。在这里需要注意的是:
一些理解: 真值函数本身就被理解为命题公式的函数形式,也就是从抽象的方式去判断命题公式的真值。就像是函数一样,如果命题公式的命题变元有所变化(也就是真值函数的自变量有所变化),那么真值函数也会有对应的真值。因此,说真值函数与等值类一一对应是没有问题的;所有的等值类下的命题公式对于相同的赋值都会返回相同的真值;这也是我们在研究命题逻辑时最关心的结果。因此,将命题公式函数化(抽象化),是有必要的。
功能完备集的定义如下:
如果任意一个真值函数都可以用仅包含某个联结词集中的联结词的命题公式表示,则称这个联结词集为功能完备集。
比如目前使用的 ${¬,∧,∨,→,↔}$ 是功能完备集,而主析取范式使用的 ${¬,∧,∨}$ 也是功能完备集(主析取范式可以表示任意真值函数)。
我们注意到功能完备集可以有很多种形式,比如 ${¬,∧,∨,→,↔}$ 、 ${¬,∧,∨}$ 。但前者跟后者相比,多出了蕴涵和双蕴涵联结词。而蕴涵实际上是可以用析取、合取和否定来表示的;象蕴涵这种可以用集合中其他的联结词来定义的联结词,我们称为冗余联结词。
如果一个功能完备集不包含任何冗余联结词,我们就称这个功能完备集为极小集。一些典型的极小集如下:
而证明一个联结词的集合是否是完备集,实质上是证明该集合是否能从一个已知的功能完备集中去掉冗余联结词,直到得到目标集合。来看一个例子:
除了以上提到的极小集以外,我们还有一些仅包含单个联结词的功能完备集。其中一个典型的例子就是皮尔斯记号:定义联结词 ${↓}$。它的定义是:$p↓q╞╡¬(p∨q)$。推演的过程如下:
/*证明思路:如果能用 ↓ 表示已知功能完备集中的每一个联结词,那么就说明 {↓} 也是完备集*/
¬p╞╡¬(p∨p)╞╡p↓p //用 ↓ 代表 ¬p
p∨q╞╡¬¬(p∨q)╞╡¬(p↓q)╞╡(p↓q)↓(p↓q) //用 ↓ 代表析取
因为 {¬, ∨} 是功能完备集,那么 {↓} 也是功能完备集。
不过反过来,证明某个联结词的集合是不是功能完备集是比较麻烦的,因为没有比较统一的办法。比如如下例子:
如果希望更好的理解形式系统,推荐阅读 计算的极限(八):符号的框架,还有 GEB 这本书。
让我们回到本节课的开头。我们将某些自然语言的逻辑推理的过程写成了字符加上符号的形式,而结果则用真值来表示。比如如下的例子:
这是一个非常简单的,符合直觉逻辑的推理过程,用之前课程中我们学到的符号和规则来表示则有:
如果命题 $A$ 表述小明是全班第一名,命题 $B$ 表述小明会拿奖,那么整个推理过程和结果可以写成:$A∧(A→B)╞B$。
其实你如果一直学下来,你可能也跟我有同样的疑问:如果上面的符号到底跟之前的自然语言表述的推理有什么关系?为啥非得用这一堆字符串来表述这个过程呢?
之前有提过,因为自然语言的不严谨,和潜在的二义性,导致很多人希望找到一种严谨的、用计算的方式来实现逻辑推理的过程。在上面的例子中,我们就创建了一套符号来代表命题,一套联结词来代表关系,从而将自然语言的推理过程转换成了符号形式的计算过程。但这里有一个非常重要的问题:我们定义的这些符号,如果脱离了赋予它的意义,那上面的这一段字符串,本身根本就没有任何意义了。
实际上,这个问题完全可以反过来想。我们自己创建的符号和联结词,本身是没有意义的;换而言之,它就可以具有任何意义。按上面的例子来说,$A∧(A→B)╞B$ 中的 $A$,既可以表示小明拿奖,也可以表示小李拿奖。这一套符号化的系统,可以代表一系列的推理过程相同的自然语言,是不是很强大?
更厉害的是,这一套系统,如果我们赋予它一些基本的,不证自明的命题;再制定一些关于这些字符的联结(运算 / 推理)规则,那么我就能通过这一些内容,来源源不断的推出一些推论了。这一套系统到了现在,甚至可以交给计算机自行推理。这一套符号体系,实际上就是我们所说的形式系统。
来看一看一个典型的形式系统需要哪一些内容:
首先,我们需要一些基石,一些不证自明的命题(重言式)。这些命题是我们所有的推论的来源,我们称之为公理(Axioms)。在形式系统中,我们用符号来表示公理。
接下来,我们需要一套规则,也就是一套文法。这套规则从形式上说明了符号之间是如何组织的,如何变化的,而从意义上来说,则代表了整个推理的过程。组织符号的规则,我们称之为命题公式;而命题公式变换的规则,我们称之为推理规则(Rules of inference)。需要注意的是,推理规则必须是由重言式导出重言式的过程,也就是所谓的真理才能推导出真理。
有了公理,和确保可以由正确结果得到正确结果的推理规则,我们就可以利用这一套系统来进行推理结论了,我们把这些由公理和推理规则推导而来的结论称之为定理(Theorem)。而这些推导的过程可以分为两个部分:证明和演绎(Proof & Deduction)。
证明的定义如下:
公式序列 $A_1,A_2,…,A_m$ 称作 $A_m$ 的一个证明,如果 $A_i(1≤i≤m)$:
1. 或者是公理;
2. 或者由 $A_{j1},…,A_{jk}(j1,…,jk<i)$ 用推理规则推得。
当这样的证明存在时,称 $A_m$ 为系统的定理,记作 $┠*A_m$ (*是形式系统的名称),或者简记为 $┠A_m$
用通俗的话来解释,就是证明是一个用已知公理或者定理,根据制定的推理规则,得到定理的过程。
再来看看演绎的定义:
设 $Γ$ 为一公式集合。公式序列 $A_1,A_2,…,A_m$ 称作 $A_m$ 的以 $Γ$ 为前提 的演绎,如果$A_i(1≤i≤m)$:
1. 或者是 $Γ$ 中的公式
2. 或者是公理
3. 或者由$A_{j1},…,A_{jk}(j1,…,jk<i)$用推理规则推得。
当有这样的演绎时,$A_m$ 称作 $Γ$ 的演绎结果,记作 $Γ┠*A_m$ (*是形式系统的名称),或者简记为 $Γ┠A_m$
此时称 $Γ$ 和 $Γ$ 的成员为 $A_m$ 的前提(Hypothesis)。
用通俗的话来解释:$A_m$ 之前的公式序列被称为以 $Γ$ 为前提的演绎(也就是推导过程)。$A_i$ 要么是 $Γ$ 里面的公式,要么是公理,要么是这两者根据规则推导而来。
而且我们仔细观察一下就会发现,证明其实是演绎的一个特例。当 $Γ$ 为一个空集的时候,也就是没有前提的情况下,演绎的过程就是证明的过程。
命题演算形式系统(Proposition Calculus) 是基于命题以及重言式构造的形式系统,简称 PC。既然是形式系统,那么 PC 一定是符号系统。
前面提到形式系统由符号系统,规则,公理组成。按照该定义,我们来看看来看一看 PC 由哪些部分组成:
首先是 PC 的符号系统:
接下来是符号的组合规则,也就是命题公式。规则大概有如下三条:
再者是 PC 系统的公理。假设 $A,B,C$ 表示任意公式,PC 采用了如下三个公式作为公理:
最后是 PC 系统的推理规则。PC 的推理规则只有一条:分离规则;即在证明演绎的过程中,如果有 $A$ 和 $A→B$,就能推出 $B$,记做 $A,A→B/B$。
对于一个形式系统来说,除了添加相应的组成元素以外,我们还需要确保它是一个“好”的形式系统。一个好的形式系统需要有以下三个特性:
PC系统是基于人类逻辑系统而构造的,因此PC系统的组成也是需要合乎逻辑的。这种合乎逻辑的表现大致表现为如下两个方面:
可以看出来的是,PC 系统的构造始终围绕着逻辑来设计的。那么,我们是怎么确保这一系列设定是合乎逻辑的?
我们可以从形式系统的概念下手。既然要确定定理与推导过程合乎逻辑的,我们需要 PC 系统中的基础组成部分也合乎逻辑:
通过确保这两个部分的逻辑性,我们就能确保在 PC系统内,由公理和规则推导出的定理都是合乎逻辑的;同时,由合乎逻辑的前提、公理、推理规则所推导出的公式,也是合乎逻辑的。
所谓的一致性,就是保证 PC 系统内任何的命题不会出现逻辑上的自相矛盾,即没有公式 $A$,使得$┠_{PC}A$ 和 $┠_{PC}¬A$ 同时成立。由 PC 系统的合理性我们可以知道,如果 $A$ 是定理,那么它必然是逻辑真理。按照矛盾律,逻辑真理的非必然不是逻辑真理;这就说明了 PC 系统是具有一致性的。
所谓的完备性,就是说在 PC 系统中,只要是合乎逻辑的命题,就一定能够推导出来。(课程中没有给出证明)
完备性可以大致分为两部分:
证明:┠PC A→A
第1步:(A→((A→A)→A))→((A→(A→A))→(A→A)) //用(A→A) 替换 B,A 替换 C,再套用公理A2得到
第2步:A→((A→A)→A) //用(A→A) 替换 B,A 替换 C,再套用公理 A1 得到
第3步:(A→(A→A))→(A→A) // 发现第二步得到的推论是第一步推论的前件,由分离规则得到本步骤的推论
第4步:A→(A→A) // 再次使用公理 A1,用 A 分别替换 B 和 C
第5步:A→A //第四步的结论是第三部的前件,由分离规则可得到本步结论,得证。
演绎:{A,B→(A→C)}┠B→C
/*由题可知本题有两个前提*/
前提1:A
前提2:B→(A→C)
/*正式演绎*/
第1步:A→(B→A) // 将 B 替换为 A,使用公理A1
第2步:B→A // :对前提1和第一步使用分离规则
第3步:(B→(A→C))→((B→A)→(B→C)) //对前提2 应用公理 A2
第4步:(B→A)→(B→C) //对前提2和第三步使用分离规则
第5步:B→C //对第二步和第四步使用分离规则,得证。
使用 PC 系统的公理和规则来证明一些复杂命题的时候,我们往往需要想方设法的去凑出能证明结论的形式。这样做有时候是非常麻烦的;为此,我们可以总结出一些定理,来帮助我们简化整个命题过程。PC 系统中主要使用的这种类型的定理有三个,我们也称之为三个元定理。
为什么要称作元定理?元是对英文 Meta 的翻译,Meta 的本身意思就是描述事物的事物。比如 Metadata,就是用于描述数据的数据,比如数据的采集者,采集时间等等。因为我们要讨论的这些定理,他们并不是 PC 系统中的定理(没有在 PC系统中证明过的定理),而是用于描述如何证明定理的定理,因此,这三个定理被称为元定理。
演绎定理的定义如下:
对任意公式集合 $Γ$ 和公式 $A,B$:
1. $Γ┠A→B$ 当且仅当 $Γ∪{A}┠B$
2. 当 $Γ=ø$ 时,$┠A→B$ 当且仅当 ${A}┠B$,或 $A┠B$
从形式上来看,就是把右边蕴涵关系里的 $A$,移到了左边作为前提条件的一部分。
而这个定理用自然语言来描述就是:
必要性:
当 A→B 是定理的时候, 根据分离规则,A 可推出 B。
因此 Γ∪A 也能推出 B。
充分性:
从 Γ∪A┠B 可以得知, B 成立。
将 B 和 A 代入公理 A1,有:B→(A→B)
根据分离规则,有 A→B 成立。
归谬定理又称为反证法,其定义如下:
对任意公式集合 $Γ$ 和公式 $A,B$:
1. 若 $Γ∪{¬A}┠B,Γ∪{¬A}┠¬B$
2. 那么 $Γ┠A$
试想一下,如果一组前提能同时推出另一个命题的正反面,那么这组前提里肯定有相互矛盾的命题在里面。那么很显然,如果我们对产生矛盾的某个命题做一个否定,那么这个命题的否定是肯定被前提集合所包含的,也肯定能被前提集合所推出。
穷举定理的定义如下:
对任何公式集合 $Γ$ 和公式 $A,B$
1. 若 $Γ∪{¬A}┠B,Γ∪{A}┠B$
2. 那么 $Γ┠B$
穷举定理的意义在于如果一个前提能推出结论,这个前提 的反面也能推出同样的结论,说明结论的成立与此前提是否成立无关。既然无关,那么 $A$ 与前提集合就没有什么关系了,因此可以去掉。
证明:┠¬¬A→A
第一步:¬¬A→(¬A→¬¬A) //由公理 A1 可得
第二步:{¬¬A,¬A }┠¬¬A //演绎定理
第三步:¬A→(¬¬A→¬A) // 公理A1
第四步:{¬A, ¬¬A} ┠¬A // 演绎定理
第五步:{¬¬A} ┠A //因为第三步和第五步推出的结果自相矛盾,因此利用归谬定理(左边可以想象成{¬¬A}∪{¬A})
第六步:┠¬¬A→A //演绎定理
证明:┠(A→C)→(((B→C)→((¬A→B)→C))
第一步:{¬A→B, B→C, A→C}┠C //演绎定理,将嵌套的前件按顺序移到左边(只是变形)
/*接下来利用穷举定理证明第一步的变形*/
第二步:{¬A→B, B→C, A→C,A}┠C // 往前提集合里添加一个 A,因为有 A→C,那么推出 C是显然的
第三步:{¬A→B, B→C, A→C,¬A}┠C // 往前提集合里添加一个¬A,因为¬A→B, B→C,那么也能推出 C
第四步:{¬A→B, B→C, A→C}┠C //根据穷举定理,{¬A→B, B→C, A→C} ∪¬A 或者 A 都能推出 C,因此这个集合能直接推出 C,得证。
我们判定一个定理是否成立,实际上就是看能否找到该定理之前的证明序列。而我们知道,在形式系统中有三个部分:符号系统、公理、推理规则。通过这三个基本元素进行推演,我们就能得到定理。由于形式系统是符号系统,因此,我们得到的定理实际上就是使用一系列构造规则,通过有限步的构造产生的特定字符串。因此可以说,定理在形式系统中的证明过程,就是符号的构造过程;而定理本身在形式系统中的状态,就是一个字符串。
明白了以上内容以后,那么判定一个定理是否是某个形式系统中的定理,实际上就是能不能找出这个字符串在该形式系统中的构造过程了。不过有时候,这个过程会很 tricky。我们来看看下面这个有趣的例子:
这个例子描述了一个简单的形式系统 MIU,来自 GEB 书中。这个 MIU 系统的定义如下:
看完上述之后,我们有一个问题:能否能判定 MU 是 MIU 形式系统中的定理呢?
结论是 MU 并不属于 MIU 系统。但很遗憾的是,这个结论并不是直接使用 MIU 系统里的公理和规则推出来的。倘若该字符串不属于本形式系统,我们肯定无法在有限步骤内找到这个字符串的。这样就很尴尬了;你也不能证明它存在,也不能证明它不存在。幸好聪明的数学家们提出了另外一个方法:同构。
什么是同构?同构就是构造另外一个形式系统。该形式系统与之前的形式系统结构相同,只是使用了另外的符号来代表。针对于 MIU 系统,人们构造了一个新的形式系统 310:即用数字 3 代替 M,用数字 1 代替 I,用 数字 0 代替 U。
经过这么一代替之后,我们发现之前的 MIU 系统,已经被我们改造为一个自然数的系统了。很显然,既然牵涉到自然数,我们就可以使用一些数论的结论来讨论 310 的一些性质了。接下来我们接着做一些翻译的工作:
那么问题也可以翻译成:30 是不是该集合中的数?
有了以上信息,我们再来分析一下这个问题应该怎么证明:
3
整除。3
整除3
整除的数3
整除的既然证明了 30 不属于系统 310,那么很显然,MU 也是不属于 MI 的了。
可以看到的是,如果仅通过形式系统本身的公理 \ 规则,是很难(或者说不可能)在有限的步骤内判定一个命题公式是否是该形式系统内的定理的;PC 系统也是如此。而同构的方式可以很好的解决这个问题。 PC 系统本身也具有自己的同构系统:真值函数运算系统。因此,判定 PC 系统中的命题公式是否为定理就非常简单了:我们只需要用真值表判断命题公式对应的真值函数是否是重言式,就可以判断该命题公式是否是 PC 中的定理。 而利用真值表计算代替使用PC系统自身元素推演,就像是利用数论解决MIU系统的难题一样,有一个最大的优势:前者的计算都是可以在有限步骤内完成的。