Ch4-谓词逻辑的基本概念
Q: 能否用命题逻辑刻画以下推理:
凡有理数都是实数 ;
2/7 是有理数 ;
所以 2/7 是实数 。
不能说是 . 需要再引用符号,来表示一个个体是否具有某个性质。
谓词和个体词
Definition(谓词):谓词是给定个体到 上的映射。常常使用大写字母 表示。
在一个命题里,如果主词只有一个,则此时表示该主词性质或属性的词便称为谓词,以 表示。
如果多于一个,表示主词之间的关系,以 表示。
Example:
例如 “3 是有理数”,其中“是有理数”是谓词,表示了 3 的关系;
“5 大于 3”,其中“大于”是谓词,表示了 5,3 之间的关系。
Definition(个体词):是一个命题里面表示思维对象的词。若指定了,称为个体常量;若没有指定,则称为个体变项。
Definition(谓词变项) 有 个个体的谓词 称为 项谓词。如果 有明确含义,则称为谓词常项,而 表示任一谓词时,称为谓词变项。
Definition(个体域/论域) 将个体变项的变化范围称为 个体域 或者 论域。e.g. 自然数集,实数集。命题正确与否,也取决于论域。
谓词 是不是命题?不是,因为没有给出 的具体定义,如 表示 是有理数, 代表 3,则 取值为 T. 谓词逻辑是命题逻辑的推广。可以认为一个命题是一个零元谓词。
函数和量词
Definition(函数):是某个体域到另外一个体域的映射,约定用小写字母表示。
Example:书上的举例:,表示张三的父亲和母亲是否结婚。
Definition(量词): 作用于个体变元,不允许作用于命题变项和谓词变项。表示为:
为真,当且仅当任意 ,都有 .
为假,当且仅当存在 ,有 .
不允许出现 .
变量易名规则:,间接说明了和具体的 无关。
Definition(辖域):是量词所约束的范围。
中, 是 的辖域。
谓词逻辑合式公式
符号约定:
表示命题变项;
表示个体;
表示谓词变项;
表示函数。
Definition(谓词逻辑的合式公式):合式公式的定义:
反面:. .
反面:. .
简单理解,就是能不能给出一个解释,使得合式公式合理。
自然语句的形式化
所有的……都是……
不等价于 ,因为这句话说的是 .
当真值取真时,真值和论域无关?
“所有的实数都是有理数”,若论域取 ,则成立;若取 ,则不成立;若取 ,则成立。
有的……是……
设 ,,不等价于 . 假设我们找到一个数既不是有理数,也不是无理数,那么这个是对的。
没有……是……
有的……不是……
至少有一偶数是素数和至少有一偶数并且至少有一素数 第一个命题等价于“有的……是……”,第二个命题等价于:
积木世界的形式描述
谓词 ,表示是否在上; 表示是否其上有积木块,则:
自然数集的形式化描述
论域是自然数集,来形式化语句:
(1)对每个数,有且仅有一个相继后元
(2)没有这样的数,0 是其相继后元
(3)对除 0 而外的数,有且仅有一个相继前元(可将这三句话作为建立自然数集合的公理)
引入:
谓词 代表 ;
表示个体 的相继后元;
表示个体 的相继前元。
那么可以这样表示:
在说:存在一个 是 的相继后元,如果另外一个数 也是相继后元,那么 .
在说:没有一个数的后继是 .
谓词变元多次量化和公式表示法
可得:
假设论域为 ,我们可以枚举:
因此, 是 的推广, 是 的推广。
在论域 上多次量化公式:
公式的普遍有效性和判定问题
和命题公式类似,也有三类:
如何理解一个解释,就是将个体变元以具体的事物代之。
对一个谓词公式来说,如果在它的任一解释 下真值都为真,便称作 普遍有效的。
对一个谓词公式来说,如果在它的某个解释 下真值为真,便称作 可满足的。
对一个谓词公式来说,如果在它的任一解释 下真值均为假,便称作 不可满足的。
有限域 上一个公式的可满足性和普遍有效性依赖于个体域个体的个数且仅依赖于个体域个体的数目
在某个含 个元素的 个体域上普遍有效 (或可满足),则在任一 个体域上也普遍有效 (或可满足);
如果某公式在 个体域上普遍有效,则在 个体域上也普遍有效;
如果某公式在 个体域上可满足,则在 个体域上也可满足。
谓词逻辑的判定问题,指的是任一公式的普遍有效性。若说谓词逻辑是可判定的,就要给出一个能行方法,使得对任一谓词公式都能判断其是否普遍有效。
Ch5-谓词逻辑的等值和推理演算
谓词逻辑的等值
等值式的定义:如果公式 的任何解释下, 都有相同的真值,则 等值。
Theorems 由命题公式移植来的等值式 (命题公式中,直接以谓词公式代入命题变项)
Theorems 否定型等值式(摩根律)
如果不是对所有 都成立,一定对一个 不成立。
Examples
“并非所有的动物都是猫” 设 : 是动物,: 是猫。
“天下乌鸦一般黑” 设 : 是乌鸦,: 一般黑。
.
.
等值的公式:不存在两个东西是乌鸦且不一般黑:.
证明:
Theorems 量词对合取、析取的分配律 若 不含 ,则:
对 , 对 的分配率一般不成立。
Problem:证明 .
Proof:例如,对于论域 ,令 ,则不成立。
Problem:但是 .
Proof:枚举 成立或者 成立。
Problem:证明 . 和上面举例相同。
Problem:证明 ,
Proof:消去存在量词, 为真,则 均为真,此时 和 均成立。
Theorems 量词对 的分配律
Proof(1.)
也可以这样证明,引入前提假设 ,则 成立当且仅当 。
Theorems 变元易名后的分配律
Proof(1.) RHS先做替换:. 然后后面一项对于第一项来说,可以视作常量 ,则:
因此:
谓词逻辑的范式
Definition 前束范式 如果 中的一切量词都位于公式的最左边(不含否定词),而且量词的辖域都延伸到公式的末端,前束范式 的一般形式为:
其中 为量词, 称为公式 的母式(基式), 中不再有量词。
谓词逻辑的任一公式都可以化为与之 等值 的前束范式,但是不唯一。
Definition 前束范式一个公式的 前束范式为 . 所有的存在量词都在全称量词的左边。 不含量词和自由个体变元。
谓词逻辑的任一公式 ,都可以化作相应的 前束范式,并且 是 普遍有效 的当且仅当其 范式是 普遍有效 的。
Problem:求 的 前束范式(P 中无量词)。
Solution:将全称量词 改写为存在量词 ,再引入谓词 和一个变元 ,得到 ,建立公式
前束范式仅在普遍有效的意义下与原公式等值,
Problem 求公式 的前束范式。
Solution:
Definition Skolem 标准型 仅仅保留全称量词的前束形。
谓词逻辑的任一公式 ,都可以化作相应的 Skolem 标准型,并且 是 不可满足 的当且仅当其 Skolem 标准型是 不可满足 的。
从左到右消去存在量词,设要消去 (),则将谓词 中出现的所有变元 均以论域中的某个常项 代入。若 () 的左边有若干全称量词 ,需将谓词 中出现的所有变元 均以全称量词 的某个多元函数 代入。
Example 求公式 的 Skolem 标准型.
替代为未出现的常项 .
替代为 的函数 .
替代为 的函数 .
因此 Skolem 标准型为 .
可以这样理解,比如说极限的定义是 .
可以给出 关于 的一个函数。
谓词逻辑的基本的推理公式
Proof:前面推导过。
Proof:引入前提假设 或 . 在 的条件下,可以分别推得 或 成立。
Proof:和上面证明方法一样,证明双向。
Proof:
Proof:解释性的说明:
当 对于任意论域中的 都成立,则存在 ,使得任意 成立。
设在一解释 下,有 ,于是有 ,使得对于一切的 ,都有 . 从而对于一切的 ,都有一个 (均选为 )使得 .
谓词逻辑的推理演算
前提引入规则;
结论引用规则;(中间结论可以作为后续推理的前提)
代入规则;(代入重言式的命题变项)
置换规则;(用等值公式置换)
分离规则(假言推理) 和 推出 .
条件证明规则。引入前提条件。 和 是等价的。
谓词逻辑的推理规则
全称量词消去规则。. 其中 是论域中的一个个体。注意如果 中存在量词和变项时,需要限制 不在 中不能出现,不能使用重复的符号。
全称量词引入规则。. 其中 是论域中任意个体。
存在量词消去规则。. 其中 是论域中一个个体常项。需要限制 中没有自由个体出现。
存在量词引入规则。. 其中 是论域中的一个个体常项。 不能出现在 里。
例如 .
但是不能再推出 ,因为不是对于同一个 都成立。
需要分析好变量之间的依赖关系。
Example:分析下述推理的正确性
. 前提;
. 全称量词消去, 与 相关;
. 存在量词消去, 依赖 .
. 全称量词引入(错误, 不能依赖 )
Problem:有的病人喜欢所有的医生:
没有病人喜欢庸医:
推出,没有医生是庸医:
Solution.
存在量词消去 .
全称量词消去
2. 推出
2. 推出
6. 消去
. 5. 4. 分离
. 8. 消去
. 9. 置换。
. 三段论
. 全称量词引入(因为 为论域中任何一个个体)
谓词逻辑的归结证明
根据 ,写出公式 .
建立子句集。
归结出矛盾。
证明 .
首先写出:
的子句集为 .
的子句集为 .
.
Skolem 化,得子句集 .
因此 的子句集为 .
得到 .
得到 .
矛盾。
.
.
.
求证 . .
建立子句集: