离散数学[3]-数理逻辑-命题逻辑及形式系统

一、重言式

1.命题公式的分类

命题公式可以从真值的角度进行分类：

• 重言式:(永真式)tautology 命题变元的所有赋值都是命题公式的成真赋值
• 矛盾式(永假式、不可满足式) contradiction 命题变元的所有赋值都是命题公式的成假赋值
• 可满足式(contingency) 命题公式至少有一个成真赋值

需要分清的概念：

• 永真式都是可满足式
•  矛盾式都不是可满足式
•  非永真式并不都是永假式
•  如果A是永真式，则¬A就是永假式， 反之亦然

重言式的例子和证明

例子:对于任何公式A

• A∨¬A是重言式(排中律)
•  A∧¬A是矛盾式(矛盾律)
•  采用命题公式的真值表证明重言式 : 证明(p∨q)∧¬p→q是重言式

二、逻辑等价式和逻辑蕴涵式

逻辑等价式(logical equivalent)

•  当命题公式A↔B是重言式时，则称A 逻辑等价于B，记作A╞╡B，称作逻 辑等价式
• 也可以理解为公式A和公式B等值
• 逻辑等价体现了两个公式之间的一种 关系:在任何赋值状况下它们都等值

一些重要的逻辑等价式(A,B,C是任意公式)

1.  E1:¬¬A╞╡A(双重否定律)
2.  E2:A∨A╞╡A，A∧A╞╡A(幂等律)
3.  E3:A∨B╞╡B∨A， A∧B╞╡B∧A(交换律)
4.  E4:(A∨B)∨C╞╡A∨(B∨C)，(A∧B)∧C╞╡A∧(B∧C)(结合律)
5.  E5:A∧(B∨C)╞╡(A∧B)∨(A∧C)，A∨(B∧C)╞╡(A∨B)∧(A∨C)(分配律)
6.  E6:¬(A∨B)╞╡¬A∧¬B， ¬(A∧B)╞╡¬A∨¬B(德摩根律)
7.  E7:A∨(A∧B)╞╡A， A∧(A∨B)╞╡A(吸收律)
8.  E8:A→B╞╡¬A∨B(蕴涵等值式)
9. E9:A↔B╞╡(A→B)∧(B→A)(等价等值式)
10.  E10:A∨t╞╡t，A∧f╞╡f(零律)
11.  E11:A∨f╞╡A，A∧t╞╡A(同一律)
12.  E12:A∨¬A╞╡t， A∧¬A╞╡f(排中律和矛盾律)
13.  E13:¬t╞╡f，¬f╞╡t
14.  E14:A∧B→C╞╡A→(B→C)
15.  E15:A→B╞╡¬B→¬A(假言易位)
16.  E16:(A→B)∧(A→¬B)╞╡¬A(归谬论)
17. E17:A↔B╞╡(A∧B)∨(¬A∧¬B)(等价等值式2)

逻辑蕴涵式(logical implication)

• 当命题公式A→B是重言式时，则称A逻辑蕴涵B，记作A╞B，称作逻辑蕴涵式, 也可以理解为公式A的所有成真赋值都是公式B的成真赋值
•  每个逻辑等价式可以看作两个逻辑蕴涵式， 也就是说A╞╡B也有A╞B,B╞A A和B等值，所以A→B和B→A都是重言式
• 逻辑蕴涵体现了两个公式AB之间的另一种 关系:在任何赋值状况下只要A真，B都真

一些重要的逻辑蕴涵式(A,B,C是任意公式)

•  I1:A╞A∨B
•  I2:A∧B╞A
•  I3:A∧(A→B)╞B
•  I4:(A→B)∧¬B╞¬A
•  I5:¬A∧(A∨B)╞B
•  I6:(A→B)∧(B→C)╞A→C
•  I7:(A→B)∧(C→D)╞(A∧C)→(B∧D)
•  I8:(A↔B)∧(B↔C)╞A↔C

逻辑结果

•  逻辑蕴涵经常会被推广为Γ╞B的形式
•  其中Γ是一系列公式，表示B是Γ的逻辑结果
•  即:使Γ中每一个公式成真的赋值，都是公 式B的成真赋值
•  即Γ中的所有公式的合取逻辑蕴涵B
•  当Γ中仅包含一个公式A时，就是A╞B;
•  如果Γ中不包含任何公式，记做╞B，表示 “B永真”

逻辑等价式和逻辑蕴涵式的几个重要性质

•  命题公式关系的自反、对称、传递等性质
•  A╞╡B当且仅当╞A↔B
•  A╞B当且仅当╞A→B
•  若A╞╡B，则B╞╡A
•  若A╞╡B， B╞╡C，则A╞╡C
•  若A╞B，则¬B╞¬A
•  若A╞B， B╞C，则A╞C
•  若A╞B，A╞╡A’，B╞╡B’，则A’╞B’

三、代入原理和替换原理

重言式的代入原理(rule of substitution)

• 将重言式A中的某个命题变元p的所有出现都代换为命题公式B， 得到的命题公式记作A(B/p)，A(B/p) 也是重言式。
• 因为重言式A的真值与p的取值状况无关，恒为t，
• 所以将p全部代换后的公式A(B/p)的 真值也恒为t

注意:仅代换部分出现本原理不成立， 为什么? 注意:如果B中包含了p或者A中的其它变元，本原理还成立么?

• 将命题公式A中的子公式C的部分出 现 替 换 为 和 C 逻 辑 等 价 的 公 式D (C╞╡D )， 得到的命题公式记作B，则A╞╡B。
•  因为C和D(在任何赋值下)等值，所以用D替换C不会改变A的真值 〉 注意:不要求全部出现都替换

代入原理RS与替换原理RR的区别

代入原理RS 替换原理RR
使用对象 任意永真式 任意命题公式
代换对象 任意命题变元 任意子公式
代换物 任意命题公式 任意与代换对象等价的命题公式
代换方式 代换同一命题变元的所有出现 代换子公式的某些出现
代换结果 仍为永真式 与原公式等价

四、证明逻辑等价式和蕴涵式

证明逻辑等价式和逻辑蕴涵式

• 真值表法:要证明A╞╡B，A╞B，只要: 分别列出A↔B和A→B的真值表，最后一列全为真即可。
•  对赋值进行讨论:要证明A╞B，只要证明: A的任意一个成真赋值都是B的成真赋值，或者 B的任意一个成假赋值都是A的成假赋值。 如果证明了A╞B和B╞A，那么就证明了A╞╡B。
•  推演法:利用已知的重言式、逻辑等价式和逻辑蕴涵式，采用代入原理和替换原理进行推演。

讨论赋值法证明逻辑等价式:(A∨B)→C╞╡(A→C)∧(B→C)

〉 先证明(A∨B)→C╞(A→C)∧(B→C)
〉 假设α是(A∨B)→C任意一个成真赋值，这样会有两种情况: 〉 α(A∨B)=f:于是α(A)=α(B)=f，就有α(A→C)=α(B→C)=t 〉 或者，
〉 α(A∨B)=t，α(C)=t:于是α(A→C)=α(B→C)=t
〉 上述两种情况都得到α((A→C)∧(B→C))=t，得证。

讨论赋值法证明逻辑等价式:(A∨B)→C╞╡(A→C)∧(B→C)

〉 再证明(A→C)∧(B→C)╞(A∨B)→C
〉 反过来，假设α是(A∨B)→C任意一个成假赋值，这样只有一种情况: 〉 α(A∨B)=t，α(C)=f
〉 当α(A)=t，α(C)=f时，α(A→C)=f;
〉 当α(B)=t，α(C)=f时，α(B→C)=f，
〉 不管如何，都有α((A→C)∧(B→C))=f
〉 得证。

推演法证明逻辑等价式:(A∨B)→C╞╡(A→C)∧(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)(蕴涵等值式，代入)

五、范式及基本术语

范式:概念及基本术语

•  每个命题公式都会存在很多与之逻辑 等价的公式
•  范式:在命题公式的多个逻辑等价的形式中，较为符合“标准”或“规范” 的一种形式

范式:概念及基本术语

•  文字(literals):命题常元、变元和它们的否定
•  前者称正文字，后者称负文字，如:p,¬q,t
•  析取子句(disjunctiveclauses):文字或者若干文字的析取， 如:p, p∨q, ¬p∨q
•  合取子句(conjunctiveclauses):文字或者若干文字的合取， 如:p, p∧q, ¬p∧q
•  互补文字对(complemental pairs of literals):指一对正文字和 负文字，如:p和¬p

析取范式(disjunctive normal form)

公式A’称作公式A的析取范式，如果:

1. A’╞╡A
2.  A’为合取子句或者若干合取子句的析取

〉 p→q的析取范式为¬p∨q(合取子句¬p 和q的析取)
〉 ((p→q)∧¬p)∨¬q的析取范式为 ¬p∨(q∧¬ p)∨¬q

合取范式(conjunctive normal form)

公式A’称作公式A的合取范式，如果:

1. A’╞╡A
2.  A’为析取子句或者若干析取子句的合取

〉 p→q的合取范式为¬p∨q(析取子句 ¬p∨q)
〉 ((p→q)∧¬p)∨¬q的合取范式为 (¬p∨t)∧(¬p∨¬q)或¬p∨¬q

六、求范式一般步骤

求命题公式的范式

〉 利用逻辑等价式和代入原理、替换原理，可 以求出任一一个公式的析取范式和合取范式
〉 求¬p→¬(p→q)的析取范式及合取范式
〉 ¬p→¬(p→q)
〉 ╞╡¬p→¬(¬p∨q)
〉 ╞╡p∨¬(¬p∨q)
〉 ╞╡p∨(p∧¬q)(析取范式)
〉 ╞╡(p∨p)∧(p∨¬q)
〉 ╞╡p∧(p∨¬q)(合取范式)
〉 ╞╡p

范式用于重言式和矛盾式的识别

〉 重言式识别
〉 合取范式中每个析取子句都包含了至 少一个互补文字对: (p∨¬p∨q)∧(p∨q∨¬q)
〉 矛盾式识别
〉 析取范式中每个合取子句都包含了至 少一个互补文字对: (p∧¬p∧q)∨(p∧q∧¬q)

求析取范式或合取范式的一般步骤

〉 消去公式中的联结词→和↔
〉 p→q化为¬p∨q(蕴涵等值式)
〉 p↔q化为(¬p∨q)∧(p∨¬q)或者(p∧q)∨(¬p∧¬q)(等价等值式)
〉 利用德摩根律将否定联结词¬向内深入，最后只作用于文字，再将 ¬¬p化为p
〉 利用分配律，最后得到需要的析取或者合取范式

范式的唯一性问题

〉 一个公式的析取范式或合取范式都不是唯一的
〉 p,p∨(p∧¬q),(p∧q)∨(p∧¬q)都是¬p→¬(p→q)的析取范式 
〉 p,p∧(p∨¬q),(p∨q)∧(p∨¬q)都是¬p→¬(p→q)的合取范式 〉 公式的析取范式有可能同时又是合取范式
〉 ¬p∨q既是p→q的析取范式又是合取范式
〉 能否找到“最为规范”的范式?
〉 具备唯一性的范式

七、主范式

主范式的定义

〉 主析取范式(majordisjunctiveform)
〉 公式A'称作公式A(p1,p2,...pn)的主析取范式，如果: 
〉 A'是A的析取范式
〉 A'中每一个合取子句里p1,p2,...pn均恰出现一次
〉 主合取范式(majorconjunctiveform)
〉 公式A'称作公式A(p1,p2,...pn)的主合取范式，如果: 
〉 A'是A的合取范式
〉 A'中每一个析取子句里p1,p2,...pn均恰出现一次

主范式的存在及唯一性?

主析取范式(或主合取范式)存在吗?

〉 如果存在的话，唯一吗?
〉 我们以主析取范式为例，来证明存在性和唯一性

主析取范式存在唯一性证明:约定

〉 首先，合取子句中的文字按照其包含的变元下标从小到大排列
〉 对于包含所有变元p1, p2, ...pn的并排列好文字顺序的合取子句，我们称为极
小项(min term)，记作mi
〉 其中i是一个整数，i对应的n位二进制表示描述了对应下标的变元在合取子句中
的否定状态
〉 如果该位是0，表示合取子句中的该位是一个负文字，否则是正文字
〉 例p1∧p2∧p3记作m7(7=111);p1∧¬p2∧¬p3记作m4(4=100)
〉 主析取范式是极小项按照其下标从小到大排列的析取

主析取范式存在唯一性证明:极小项赋值引理

〉 极小项只有唯一的成真赋值，
〉 且成真赋值中每个变元的取值等于极 小项下标的二进制形式中变元下标所 对应的二进制位的值:
〉 p1∧p2∧p3(m7)的唯一成真赋值 是p1=1, p2=1, p3 =1
〉 p1∧¬p2∧¬p3(m4)的唯一成真 赋值是p1=1, p2=0, p3 =0

主析取范式存在唯一性证明:主析取范式的成真赋值

〉 极小项和主析取范式的关系
〉 主析取范式包含的极小项的成真赋值 也是主析取范式的成真赋值
〉 主析取范式的任一一个成真赋值是其 包含的某个极小项的成真赋值
〉 主析取范式不包含的极小项的成真赋 值是主析取范式的成假赋值

主析取范式存在唯一定理:存在性证明

〉 任何命题公式A(p1, p2, ...pn)的主析取范式都是存在的，并且是唯一的。
〉 假设A'是公式A(p1, p2, ...pn)的析取范式
〉 如果A'中某个合取子句Ai既不包含pj，也不包含¬pj，那么我们将Ai展成如下 形式:
〉 Ai╞╡Ai∧1╞╡Ai∧(pj∨¬pj)╞╡(Ai∧pj) ∨(Ai∧¬pj)
〉 将合取子句中重复出现的命题变元，矛盾式消去，将重复出现的合取子句消去
〉 p∧p╞╡p; p∧¬p╞╡0; Ai∨Ai╞╡ Ai
〉 最后将所有的合取子句整理变元顺序，成为极小项，并得到主析取范式A''

主析取范式存在唯一定理:唯一性证明

〉 反证法:假设公式A(p1, p2, ...pn)存在两个不同的主析取范式B和C
〉 由于A╞╡B且A╞╡C，所以B╞╡C
〉 因为B和C是两个不同的主析取范式，那么一定存在某个极小项mi只出现在B或 者只出现在C中，不妨设mi只出现在B中，不出现在C中，这样:
〉 mi的成真赋值是B的成真赋值，却是C的成假赋值
〉 与B╞╡C矛盾
〉 所以B和C必然相同，也就是说公式A(p1, p2, ...pn)的主析取范式是唯一的
〉 存在性证明还给出了主析取范式的构造步骤。

命题公式A(p1, p2, …pn)的等值分类

〉 具有相同主析取范式的公式都是等值的，属于同一个等值类，否则 属于不同的等值类
〉 虽然公式的数量无限多，但等值类的数量是有限的:
〉 极小项的数量为N=2n;
〉 由极小项组合成的主析取范式的数量为2N;
〉 等值类的数量等于主析取范式的数量

主合取范式:具有和主析取范式对称的性质

〉 极大项和成假赋值
〉 主合取范式的存在性和唯一性
〉 主合取范式的构造步骤
〉 命题公式A(p1, p2, ...pn)的等值分类

八、联结词集完备性

联结词集完备性:真值函数

〉 每一个等值类都对应唯一的真值函数
F(p1, p2, ...pn)
〉 真值函数每个变元的定义域是{0,1}，
值域是{0, 1}
〉 真值函数与相应等值类中的每个命题 公式等值
特别的，与主析取范式(或主合取范式)等值
〉 真值函数与等值类是一一对应的

联结词集完备性:功能完备集

〉 如果任意一个真值函数都可以用仅包含某个联结词集中的联结词的
命题公式表示，则称这个联结词集为功能完备集
〉 要点:命题公式中用到的所有联结词
〉 目前使用的{¬,∧,∨,→,↔}是功能完备集
〉 还有其它的功能完备集吗? 我们注意到任意真值函数都可以用主析取范式来表示，而主析取范式中只有三 种联结词:¬,∧,∨
〉 {¬,∧,∨}是功能完备集

冗余联结词

〉 在一个联结词集中，如果某个联结词 可以用集合中其它联结词来定义，则 这个联结词称作冗余联结词
〉 {¬,∧,∨,→,↔}是否存在冗余联结词?
〉 A→B╞╡¬A∨B，所以→是冗余联结词
〉 {¬,∧,∨,↔}中还有冗余联结词吗?
〉 {¬,∧,∨}中还有冗余联结词吗?

功能完备集证明和极小集

〉 {¬,→}是功能完备集
〉 证明思路:从一个已知的功能完备集 中去掉冗余联结词，直至得到{¬,→}
〉 极小的功能完备集
〉 如果一个功能完备集中不含冗余联结
词，则称这个功能完备集为极小的。
〉 {¬,→}， {¬,∧}， {¬,∨}都是极小功 能完备集

仅包含单个联结词的功能完备集

〉 定义联结词↓(Peirce记号)
〉 p↓q╞╡¬(p∨q)
〉 {↓}是功能完备集
〉 证明思路:用↓去定义已知功能完备集 中的每一个联结词，如{¬,∨}
〉 ¬p╞╡¬(p∨p)╞╡p↓p
〉 p∨q╞╡¬¬(p∨q)
〉 ╞╡¬(p↓q)╞╡(p↓q)↓(p↓q)

非功能完备集证明

〉 如何证明某个联结词集合不是功能完 备集?
〉 并没有统一的证明方法
〉 {∧}不是功能完备集，因为不能构成
矛盾式
〉 不能仅用重言式、逻辑等价式和代入、 替换原理推演证明

非功能完备集证明

〉 {¬,↔}不是功能完备集，
〉 我们注意到，由{¬,↔}组成的命题公 式其成真赋值的个数总是偶数，
〉 不能表示那些成真赋值个数为奇数的 真值函数

九、形式系统和证明、演绎

形式系统

〉 重言式反应了人类逻辑思维的基本规 律
〉 排中律A∨¬A╞╡t
〉 矛盾律A∧¬A╞╡f
〉 假言推理A∧(A→B)╞B
〉 归谬推理(A→B)∧¬B╞¬A
〉 穷举推理(A∨B)∧(A→C)∧(B→C)╞C

形式系统

〉 真值计算、以代入原理、替换原理进 行推演
〉 难以反应人类思维推理过程，
〉 需要建立严密的符号推理体系
〉 形式系统是一个符号体系
〉 系统中的概念由符号表示，推理过程即符号变换的过程
〉 以若干最基本的重言式作为基础，称作公理(axioms)
〉 系统内符号变换的依据是若干确保由重言式导出重言式的规则，称 作推理规则(rules of inference)
〉 公理和推理规则确保系统内由正确的前提总能得到正确的推理结果

证明与演绎:证明Proof

〉 公式序列A1,A2,...,Am称作Am的一个证明，如果Ai(1≤i≤m):
〉 或者是公理;
〉 或者由Aj1,...,Ajk(j1,...,jk<i)用推理规则推得。
〉 当这样的证明存在时，称Am为系统的定理(theorem)，记作 ┠*Am(*是形式系统的名称)，或者简记为┠Am

证明与演绎:演绎Deduction

〉 设Γ为一公式集合。公式序列 A1,A2,...,Am称作Am的以Γ为前提 的演绎，如果Ai(1≤i≤m):
〉 或者是Γ中的公式
〉 或者是公理
〉 或者由Aj1,...,Ajk(j1,...,jk<i)用推理 规则推得。

证明与演绎:演绎Deduction

〉 当有这样的演绎时，Am称作Γ的演
绎结果，
〉 记作Γ┠*Am(*是形式系统的名称)，
或者简记为Γ┠Am
〉 称Γ和Γ的成员为Am的前提
(hypothesis)
〉 证明是演绎在Γ为空集时的特例

十、命题演算形式系统

命题演算形式系统PC(Proposition Calculus)

〉 我们将命题以及重言式变换演算构造为形式系统，称为命题演算形式系统PC
〉 首先，是PC的符号系统
〉 命题变元:p,q,r,s,p1,q1,r1,s1,...
〉 命题常元:t,f
〉 联结词:¬,→(注意是功能完备集)
〉 括号:(,)
〉 命题公式:(高级成分，规定了字符的合法组合方式) 命题变元和命题常元是公式 如果A,B是公式，则(¬A)，(A→B)均为公式(结合优先级和括号省略约定同前) 只有有限次使用上面两条规则得到的符号串才是命题公式

〉 PC的公理(A,B,C表示任意公式)
〉 A1:A→(B→A)
〉 A2:(A→(B→C))→((A→B)→(A→C)) 〉 A3:(¬A→¬B)→(B→A)
〉 PC的推理规则(A,B表示任意公式) 〉 A,A→B/B(分离规则)

PC的性质:合理性Soundness

〉 如果公式A是系统PC的定理，则A 是重言式(如果┠PCA，则╞A)
〉 如果A是公式集合Γ的演绎结果，那 么A是Γ的逻辑结果(如果Γ┠PCA， 则Γ╞A)
〉 说明了PC中的定理和演绎结果都合 乎逻辑

PC的性质:合理性Soundness说明

〉 首先，PC中的公理A1,A2,A3都是重言式;
〉 其次，PC的分离规则是“保真”的，
就是如果A真，A→B真，总有B真。
〉 这样:
〉 由公理和规则导出的定理都是重言式
〉 由Γ、公理和规则导出的公式，在Γ中
的公式都为真时也为真

PC的性质:一致性(consistency)

〉 没有公式A，
〉 使得┠PCA和┠PC¬A同时成立 (不会出现自相矛盾)
〉 由PC的合理性容易证明

PC的性质:完备性(completeness)

〉 如果公式A是重言式，
〉 则A一定是PC中的定理(如果╞A， 则┠PCA)
〉 如果公式A是公式集合Γ的逻辑结果，
〉 则A一定是Γ的演绎结果(如果Γ╞A， 则Γ┠PCA)。证明很难，略。
〉 合乎逻辑的命题，在PC中一定能推 导出来

十一、PC中的证明

证明定理:┠PCA→A

〉 1](A→((A→A)→A))→((A→(A→A))→(A→A)):公理A2 〉 2]A→((A→A)→A):公理A1
〉 3](A→(A→A))→(A→A):对1,2使用分离规则
〉 4]A→(A→A):公理A1
〉 5]A→A:对3,4使用分离规则
〉 上述5个公式构成的序列，即为证明

演绎:{A,B→(A→C)}┠B→C

〉 1]A:前提
〉 2]B→(A→C):前提
〉 3]A→(B→A):公理A1
〉 4]B→A:对1,3用分离规则
〉 5](B→(A→C))→((B→A)→(B→C)):公理A2 〉 6](B→A)→(B→C):对2,5用分离规则
〉 7]B→C:对4,6用分离规则

十二、三个元定理

演绎定理

〉 对任意公式集合Γ和公式A,B
〉 Γ┠A→B当且仅当Γ∪{A}┠B
〉 当Γ=ø时，┠A→B当且仅当{A}┠B，或A┠B
〉 证明必要性:
〉 有A→B，加上A，分离规则得到B
〉 证明充分性:
〉 有B，以及公理A1:B→(A→B)，分离规则 得到A→B

归谬定理

〉 若Γ∪{¬A}┠B，Γ∪{¬A}┠¬B，
〉 那么Γ┠A
〉 意义:
〉 如果同一组前提能推导出相互矛盾的 结果，说明这组前提之间相互不一致，
〉 也就是说总有一些前提是其余前提的 对立面。

穷举定理

〉 对任何公式集合Γ和公式A,B
〉 若Γ∪{¬A}┠B，Γ∪{A}┠B
〉 那么Γ┠B
〉 意义:
〉 如果一个前提能推出结论，这个前提的反面也能推出同样的结论，
〉 说明结论的成立与此前提是否成立无关。

元定理简化证明:┠¬¬A→A

〉 ¬¬A→(¬A→¬¬A):公理A1
〉 由演绎定理就有:{¬¬A,¬A}┠¬¬A
〉 ¬A→(¬¬A→¬A):公理A1
〉 由演绎定理证明了:{¬A,¬¬A}┠¬A， 也就是{¬¬A, ¬A}┠¬A
〉 上面两个前提，用归谬定理得到 {¬¬A}┠A
〉 再用演绎定理，有┠¬¬A→A

元定理简化证明:┠(A→C)→(((B→C)→((¬A→B)→C))

〉 根据演绎定理，只需要证明{A→C,B→C,¬A→B}┠C 〉 因为{A→C,B→C,¬A→B,A}┠C是显然的
〉 {A→C,B→C,¬A→B,¬A}┠C是易证的
〉 根据穷举定理{A→C,B→C,¬A→B}┠C得证

十三、定理判定问题

形式系统构造了一个符号串集合

〉 形式系统定义就是符号串集合的构造性定义
〉 符号体系规定了符号串可能包含的字符(或 字符的合法组合模式，词)
如PC中的命题变元、常元和公式的定义
〉 公理规定了几个集合中的符号串(或者这种
符号串的模式)
如PC中的公理，实质是公理模式
〉 推理规则规定了从集合中已知符号串变换生 成集合中其它符号串的方法
如PC中的分离规则

定理判定问题:符号串的构造过程

〉 形式系统中的定理就是在集合中的符号串
〉 定理的证明过程就是符号串的构造过程
〉 这个过程需要在有限步内结束

定理判定问题:定理判定问题

〉 给定一个命题公式，判定是否形式系统中的定理，给出定理的证明
〉 给定一个符号串，判定是否在集合里，给出构造的过程
〉 能否单靠形式系统本身的公理和推理 规则在有限步骤内判定定理和非定 理?

一个简单的形式系统MIU

〉 符号系统:M,I,U组成的串
〉 初始串:MI

公理:MI

〉 规则1:如果串的最后一个符号是I，则可以加上一个U
如果xI是定理，那么xIU也是定理
〉 规则2:如果串符合Mx，则可以再加上x而生成Mxx，x代表任何 一个由M,I,U组成的串
如果Mx是定理，那么Mxx也是定理
〉 规则3:如果串中出现连续3个I，则可以用U代替III得到新串 如果xIIIy是定理，那么xUy也是定理
〉 规则4:如果串中出现UU，则可以将UU删去得到新串 如果xUUy是定理，那么xy也是定理
〉 判定问题:MU是否系统中的串? MU是否定理?

MIU的定理树

〉 由公理和推理规则，我们容易构造定理树
〉 但无法保证在有限步骤内找到定理所在位置
〉 那么MU到底是不是定理?
〉 需要另寻方法
〉 求助于系统之外的定律

一个MIU的同构系统310

1. M对应3，I对应1，U对应0
2. 自然数31在集合中
3.  规则1:如果集合中有数以1结尾，则添一个0也是集合中的数
4.  规则2:如果集合中有数以3开始，则把3后面的数再重复一次添在 末尾也是集合中的数
5.  规则3:如果集合中有数包含111，则把111替换成0也是集合中的 数
6.  规则4:如果集合中有数包含00，则去掉00的数也是集合中的数
7.  问:30是不是集合中的数?

310系统中的判定:回归MIU系统的结论

1.  通过分析数的构造规则，我们发现集合中的数都不可能被3整除
2.  首先，31不能被3整除
3.  其次，规则1~4都无法从不能被3整 除的数生成能被3整除的数
4.  而30可以被3整除，所以30不属于这 个集合
5.  对照回MIU系统的结论:MU不是MIU系统中的定理

PC系统的定理判定问题?

1.  一个符合PC符号体系定义的命题公式，是否是PC中的定理?
2.  同样，仅用PC系统中公理和分离规则 难以保证能在有限步骤判定一个命题 公式是否定理
3.  幸运的是，命题演算系统PC有一个非 常重要的同构:真值函数运算系统
4.  只需要用真值表判定命题公式对应的 真值函数是否重言式，即可判定是否 PC中的定理，
5.  真值表的运算是有限步骤可以完成的。 (注意:真值表并不是PC中的成分)

Ps:果真好乏味呀。。。MIU这个例子倒是很好玩的呢

参考资料

陈斌 北京大学地球与空间科学学院 gischen@pku.edu.cn