离散数学[4]-数理逻辑-谓词逻辑及形式系统
一、个体、谓词和量词
命题的解析
-
命题逻辑中最小研究单位是原子命题, 并没有进一步的内部结构*
-
定义:命题是对确定的对象作出判断的陈述句
〉 那么,对不确定的对象如何?(x>5) 〉 以及,进行不同条件下的判断如何?
〉 命题逻辑中的推理,关注真值的推演 〉 假言推理、归谬推理和穷举推理 〉 建立在重言式、代入和替换原理基础上 〉 命题逻辑中,命题之间相互独立,没有内在联系 〉 在经典的三段论推理中,命题逻辑有些力不从心
命题之间的内在联系
-
三段论例子:
- 大前提:p:所有的学校都有学生
- 小前提:q:北京大学是学校
- 结论:r:北京大学有学生
-
命题逻辑的形式化结果:
- (p∧q)→r
- 一个正确推理在命题逻辑中并不是永 真式
- 常识:三个命题包含了某些有关联的 概念,并非相互独立
命题的结构分析
- 命题:对确定的对象作出判断的陈述句
- 被作判断的对象:个体
- 作出的判断:谓词
- 个体的数量:量词(所有、有些、没有)
- 谓词逻辑将量词作用于个体,引入个体变元,讨论不确定的对象
- 谓词逻辑也称作一阶逻辑(First Order Logic)
- 如果将量词作用于谓词,引入谓词变 元,属于二阶逻辑研究范围
个体(individual)
- 谓词逻辑中将一切被讨论的对象都称作个体。
- 确定的个体常用a,b,c表示,称作个体常元(constants)
- 不确定的个体常用x,y,z,u,v,w表示,称作个体变元(variables)
- 被讨论对象的全体称作个体域(domainofindividuals),常记做D
- 包含一切对象的个体域特称为全总域(universe),记做U
谓词(predicate)
- 通常是谓语,称作谓词
〉 “北京大学是学校”中的“…是学校” 〉 “张三和李四是朋友”中的“…和… 是朋友” 或者“…和…是…”
- 谓词中可以放置个体的空位个数称为谓词的元数
〉 单元、二元、三元谓词
谓词命名式
- 将谓词中的个体空位用变元字母代替,称作谓词命名式
- 常用大写字母P、Q、R等代表谓词,谓词命名式形如P(x)、Q(x,y)
- 命名式中的变元字母并没有独立的含义,仅是占位符(place holder)
〉 “…是学校”记做SCHL(x) 〉 “…和…是朋友”记做FRD(x,y), 〉 “…和…是…”记做REL(x,y,r)
谓词填式
- 将谓词中的个体空位用个体变元或常元代替,称作谓词填式
- 谓词填式在形式上和命名式相同,但是属于不同的概念,需要根据上下文加以区分
- 类似于编程语言中的函数说明(形参) 和函数调用(实参)之区分
- SCHL(北京大学)表示“北京大学是 学校”
- FRD(张三,李四)表示“张三和李四是 朋友”
- R(x)表示“x是实数”,x为个体变元
- 当谓词填式中的个体都是常元时,它是一个命题,具有确定的真值
量词(quantifiers)
-
指数量词“所有”和“有”
-
“所有”为全称量词(universalquantifier),记做(Any/All)
-
“有”为存在量词(existentialquantifier),记做(Exist)
-
量词作用于谓词时需要引入一个指导变元,同时放在量词后面和谓词填式中:xP(x)、 xP(x)
-
指导变元是不可取值代入的,称作约束变元(bound variables), 约束变元可以改名而不改变语句含义
-
可以取值代入的个体变元称作自由变元(freevariables)
-
量词所作用的谓词或者复合谓词表达式,称作量词的辖域(domain of quantifiers)
-
对于一元谓词,xP(x)和xP(x)都是命题,对于有穷的个体域 〉 xP(x)等价于P(a1)∧…∧P(aN)
-
xP(x)等价于P(a1)∨…∨P(aN)
-
量词用例:
- 个体域是所有人,xFRD(x,张三)表示“张三在这个世界上有朋友”
- 个体域是{1,2},x(x>0)等价于(1>0)∧(2>0)
- 个体域是所有正整数:歌德巴赫猜想
〉 所有大于2的偶数,均可表示为两个素数之和 〉 xpq(Even(x)∧(x>2)→(x=p+q)∧Prime(p)∧Prime(q))
二、谓词公式
谓词公式定义
-
谓词填式是公式,命题常元(零元谓词)是公式,称作原子公式
-
如果A,B是公式,x为任一变元,那么(¬A),(A→B),(xA),(xA) 都是公式(5个联结词还要包括∧,∨,↔)
-
只有有限次使用上述两个条款形成的符号串是公式 〉 联结词结合优先级和括号省略约定同前 〉 注意(xA),(xA)中公式A可以不包含变元x,此时(xA),(xA)均等价于A
谓词公式成为命题
-
如果给定个体域,公式中的所有谓词都有明确意义,公式中的所有自由变元取定个体,谓词公式就成为一个命题
-
设个体域为实数域,E(x,y)表示x=y,L(x,y)表示x<y,那么 〉 xL(0,x2+1)真,xE(x2+x+1,0)假
-
当个体域变成复数域,则上面的真值将改变
-
我们可以使用常用的数学公式代替谓词的形式
1. x(x2+x+1=0)
语句形式化:设个体域为人类
-
有人勇敢,但不是所有人都勇敢
- xBrave(x)∧¬xBrave(x)
-
勇敢者未必是成功者
- ¬x(Brave(x)→Success(x)) 〉 x(Brave(x)∧¬Success(x))
-
君子坦荡荡,小人常戚戚
- x(P(x)→Q(x))∧x(R(x)→S(x))
-
张三孤独走完一生
- x(¬FRD(x,张三)) 或者 ¬xFRD(x,张三)
三、永真式
谓词公式成为命题,具有确定真值的条件
1. 给定个体域
2. 公式中的所有谓词都有明确意义 (解释)
3. 公式中的所有自由变元取定个体
永真式是逻辑中重要的概念
谓词公式有4个层次的“永真”
谓词公式可满足式及永假式
如果对于某个个体域,谓词的某个解释,和自由变元的某个取值,公式A 在此处取值真,则称公式A是可满足式 〉 公式A不可满足时也称A是永假式
谓词公式的逻辑等价与逻辑蕴含
〉 逻辑等价
〉 A╞╡B当且仅当对一切域、解释和变 元取值状况,A和B都具有相同的真 值
〉 逻辑蕴涵
〉 A╞B当且仅当对一切域、解释,一切 使A成真的变元取值状况均使B成真
重要的谓词演算永真式#1
〉所有命题逻辑中的重言式
〉 当A不含变元x时,xA╞╡A,xA╞╡A
〉 xA(x)╞A(x),A(x)╞xA(x), xA(x)╞xA(x)
〉 ¬x¬A(x)╞╡xA(x)
〉 ¬x¬A(x)╞╡xA(x)
〉 ¬xA(x)╞╡x¬A(x)
〉 ¬xA(x)╞╡x¬A(x)
重要的谓词演算永真式#2
〉当公式B中不含自由变元x时,有:
〉 xA(x)∨B╞╡x(A(x)∨B)
〉 xA(x)∧B╞╡x(A(x)∧B)
〉 xA(x)∨B╞╡x(A(x)∨B)
〉 xA(x)∧B╞╡x(A(x)∧B)
重要的谓词演算永真式#3
当公式B中含自由变元x时,有
〉 x(A(x)∧B(x))╞╡xA(x)∧xB(x)
〉 xA(x)∨xB(x)╞x(A(x)∨B(x))
〉 x(A(x)∧B(x))╞xA(x)∧xB(x)
〉 x(A(x)∨B(x))╞╡xA(x)∨xB(x)
重要的谓词演算永真式#4 〉
量词的组合与顺序:
〉 xyA(x,y)╞╡yxA(x,y)
〉 xyA(x,y)╞yxA(x,y)
〉 yxA(x,y)╞xyA(x,y)
〉 xyA(x,y)╞yxA(x,y)
〉 xyA(x,y)╞╡yxA(x,y)
重要的谓词演算永真式#5
〉 当C中无自由变元x时,有:
〉 x(C→A(x))╞╡C→xA(x)
〉 x(C→A(x))╞╡C→xA(x)
〉 x(A(x)→B(x))╞xA(x)→xB(x)
四、谓词演算形式系统FC
一阶谓词演算形式系统(First order predicate Calculus)
-
FC的符号系统:
- 个体变元:x,y,z,u,v,w,…
- 个体常元:a,b,c,d,e,…
- 个体间运算符号(函数符)f(n),g(n),h(n),… 其中n是正整数,表示函数的元数
- 谓词符号:P(n),Q(n),R(n),S(n),… 其中n是非负整数,表示谓词的元数 当n=0时,谓词公式退化为命题常元
- 真值联结词:¬,→ 〉
- 量词:(x等价于¬x¬)
FC的高级语言成分:个体项
-
括号:(, )
-
个体项(term),简称项:
- 个体变元和个体常元是项
- 对任意正整数n,如果f(n)为一n元函数符, t1,…,tn为项,则f(n)(t1,…,tn)也是项
- 除有限次数使用上述两个条款确定的符号串外, 没有别的东西是项
FC的高级语言成分:合式公式
合式公式(well-formed formula),简称公式
- 对任意非负整数n,如果P(n)是一n元谓词 符,t1,…,tn为项,那么P(0)(命题常元) 和P(n)(t1,…,tn)(n>0)是公式;
- 如果A,B是公式,v为任一个体变元,那么 (¬A), (A→B), (vA)(或(vA(v)))均为公式
- 除有限次数使用上述两个条款确定的符号串外,没有别的东西是公式
全称封闭式(generalization closure)
〉 设v1,...,vn是公式A中的自由变元, 那么公式v1...vnA(或 v1...vnA(v1,...,vn))称为公式A 的全称封闭式。
〉 A中不含自由变元时,A的全称封闭 式为其自身
FC的公理
〉 A1:A→(B→A)
〉 A2:(A→(B→C))→((A→B)→(A→C))
〉 A3:(¬A→¬B)→(B→A)
〉 A4:xA(x)→A(t/x)(x为任一自由变元,t为对x可代入的项)
〉 A5:x(A(x)→B(x))→(xA(x)→xB(x))(x为任一自由变元)
〉 A6:A→xA(A中无自由变元x)
〉 A7:(A1到A6的全称封闭式都是FC的公理)
〉 我们看到A1~A3是命题逻辑的重言式,也是谓词演算的永真式,A4~A7是谓 词演算的永真式
FC的推理规则和重要性质
〉 FC的推理规则(A,B表示任意公式)
〉 A,A→B/B(分离规则)
〉 FC的重要性质
- 合理性、一致性、完备性
- 演绎定理
- 归谬定理
- 穷举定理
五、全称引入规则及存在消除规则
全称引入规则(universal generalization)
- 对于任意公式A,变元v,如果┠A,那么┠vA
证明:
〉 对A的证明序列长度l进行归纳
l=1时,A为公理,那么:
〉 如果A中有自由变元v,vA就是A的全称封闭式,根据A7,vA还是公理;
〉 如果A中没有自由变元,由A和公理A6:A→vA用分离规则,得到 ┠vA
假设l<k时全称引入规则成立,而A的证明序列是A1,A2,...,Ak(=A)
1 如果Ak是公理,则证明同上;
2 如果Ak不是公理,则一定由Ai和Aj(=Ai→Ak)(i,j<k)用分离规 则得出
〉 由归纳假设我们有┠vAi和┠v(Ai→Ak)
〉 同时我们有公理v(Ai→Ak)→(vAi→vAk)
〉 对上式公理和归纳假设结果用两次分离规则,得到┠vAk也就是 ┠vA
〉 归纳完成,全称引入规则得证。
全称引入规则推广到演绎结果
-
对任何公式集Γ,公式A以及不在Γ中,任何公式自由出现的变元v,如果Γ┠A,那么Γ┠vA
-
关于全称引入规则的直觉表述:
〉 如果我们能够用一组与变元v无关的 前提演绎出A(v) 〉 表明我们已经对任意的v导出了A(v), 也就是vA(v) 〉 反过来,如果前提中有公式B(v)包含 了自由变元v 〉 那么导出的A(v)是以B(v)为前提的,即v不是任意的,所以不会有vA(v)成立
存在消除规则(existential instantiation)
-
设A,B为任意公式,变元x是公式A,但不是公式B的自由变元
〉 那么当┠xA(x),A(x)┠B同时成立时,有┠B 〉 同样具有演绎的推广形式 〉 意义:如果A(x)能推出B成立,而B中并不包含变元x,说明B的成立与x的具体取值无关, 只需要有x能使A(x)为真,B即为真。 〉 数学证明中经常使用的“不妨设……”句式, 即为存在消除规则
六、自然推理系统
PC和FC的不足之处
- FC和PC一样,证明和演绎过程都过 于繁复
- 为了追求简洁,只用2个联结词、1个 量词和1条推理规则
- 如果能够引入更多的联结词、量词、 推理规则,那么证明和演绎过程会显得更自然
人们经常在推理过程中使用假设
- (演绎)为了证明A→B,常假设A成立,如果能够证明B成立,则 完成了A→B的证明;
- (归谬/反证)为了证明A,常假设¬A,如果导出矛盾(假命题f), 则A成立;
- (穷举)已知A∨B,要证明C,常假设A和B成立分别证明C,如果都能成功,则完成C的证明
- (不妨设)已知vA(v),要证明与v无关的C,常假设A(v0),如果能够证明C,则完成C的证明
- 在形式系统中引入带假设的推理规则,能够使推理过程更加接近人的思维,更加高效和便捷
自然推理系统ND(Natural Deduction)
- 采用5个联结词,2个量词
- 少数公理,更多的规则,引入假设
- 用推理规则体现人的推理习惯
- ND的符号系统:
1. 引入5个联结词、2个量词
-
ND的公理:
Γ;A┠A(Γ是公式集合)
自然推理系统ND的推理规则
- 假设引入规则
〉 Γ┠B
〉 Γ;A┠B(源于重言式B→(A→B))
- 假设消除规则
〉 Γ;A┠B,Γ;¬A┠B
〉 Γ┠B(源于重言式¬A→(A→B)) 〉 推理中的分情况证明
-
∨引入规则
- 〉 Γ┠A
- Γ┠A∨B(源于重言式A→(A∨B))
-
∨引入规则(加强形式)
1. Γ; ¬B┠A
2. Γ┠A∨B(源于重言式(¬B→A)↔(B∨A))
- ∨消除规则
1. Γ; A┠C,Γ; B┠C,Γ┠A∨B
2. Γ┠C(源于重言式(A∨B)∧(A→C)∧(B→C)→C)
- ∧引入规则
1. Γ┠A,Γ┠B
2. Γ┠A∧B
- ∧消除规则
1. Γ┠A∧B, Γ┠A
- →引入规则
1. Γ;A┠B
2. Γ┠A→B(即演绎定理) 〉
- →消除规则
1. Γ┠A→B,Γ┠A
2. Γ┠B(即分离规则)
- ¬引入规则
1. Γ; A┠B,Γ; A┠ ¬B
2. Γ┠¬A
- ¬引入规则(2)
1. Γ;A┠f
2. Γ┠ ¬A(反证法)
- ¬消除规则
1. Γ┠A, Γ┠ ¬A
2. Γ┠B(虚假的前提可以蕴涵任何结论)
- ¬¬引入规则
1. Γ┠A
2. Γ┠¬¬A
- ¬¬消除规则
1. Γ┠¬¬A
2. Γ┠A
- ↔引入规则
1. Γ┠A→B,Γ┠B→A 〉 Γ┠A↔B
- ↔消除规则
1. Γ┠A↔B
2. Γ┠A→B
- 引入规则
1. Γ┠A
2. Γ┠ vA(v在A中无自由出现,FC公理)
- 引入规则(2)
1. Γ┠ A(v)
2. Γ┠ vA(v)(v在Γ中无自由出现,全称引入规则)
- 消除规则
1. Γ┠ vA(v)
2. Γ┠ A(t/v)(t对v可代入) 源于FC的公理A4:xA(x)→A(t/x)
- 引入规则
1. Γ┠A(t)
2. Γ┠vA(v/t)(源于永真式 A(t)→vA(v/t))
- 消除规则
1. Γ┠vA(v),Γ;A(e/v)┠C
2. Γ┠C
七、ND中的定理证明
ND中的证明和演绎
〉 在ND中,称A为Γ的演绎结果,即Γ┠NDA简记为Γ┠A,如果存在如 下序列:
〉 (Γ=Γ1)Γ1┠A1,Γ2┠A2,...,Γn┠An(Γn=Γ,An=A)
〉 使得Γi┠Ai(1≤i≤n): 1 或者是公理;
2 或者是Γj┠Aj (j<i)
3 或者是对Γj1┠Aj1,..., Γjk┠Ajk(j1,...,jk<i)使用推理规则导出 的
〉 如果有Γ┠A,且Γ=ø,则称A为ND的定理
ND证明定理:┠A∨¬A
(1)A┠A;公理
〉 (2)A┠A∨¬A;∨引入规则(1)
〉 (3)¬A┠¬A;公理
〉 (4)¬A┠A∨¬A;∨引入规则(3)
〉 (5)┠A∨¬A;假设消除规则(2)(4)
定理证明:x(A(x)→B(x))→(xA(x)→xB(x))
1 x(A(x)→B(x)), xA(x)┠xA(x);公理
2 x(A(x)→B(x)), xA(x)┠A(t);消除规则(1)
3 x(A(x)→B(x)), xA(x)┠x(A(x)→B(x));公理
4 x(A(x)→B(x)), xA(x)┠A(t)→B(t); 消除规则(3) 5 x(A(x)→B(x)), xA(x)┠B(t);→消除规则(2)(4)
6 x(A(x)→B(x)), xA(x)┠xB(x); 引入规则(5)
7 x(A(x)→B(x))┠xA(x)→xB(x);→引入规则(6)
8 ┠x(A(x)→B(x))→(xA(x)→xB(x)) ;→引入规则
ND的一些重要性质
〉 FC的公理和定理都是ND的定理
〉 ND是合理的、一致的、完备的
参考资料:
陈斌 北京大学地球与空间科学学院 gischen@pku.edu.cn
个人公众号,比较懒,很少更新,可以在上面提问题,如果回复不及时,可发邮件给我: tiehan@sina.cn