离散数学[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的偶数,均可表示为两个素数之和 〉 xpq(Even(x)∧(x>2)→(x=p+q)∧Prime(p)∧Prime(q))

二、谓词公式

谓词公式定义

  1. 谓词填式是公式,命题常元(零元谓词)是公式,称作原子公式

  2. 如果A,B是公式,x为任一变元,那么(¬A),(A→B),(xA),(xA) 都是公式(5个联结词还要包括∧,∨,↔)

  3.  只有有限次使用上述两个条款形成的符号串是公式 〉 联结词结合优先级和括号省略约定同前 〉 注意(xA),(xA)中公式A可以不包含变元x,此时(xA),(xA)均等价于A

谓词公式成为命题

  1. 如果给定个体域,公式中的所有谓词都有明确意义,公式中的所有自由变元取定个体,谓词公式就成为一个命题

  2. 设个体域为实数域,E(x,y)表示x=y,L(x,y)表示x<y,那么 〉 xL(0,x2+1)真,xE(x2+x+1,0)假

  3. 当个体域变成复数域,则上面的真值将改变

  4. 我们可以使用常用的数学公式代替谓词的形式

    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 〉

量词的组合与顺序:

〉 xyA(x,y)╞╡yxA(x,y) 
〉 xyA(x,y)╞yxA(x,y) 
〉 yxA(x,y)╞xyA(x,y) 
〉 xyA(x,y)╞yxA(x,y) 
〉 xyA(x,y)╞╡yxA(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),简称公式

  1.  对任意非负整数n,如果P(n)是一n元谓词 符,t1,…,tn为项,那么P(0)(命题常元) 和P(n)(t1,…,tn)(n>0)是公式;
  2. 如果A,B是公式,v为任一个体变元,那么 (¬A), (A→B), (vA)(或(vA(v)))均为公式
  3.  除有限次数使用上述两个条款确定的符号串外,没有别的东西是公式

全称封闭式(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的重要性质
  1. 合理性、一致性、完备性
  2. 演绎定理
  3. 归谬定理
  4. 穷举定理

五、全称引入规则及存在消除规则

全称引入规则(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的不足之处

  1. FC和PC一样,证明和演绎过程都过 于繁复
  2. 为了追求简洁,只用2个联结词、1个 量词和1条推理规则
  3. 如果能够引入更多的联结词、量词、 推理规则,那么证明和演绎过程会显得更自然

人们经常在推理过程中使用假设

  •  (演绎)为了证明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)

  1. 采用5个联结词,2个量词
  2. 少数公理,更多的规则,引入假设
  3.  用推理规则体现人的推理习惯
  4. ND的符号系统:

    1. 引入5个联结词、2个量词

  5. ND的公理:

    Γ;A┠A(Γ是公式集合)
    

自然推理系统ND的推理规则

  1. 假设引入规则

    〉 Γ┠B 〉 Γ;A┠B(源于重言式B→(A→B))

  2.  假设消除规则

    〉 Γ;A┠B,Γ;¬A┠B 〉 Γ┠B(源于重言式¬A→(A→B)) 〉 推理中的分情况证明

  3. ∨引入规则

    1. 〉 Γ┠A
    2.  Γ┠A∨B(源于重言式A→(A∨B))
  4. ∨引入规则(加强形式)

    1.  Γ; ¬B┠A  
    2.  Γ┠A∨B(源于重言式(¬B→A)↔(B∨A))
  5. ∨消除规则

    1.  Γ; A┠C,Γ; B┠C,Γ┠A∨B   
    2.  Γ┠C(源于重言式(A∨B)∧(A→C)∧(B→C)→C)
  6. ∧引入规则

    1. Γ┠A,Γ┠B
    2.  Γ┠A∧B
  7. ∧消除规则

    1.  Γ┠A∧B,   Γ┠A
  8. →引入规则

    1. Γ;A┠B
    2.  Γ┠A→B(即演绎定理) 〉
  9. →消除规则

    1.  Γ┠A→B,Γ┠A
    2. Γ┠B(即分离规则)
  10.  ¬引入规则

    1.  Γ; A┠B,Γ; A┠ ¬B
    2. Γ┠¬A
  11. ¬引入规则(2)

    1. Γ;A┠f
    2. Γ┠ ¬A(反证法)
  12.  ¬消除规则

    1. Γ┠A, Γ┠ ¬A
    2. Γ┠B(虚假的前提可以蕴涵任何结论)
  13.  ¬¬引入规则

    1.  Γ┠A
    2. Γ┠¬¬A
  14.  ¬¬消除规则

    1.  Γ┠¬¬A
    2. Γ┠A

    3.  ↔引入规则

    4.  Γ┠A→B,Γ┠B→A 〉 Γ┠A↔B

  15. ↔消除规则

    1.  Γ┠A↔B
    2. Γ┠A→B
  16.  引入规则

    1.  Γ┠A
    2. Γ┠ vA(v在A中无自由出现,FC公理)
  17.  引入规则(2)

    1. Γ┠ A(v)
    2. Γ┠ vA(v)(v在Γ中无自由出现,全称引入规则)
  18.  消除规则

    1.  Γ┠ vA(v)
    2. Γ┠ A(t/v)(t对v可代入)   源于FC的公理A4:xA(x)→A(t/x)
  19. 引入规则

    1.  Γ┠A(t)
    2. Γ┠vA(v/t)(源于永真式 A(t)→vA(v/t))
  20. 消除规则

    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

个人公众号,比较懒,很少更新,可以在上面提问题:

更多精彩,请移步公众号阅读:

Sam avatar
About Sam
专注生物信息 专注转化医学