命题逻辑及形式系统【下】

在上一篇文章中我们已经讨论了由原子命题和逻辑联结词构成的命题公式。下面我们来探讨一下命题公式的分类，以及其中较为重要的重言式。

一、重言式

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

重言式，（永真式）tautology：命题变元的所有赋值都是命题公式的成真赋值
矛盾式（永假式、不可满足式）contradiction：命题变元的所有赋值都是命题公式的成假赋值
可满足式(contingency)：命题公式至少有一个成真赋值
其中，需要分清的概念是：永真式都是可满足式。矛盾式都不是可满足式。非永真式并不都是永假式。如果A是永真式，则¬A就是永假式，反之亦然。

例如：A∨¬A是重言式（排中律） A∧¬A是矛盾式（矛盾律）

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

逻辑等价式(logical equivalent)

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

一些重要的逻辑等价式（A,B,C是任意公式）
〉 E1：¬¬A╞╡A（双重否定律）
〉 E2：A∨A╞╡A，A∧A╞╡A（幂等律）
〉 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：¬(A∨B)╞╡¬A∧¬B， ¬(A∧B)╞╡¬A∨¬B（德摩根律）
〉 E7：A∨(A∧B)╞╡A， A∧(A∨B)╞╡A（吸收律）
〉 E8：A→B╞╡¬A∨B（蕴涵等值式）
〉E9：A↔B╞╡(A→B)∧(B→A)（等价等值式）
〉 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：A∧B→C╞╡A→(B→C)
〉 E15：A→B╞╡¬B→¬A（假言易位）
〉 E16：(A→B)∧(A→¬B)╞╡¬A（归谬论）
〉 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都是重言式
〉逻辑蕴涵体现了两个公式A B之间的另一种关系：在任何赋值状况下只要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) RS
〉将重言式A中的某个命题变元p的所有出现都代换为命题公式 B，得到的命题公式记作A(B/p)，A(B/p) 也是重言式。
〉因为重言式A的真值与p的取值状况无关，恒为 t，所以将p全部代换后的公式A(B/p)的真值也恒为t

注意：仅代换部分出现本原理不成立，

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

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

常用来证明逻辑等价式的方法有如下几种方法：

〉 真值表法：要证明 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∨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
〉 析取子句(disjunctive clauses)：文字或者若干文字的析取，如：p, p∨q, ¬p∨q
〉 合取子句(conjunctive clauses)：文字或者若干文字的合取，如：p, p∧q, ¬p∧q
〉 互补文字对(complemental pairs of literals)：指一对正文字和负文字，如：p和¬p

析取范式 (disjunctive normal form)

〉公式A’称作公式A的析取范式，如果： A’╞╡A ， A’ 为合取子句或者若干合取子句的析取
〉 p→q的析取范式为 ¬p∨q（合取子句¬p和q的析取）
〉 ((p→q)∧¬p)∨¬q的析取范式为 ¬p∨(q∧¬ p)∨¬q

合取范式(conjunctive normal form)

〉公式A’称作公式A的合取范式，如果： A’╞╡A
〉 A’为析取子句或者若干析取子句的合取
〉 p→q的合取范式为 ¬p∨q（析取子句¬p∨q）
〉 ((p→q)∧¬p)∨¬q的合取范式为 (¬p∨t)∧(¬p∨¬q) 或 ¬p∨¬q

一般使用逻辑等价式和代入原理、替换原理，可以求出任一一个公式的析取范式和合取范式。同时范式用于重言式和矛盾式的识别。例如：

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

一个公式的析取范式或合取范式都不是唯一的，公式的析取范式有可能同时又是合取范式。例如¬p∨q既是p→q的析取范式又是合取范式，那么能否找到“最为规范”的范式？同时具备唯一性的范式呢？那就应该是主范式。

主范式

主析取范式 (major disjunctive form)：公式 A' 称作公式A(p1, p2, …pn)的主析取范式，

如果： A' 是A的析取范式，A'中每一个合取子句里p1, p2, …pn均恰出现一次

主合取范式(major conjunctive form)：公式A'称作公式A(p1, p2, …pn)的主合取范式，

如果：A'是A的合取范式，A'中每一个析取子句里p1, p2, …pn均恰出现一次

此外，我们可以通过证明主范式（析取或者合取范式）的存在性和唯一性。即他们是存在且唯一的。

逻辑联结词的完备性

在之前我们已经提到过了关于逻辑词的完备性问题。

如果任意一个真值函数都可以用仅包含某个联结词集中的联结词的命题公式表示，则称这个联结词集为功能完备集

如果在去掉逻辑词完备集中的冗余的联结词就是极小的功能完备性。比如：{¬,→}， {¬,∧}， {¬,∨}都是极小功
能完备集

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

重言式反应了人类逻辑思维的基本规律，如下所示：
〉排中律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)用推理规则推得

当有这样的演绎时， 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（分离规则）

以上就是命题演算形式系统的定义，它满足合理性、一致性、完备性。

合理性Soundness说明：

首先，PC中的公理A1,A2,A3都是重言式；其次，PC的分离规则是“保真”的，就是如果A真，A→B真，总有B真。

这样：由公理和规则导出的定理都是重言式，由Γ、公理和规则导出的公式，在Γ中的公式都为真时也为真。

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

完备性(completeness)

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

三个元定理

演绎定理
〉对任意公式集合Γ和公式A,B， Γ┠A→B当且仅当Γ∪{A}┠B。当Γ=ø时，┠A→B当且仅当{A}┠B，或A┠B

归谬定理
〉对任何公式集合Γ和公式A,B，若 Γ∪{¬A}┠B，Γ∪{¬A}┠¬B，那么Γ┠A 。

意义：如果同一组前提能推导出相互矛盾的结果，说明这组前提之间相互不一致，也就是说总有一些前提是其余前提的对立面

穷举定理
〉对任何公式集合Γ和公式A,B，若Γ∪{¬A}┠B，Γ∪{A}┠B。那么Γ┠B

意义：如果一个前提能推出结论，这个前提的反面也能推出同样的结论，说明结论的成立与此前提是否成立无关。

八、形式系统的判定性问题

形式系统定义就是符号串集合的构造性定义
〉 符号体系规定了符号串可能包含的字符（或字符的合法组合模式，词）
如PC中的命题变元、常元和公式的定义

〉公理规定了几个集合中的符号串（或者这种符号串的模式）。如PC中的公理，实质是公理模式

〉推理规则规定了从集合中已知符号串变换生成集合中其它符号串的方法。如PC中的分离规则

符号串的构造过程

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

定理判定问题

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

一个简单的形式系统，比如侯世达-集异壁书中的 MIU 形式系统。其实仅靠自身的公理和推理规则是很难判定一个公式是否在该形式系统中的，一般可以找到与该形式系统同构的系统，而在新的同构的系统中比较容易判断。从而借助外面的系统进行判断。在 MIU系统它同构了一个自然数系统，如 310 ，在由素数的性质进行了判断。那我们不禁会想了命题演算形式系统（PC符号体系）呢？一个符合PC符号体系定义的命题公式，是否是PC中的定理吗？容易判定吗？

其实同样，仅用PC系统中公理和分离规则难以保证能在有限步骤判定一个命题公式是否定理。

但是幸运的是，命题演算系统PC有一个非常重要的同构：真值函数运算系统

〉只需要用真值表判定命题公式对应的真值函数是否重言式，即可判定是否PC中的定理，
〉真值表的运算是有限步骤可以完成的，所以我们就可以对PC中的定理进行判定了。

（注意：真值表并不是PC中的成分，也可以认为是寻找的外在同构的真值函数运算系统）

【数理逻辑三】命题逻辑及形式系统【下】相关推荐

【数理逻辑】命题逻辑 ( 命题逻辑推理正确性判定 | 形式结构是永真式 - 等值演算 | 从前提推演结论 - 逻辑推理 )
文章目录一. 命题逻辑推理正确性判定二. 形式结构是永真式 ( 等值演算 ) 三. 从前提推演结论 ( 逻辑推理 ) 一. 命题逻辑推理正确性判定命题推理 , 根据前提 , 推理出结论 ; ...
【数理逻辑】命题逻辑 ( 等值演算 | 幂等律 | 交换律 | 结合律 | 分配律 | 德摩根律 | 吸收率 | 零律 | 同一律 | 排中律 | 矛盾律 | 双重否定率 | 蕴涵等值式 ... )
文章目录一.等值演算二.等值式三.基本等值式四.基本运算五.等值演算基于上一篇博客 [数理逻辑]命题逻辑 ( 命题与联结词回顾 | 命题公式 | 联结词优先级 | 真值表可满足式矛盾式 ...
运维经验分享（三）-- 解决Ubuntu下crontab不能正确执行脚本的问题
原创作品,允许转载,转载时请务必以超链接形式标明文章原始出处 .作者信息和本声明.否则将追究法律责任.http://dgd2010.blog.51cto.com/1539422/1676490 运维 ...
第五节系统调用的三个层次（下） ——20135203齐岳
第五节系统调用的三个层次(下) By 20135203齐岳本周的课程主要内容有三点: 在MenuOS中通过添加代码增加自定义的系统调用命令使用gdb跟踪调试内核简单分析system_call代 ...
KETTLE调度第三篇：Windows下调度Dos脚本编写和遇到的一些问题解决
KETTLE调度第三篇:Windows下调度Dos脚本编写和遇到的一些问题解决参考文章: (1)KETTLE调度第三篇:Windows下调度Dos脚本编写和遇到的一些问题解决 (2)https:// ...
（Linux无线网卡WIFI上网三）嵌入式Linux下的WIFI使用
导航 (Linux无线网卡WIFI上网一 )USB-WIFI驱动移植 (Linux无线网卡WIFI上网二 )WPA_SUPPLICANT--Linux下的wifi管理工具移植 (Linux无线网卡 ...
【梅哥的Ring0湿润插入教程】重磅第三课：Ring0下的PE Loader及重加载内核秒杀一切内核级钩子（上篇）...
[梅哥的Ring0湿润插入教程] Email:mlkui@163.com 转载请注明出处,谢绝喷子记者等,如引起各类不适请自觉滚J8蛋! 第三课:Ring0下PE Loader及重加载内核绕过一切内核 ...
[新浪]新东方三大网红跌下神坛这一年
新东方三大网红跌下神坛这一年 2018-11-23 08:28:29 创事记微博作者: 锌刻度我有话说(863人参与) 欢迎关注"创事记"的微信订阅号:sinac ...
系统工程（SE）学习笔记（三）——需求工程（下）
系统工程(SE)学习笔记(三)--需求工程(下) 零．回顾壹. 三问需求分析贰．什么是好的系统需求叁．总结在需求工程(上)中,我们聊过了STH(stakeholder)和STH Req( ...
【新知实验室三步完成Windows下实时音视频开发】
三步完成Windows下实时音视频开发第一步:开通产品第二步:下载源码第三步:编译源码第四部:运行测试背景介绍实时音视频(Tencent RTC)基于腾讯21年来在网络与音视频技术上的深度 ...

【数理逻辑三】命题逻辑及形式系统【下】