命题逻辑公理系统

1、计算机学院1计算机学院1主要内容主要内容 概述概述 命题逻辑公理系统命题逻辑公理系统 谓词逻辑公理系统谓词逻辑公理系统 公理系统性质公理系统性质 理论与模型理论与模型 判定问题判定问题 总结总结计算机学院2计算机学院2逻辑公理系统逻辑公理系统 公理系统公理系统 从一些从一些公理公理出发，根据出发，根据演绎法演绎法，推导出一系列，推导出一系列定理定理，形成的演绎，形成的演绎体系叫作体系叫作公理系统公理系统。 公理系统的组成：公理系统的组成： 符号集；符号集； 公式集公式集公式是用于表达命题的符号串；公式是用于表达命题的符号串； 公理集公理集公理是用于表达推理由之出发的初始肯定命题；公理是用于表达

2、推理由之出发的初始肯定命题； 推理规则集推理规则集推理规则是由公理及已证定理得出新定理的规则；推理规则是由公理及已证定理得出新定理的规则； 定理集定理集表达了肯定的所有命题。表达了肯定的所有命题。计算机学院3计算机学院3命题逻辑的公理系统命题逻辑的公理系统 定义定义3.1 3.1 命题逻辑的公理系统定义命题逻辑的公理系统定义: : 符号符号 命题变元命题变元p p1 1,p ,p2 2, ,p pn n 联结词符号联结词符号，; ; 括号括号(,)(,) 合式公式合式公式 命题变元是合式公式；命题变元是合式公式； 若若Q Q是公式，则是公式，则( (Q)是合式公式；是合式公式； 若若Q,RQ,

3、R是公式，则是公式，则(Q(QR)R)是合式公式。是合式公式。定义了所有合式公式定义了所有合式公式计算机学院4计算机学院4命题逻辑的公理系统命题逻辑的公理系统 有以下三个公理模式，其中有以下三个公理模式，其中P,Q,RP,Q,R可为任意公式可为任意公式 公理模式公理模式A1Q Q (RQ) 公理模式公理模式A2(P(P (QR) (PQ) (PR) 公理模式公理模式A3( (Q R) (RQ) 推理规则推理规则( (分离规则分离规则,MP,MP规则规则) ) 从从Q Q和和Q QR R推出推出R RQ Q和和Q QR R称为前提称为前提R R称为结论称为结论计算机学院5计算机学院5公理系统公理

4、系统 罗素公理系统罗素公理系统 Q Q Q Q Q Q Q QQ Q R R Q Q R RR R Q Q (P(PQ)Q)(P(P R RQ Q R)R) 弗雷格公理系统弗雷格公理系统 Q(RQ) (P(QR) (PQ) (PR) (P(QR) (Q(PR) (QR) (RQ) QQ QQ 卢卡西维茨公理系统卢卡西维茨公理系统 Q(RQ) (P(QR) (PQ) (PR) (QR) (R Q)计算机学院6计算机学院6缩写公式缩写公式 QR=(QR) QR= (QR) QR=(QR) (RQ) QR= (QR)计算机学院7计算机学院7公式复杂度公式复杂度 公式公式Q的复杂度表示为的复杂度表示为

5、FC(Q) 命题变元复杂度为命题变元复杂度为0 0，如果，如果Q是命题变元，则是命题变元，则FC (Q)=0。 如果公式如果公式Q= R，则，则FC (Q)=FC(R)+1。 如果公式如果公式Q=R1R2，则，则FC (Q)=maxFC(R1), FC(R2)+1。计算机学院8计算机学院8推理序列推理序列 已知已知Q成立成立， 证明证明RQ成立成立 A1= Q (RQ) A A1 A2= Q Q A3= RQ 推理序列推理序列 =Q，公式集，公式集前提前提A A1 1、A A2 2、A A3 3 推理序列推理序列A A3 3 结论结论计算机学院9计算机学院9演绎与推理序列演绎与推理序列 定义定

6、义3.2 3.2 设设是合式公式集是合式公式集, , Q Q是是合式公式，有推理步骤合式公式，有推理步骤A A1 1,A,A2 2, ,A An n，公式序列公式序列 1 1, , 2 2, , n n ，其中，其中A A1 1=1 1A A2 2=2 2. .A An n=n n ( ( n n =Q=Q) ) 每个每个 k k满足以下条件之一，满足以下条件之一， (1) (1) 是公理；是公理； (2) (2) k k ； (3) (3) 有有i,jk i,jk k k= = i i j j由由 i i, , j j用用MPMP规则规则推出。推出。 则称它为则称它为Q Q的从的从的一个的一

7、个推演推演( (演演绎绎) ), ,记为记为 Q Q。 称为推演的称为推演的前提集前提集，称称为为结论结论 推理序列推理序列 如果推理步骤序列如果推理步骤序列是是A A1 1,A,A2 2, ,A An n，则推则推理序列长度理序列长度n n。 推论：推论： 如果如果Q Q是公理或是公理或 Q ，则则 Q计算机学院10计算机学院10证明与定理证明与定理 如果存在从如果存在从推演出推演出Q，则记为，则记为Q 。 Q1,Q2,QnQ简记为简记为 Q1,Q2,Qn Q 如果如果为空集为空集 ，则记为，则记为Q。 如果如果Q，并且有推理步骤，并且有推理步骤A1,A2,An，则则A1,A2,An称为的一

8、个称为的一个证明证明。 如果如果Q ，则，则Q称为称为定理定理。计算机学院11计算机学院11 P, Q(PR)QR A1= P A1 A2=P (QP) A1 A1 A3=QP A2 = A1 A3 A4= Q(PR) A4 A5= (Q(PR)(QP)(QR) A2 A2 A6= (QP)(QR) A5 = A4A6 A7= (QR) A6 = A3A7 计算机学院12计算机学院12 例：例：(QR) (QQ) A1=Q (RQ) A A1 1 A2= (Q (RQ) (QR) (QQ) A A2 2 A3= (QR) (QQ) A2=A1A3计算机学院13计算机学院13重要定律重要定律 三

9、段论：三段论：Q, QR R 传递律：传递律：PQ,QRPR 反证律反证律：如果如果, Q R, , Q R,则则 Q 归谬律归谬律：如果如果, Q R, , Q R，则，则 Q计算机学院14计算机学院14重要定理重要定理 (P(QR) (Q(PR) (Q R)(PQ)(PR) (P Q)(QR)(PR) QQ QQ QQ (QR)(QR) Q(QR) R) (QR)( RQ) ( QR)( RQ) (Q R )(RQ) Q(Q R) ( QQ)(RQ) ( QQ)Q 计算机学院15计算机学院15三段论三段论 Q, QR R A1= QR A1 A2= Q A2 A3= R A1=A2 A3

10、计算机学院16计算机学院16传递律传递律 PQ,QRPR A1=(QR) (P (QR) A1 A1 A2=QR A2 A3=P (QR) A1=A2 A3 A4=(P (QR) (PQ) (PR) A2A2 A5=(PQ) (PR) A4=A3 A5 A6=(PQ) A6 A7=(PR) A5=A6A7计算机学院17计算机学院17 (P(QR)(Q(PR)A A1 1=(P =(P (Q (Q R) R) ( P ( P Q)Q)(P (P R) R) A A 2 2A A2 2= = ( P ( P Q)Q)(P (P R)R)(Q(Q( P ( P Q)Q)(P (P R) ) R) )

11、 A A 1 1A A3 3=(=(Q Q( P ( P Q)Q)(P (P R) R) ( Q( Q( P ( P Q) Q) (Q(Q(P (P R) R) A A 2 2A A4 4= (P = (P (Q (Q R) R) ( Q( Q( P ( P Q) Q) (Q(Q(P (P R) AR) A1 1, , A A2 2, , A A3 3 A A4 4A A5 5= =(P (P (Q (Q R) R) ( Q( Q( P ( P Q) Q) (Q(Q(P (P R)R) ( (P ( (P (Q (Q R) R) ( Q( Q( P ( P Q)Q) (P (P (Q (Q R

12、) R) (Q (Q (P (P R) R) A A 2 2A A6 6= =(P (P (Q (Q R)R)(Q(Q(P(PQ)Q)(P(P(Q (Q R)R)(Q(Q(P(PR) AR) A5 5=A=A4 4 A A6 6A A7 7= Q= Q(P(PQ) Q) A A 1 1A A8 8= (Q= (Q( P ( P Q) Q) ( (P ( (P (Q (Q R) R) ( Q( Q( P ( P Q) Q) A A 1 1A A9 9= (P = (P (Q (Q R) R) ( Q( Q( P ( P Q) AQ) A8 8=A=A7 7 A A9 9A A1010=(P =(

13、P (Q (Q R) R) (Q (Q (P (P R) AR) A6 6=A=A9 9 A A1010计算机学院18计算机学院18 (Q R)(P Q) (PR) A1= (Q R) (P (Q R) A1 A1 A2= (P(Q R) (P Q) (P R) A2 A2 A3= (Q R)(P Q)(P R) A1, A2 A3计算机学院19计算机学院19(PQ)(QR)(PR) A1=(Q R) (P Q) (P R) (Q R)(P Q) (PR) A2=(Q R) (P Q) (P R) (P Q)(Q R) (P R) (P(QR) (Q(PR) A3=(P Q)(QR)(PR)

14、A A2 2= =A A1 1 A A3 3计算机学院20计算机学院20 QQ A1=(Q (QQ)Q)(Q(QQ)(QQ) A A2 2 A2=Q (QQ) Q) A1A1 A3=(Q (QQ) (QQ) A1=A2A3 A4=Q (QQ) A1A1 A5=QQ A3=A4A5计算机学院21计算机学院21 QQ A1=Q (QQ) A1A1 A2= (QQ) ( QQ) A3A3 A3=( QQ) (QQ) A3A3 A4= Q (QQ) A1, A2, A3 A4 A5=(Q (QQ) (Q Q) (Q Q) A2A2 A6=(Q Q) (Q Q) A5=A4 A6 A7=(Q Q) Q

15、Q A8=Q Q A6=A7 A8 计算机学院22计算机学院22 Q Q A1= (Q Q)(QQ) A3 A3 A2= (Q Q) QQ A3= (QQ) (QQ ) A3 A3 A4= QQ A3=A2 A4 计算机学院23计算机学院23 (Q(QR)R)( (Q QR) R) A A1 1= R= RR R Q QQ Q A A2 2=(R=(RR)R)( (Q Q(R(RR) R) A A 1 1 A A3 3= =Q Q(R(RR) AR) A2 2=A=A1 1 A A3 3 A A4 4=(=(Q Q(R(RR)R)( ( (Q QR)R)( (Q QR)R) ) A A 2 2

16、 A A5 5= (= (Q QR)R)( (Q QR) AR) A4 4=A=A3 3 A A5 5 A A6 6= = Q Q Q Q Q QQ Q A A7 7=(=(Q Q Q)Q)(Q(QR)R)( (Q Q R) R) (P(P Q)Q)(Q (Q R)R)(P (P R)R) A A8 8=(Q=(QR)R)( (Q Q R) AR) A7 7=A=A6 6 A A8 8 A A9 9=(Q=(QR)R)( (Q QR) AR) A8 8, A, A5 5A A9 9计算机学院24计算机学院24 Q(QR) R)A A1 1=(Q=(QR)R)(Q(QR) R) Q QQ QA

17、A2 2=(Q=(QR)R)(Q(QR)R)( (Q Q( (Q QR R) )R) R) (P (P(Q(QR)R)(Q(Q(P(PR)R)A A3 3= Q= Q(Q(QR)R)R) R) A A2 2= =A A1 1 A A3 3计算机学院25计算机学院25(QR) ( R Q)A1 1= (QR)(QR) (Q(QR)R)( (Q QR) R) A2 2= ( Q R) ( R Q) A3A3A3 3= (QR)( Q R) A A2 2= =A A1 1 A A3 3 计算机学院26计算机学院26 ( Q R )( RQ)A1 1= ( QR)( RQ) (QR) ( R Q)A2

18、 2= QQ QQA3 3= (Q Q)( RQ)( RQ) (Q R)(P Q) (PR) A4 4= ( RQ)( RQ) A A3 3= =A A2 2 A A4 4A5 5= ( QR) ( RQ) A1, A4 A5计算机学院27计算机学院27 (Q R )(RQ) A1 1= (Q R )(RQ) A3A3 A2 2= (Q Q) (Q R ) (QR ) (PQ)(QR)(PR) A3 3= (Q Q) (Q Q) A4 4= (Q R ) (QR ) A A2 2= =A A3 3 A A4 4 A5 5= (Q R ) (RQ) A4, A1 A5计算机学院28计算机学院28

19、 Q(Q R)(涵义涵义) A1= Q(RQ) A1A1 A2= ( RQ) (QR) A3A3 A3= Q(QR) A1， A2 A3 计算机学院29计算机学院29 ( ( Q QQ)Q)(R(RQ)Q) A A1 1= = Q Q( (R RQ) Q) A1A1 A A2 2=(=(R RQ)Q)(Q(QR R) ) A3A3 A A3 3= = Q Q (Q(QR R) ) A A1 1, A, A2 2A A3 3 A A4 4=(=( Q Q(Q(QR)R) ( ( Q QQ)Q)( ( Q QR) R) A2A2 A A5 5=( =( Q Q Q) Q) ( ( Q Q R) A

20、R) A4 4=A=A3 3 A A5 5 A A6 6= (= ( Q Q R) R) (R(RQ) Q) A 3A 3 A A7 7=(=( Q QQ)Q)(R(RQ) AQ) A5 5, A, A6 6A A7 7计算机学院30计算机学院30 ( ( Q QQ)Q)Q Q A A1 1=(=( Q QQ)Q)( ( Q QQ)Q)Q) Q) ( ( Q QQ)Q)(R(RQ)Q) A A2 2=(=( Q QQ)Q)( ( Q QQ)Q)Q)Q) ( Q QQ)Q)( ( Q QQ) Q) ( ( Q QQ)Q)Q) Q) A2A2 A A3 3=(=( Q QQ)Q)( ( Q QQ)

21、Q)( ( Q QQ)Q)Q) AQ) A2 2=A=A1 1 A A3 3 A A4 4= (= ( Q QQ)Q) ( ( Q QQ) Q) A 1A 1 A A5 5=(=( Q QQ)Q)Q AQ A3 3=A=A4 4 A A5 5计算机学院31计算机学院31 QRQ A1= Q(RQ) A1A1 A2= QRQ QR=(QR)计算机学院32计算机学院32 QR RQA1 1= =(R(RQ)Q)(Q (Q R) R) (R(RQ)Q)(Q (Q R) R) A2 2=(=(R(RQ)Q)(Q (Q R)R) ( ( (Q(QR)R)(R(RQ)Q) (RQ)( Q R) A3 3=

22、 = (Q(QR)R)(R(RQ) Q) Q R = (QR)A4 4= = Q Q R R R R Q Q计算机学院33计算机学院33 QRQA1 1= Q(R Q) A1A1 A2 2= (RQ)(QR) (QR)(RQ)A3 3= = Q(Q R) A A1 1, A, A2 2A A3 3A4 4=(Q(Q R) ) (Q R)Q) (QR)(RQ)A5 5= = (Q R)Q A A4 4=A=A3 3 A A5 5A6 6= QR Q QR =(QR)计算机学院34计算机学院34 例：若例：若R，则则QR。 A1=C1 Ak-1=Ck-1 Ak=R R Ak+1= R (QR) A

23、1 Ak+2= QR Ak+1=Ak Ak+2 QR计算机学院35计算机学院35例：若例：若 PQ ， P (QR) ，则则 PR。A1=D1Am-1=Dm-1Am= PQ PQ Am+1=Dm+1Am+n-1=Dm+n-1Am+n= P (QR) P (QR) Am+n+1=(P(QR) ) (PQ) (PR) A A2 2Am+n+2=(PQ) (PR) Am+n+1=Am+nAm+n+2Am+n+3=PR Am+n+2=AmAm+n+3计算机学院36计算机学院36演绎定理演绎定理 Q R 当且当且 仅当仅当 QR 归纳基础：归纳基础：用关于用关于Q到到R的推演长度的推演长度n作归纳证明。

24、作归纳证明。 当当n=1时，时，R或为公理，或属于或为公理，或属于 ，或，或R是是Q。 若若R是公理，则是公理，则 A1=R A2= R(QR) A3= (QR) 所以所以 QR，从而从而 QR 若若 R ，则，则 A1=R A2= R(QR) A3= (QR) 有有 QR 若若R=Q，则，则 Q Q 所以所以 QQ计算机学院37计算机学院37演绎定理演绎定理(2)(2) 归纳假设：归纳假设：假设假设Q到到R的推演长度小于的推演长度小于n定理成立。定理成立。 归纳证明：当归纳证明：当Q到到R的推演长度等于的推演长度等于n时，有时，有 Q R A1=Q1 A2=Q2 Ai= PR Aj=P An

25、=R 从从的推演的推演 A1=D1 Am= QP Ak= Q (PR) Ak+1= Q (PR) (QP) (Q R) Ak+2= (QP)(Q R) Ak+3= (Q R) 因为因为i,jn,有所以有所以 Q P QP Q PR Q (PR)计算机学院38计算机学院38演绎定理演绎定理(3)(3) 到到QR 的推演的推演 由由 QR可知，有推理序列可知，有推理序列A1, A2, Am， 使得使得Am= QR 。 证明有证明有Q R 。因为。因为 有推理序列有推理序列A1, A2, Am，其中，其中 Am= QR Am+1= Q Am+2= R计算机学院39计算机学院39 (Q(QR) (QR

26、) 根据演绎规则根据演绎规则 (Q (Q R) Q R (Q (Q R) ,Q R A1= Q (Q R) A2= Q A3= Q R A4=R计算机学院40计算机学院40再看传递律再看传递律 PQ,QRPR (Q R) (P Q) (P R) (P Q) (Q R) (P R)计算机学院41计算机学院41 (P(QR) (Q(PR) 根据演绎规则根据演绎规则 P (Q R) Q (P R) P (Q R) ,Q P R P (Q R) ,Q, P R A1= P(Q R) A2= P A3= Q R A4=Q A5=R计算机学院42计算机学院42反证律反证律 如果如果, Q R, , Q R

27、,则 QA1 1= = Q RA2 2= = Q RA3 3= (= ( QR)(R Q )A4 4= = RQ A5 5= = QQA6 6= = (Q Q)QA7 7= = Q 计算机学院43计算机学院43归谬律归谬律 如果如果, Q R, , Q R，则，则 QA1 1= = Q RA2 2= = Q RA3 3= = RQA4 4= = Q Q A5 5= = = QQA6 6= = = Q QA7 7= = ( Q Q) QA8 8= = Q 计算机学院44计算机学院44 P,QP Q P,Q, (P Q)Q， P,Q, (P Q) Q A1 1= PA2 2= Q A3 3= (P

28、 Q)A4 4= (P Q) (P Q) A5 5= P QA6 6= Q 所以有所以有P,Q (P Q)，即，即P,Q P Q计算机学院45计算机学院45 (PQ) (PR) (PQ R)演绎定理：演绎定理：(PQ) (PR) ，P Q RA1 1= ( PQ) (PR)A2 2= PA3 3= ( PQ) (PR) ( PQ) A4 4= PQA5 5= QA6 6= ( PQ) (PR) ( PR)A7 7= PRA9 9= RA1010= Q R计算机学院46计算机学院46主要内容主要内容 概述概述 命题逻辑公理系统命题逻辑公理系统 谓词逻辑公理系统谓词逻辑公理系统 公理系统性质公理系

29、统性质 理论与模型理论与模型 判定问题判定问题 总结总结计算机学院47计算机学院47谓词逻辑的公理系统谓词逻辑的公理系统 定义定义3.4 3.4 谓词逻辑的公理系统定义如下：谓词逻辑的公理系统定义如下： (1) (1) 符号：符号： 个体变元个体变元x x1 1,x ,x2 2 , , 个体常元个体常元a a1 1,a ,a2 2 , , 对每个正整数对每个正整数n n，n n元函数符号元函数符号f f1 1,f ,f2 2 , , 对每个正整数对每个正整数m m，m m元谓词符号元谓词符号P P1 1,P ,P2 2 , , 联结词符号联结词符号 ， 量词符号量词符号 逗号，逗号， 括号括号

30、(,)(,)计算机学院48计算机学院48 (2) (2) 项定义如下：项定义如下： 个体常元是项；个体常元是项； 个体变元是项；个体变元是项； 若是若是t t1 1,t,tn n项，则是项，则是f fi i(t (t1 1,t,tn n) )项。项。 (3) (3) 公式定义如下：公式定义如下： 若是若是t t1 1,t,tn n项，则项，则P Pi i(t (t1 1,t,tn n) )是公式。是公式。 若若A A是公式，则（是公式，则（A A）是公式；）是公式； 若若A,BA,B是公式，则（是公式，则（A AB B）是公式；）是公式； 若若A A是公式，则（是公式，则（xA A）是公式。）

31、是公式。计算机学院49计算机学院49 公理公理 公理模式公理模式A A1 1A A (BA) 公理模式公理模式A A2 2(A(A (BR) (AB) (AR) 公理模式公理模式A A3( (A B) (BA) 公理模式公理模式A A4 4 xAAtx 其中项其中项t t对于对于A A中的中的x x可代入可代入 公理模式公理模式A A5 5 x( ( AB) (A xB)其中其中x不是不是A A中自由变元中自由变元 公理模式公理模式A A4 4说明说明 如果公式如果公式A A对于一对于一切切x x成立，则公式成立，则公式A A对于任意对于任意t t成立。成立。 但是，但是， 项项t t中没有中

32、没有约束变元约束变元 在自然数论域在自然数论域xy(xy) y(yy)计算机学院50计算机学院50 5) 5) 推理规则：推理规则： 分离规则（简称分离规则（简称MPMP规则）：规则）： 从从A A和和A AB B推出推出B B。 概括规则（简称概括规则（简称UGUG规则）：规则）： 从从A A推出（推出（x A A）。）。 概括规则说明概括规则说明 x x是自由出现是自由出现x不是常元不是常元x不是选择变元不是选择变元计算机学院51计算机学院51缩写公式缩写公式 AB=(AB) AB= (AB) AB=(AB) (BA) AB= (AB) xA(x)=xA(x)计算机学院52计算机学院52公

33、式复杂度公式复杂度 公式公式A的复杂度表示为的复杂度表示为FC(A) 命题变元复杂度为命题变元复杂度为0 0，如果，如果P P是谓词变元，则是谓词变元，则FC (P)=0FC (P)=0。 如果公式如果公式A=A= B B，则，则FC (A)=FC(B)+1FC (A)=FC(B)+1。 如果公式如果公式A=B1A=B1B2B2，则，则FC (A)=maxFC(B1), FC(B2)+1FC (A)=maxFC(B1), FC(B2)+1。 如果公式如果公式A= A= x B B，则，则FC (A)= FC(B)+1FC (A)= FC(B)+1。计算机学院53计算机学院53演绎与证明演绎与证

34、明 定义定义3.2 3.2 设设是合式公式集是合式公式集, , Q Q是是合式公式，有推理步骤合式公式，有推理步骤A A1 1,A,A2 2, ,A An n，公式序列公式序列 1 1, , 2 2, , n n ，其中，其中A A1 1=1 1A A2 2=2 2. .A An n=n n ( ( n n =Q=Q) ) 每个每个 k k满足以下条件之一，满足以下条件之一， (1) (1) 是公理；是公理； (2) (2) k k ； (3) (3) 有有i,jk i,jk k k= = i i j j由由 i i, , j j用用MPMP规则规则推出。推出。 (4) (4) 有有ijij使

35、使A Aj j= = x xA Ai i由用由用UGUG规则推出规则推出 则称它为则称它为Q Q的从的从的一个的一个推演推演( (演演绎绎) ), ,记为记为 Q Q。 称为推演的称为推演的前提集前提集，称称为为结论结论 序列序列A A1 1,A,A2 2, ,A An n，称称为从为从演绎出演绎出n n的的一个一个证明证明。 nn也称由也称由可可证明证明n n。 推理序列推理序列 如果推理步骤序列如果推理步骤序列是是A A1 1,A,A2 2, ,A An n，则推则推理序列长度理序列长度n n。 推论：推论： 如果如果Q Q是公理或是公理或 Q ，则则 Q计算机学院54计算机学院54 x(

36、P(x)P(x)A1 1= = P(x) P(x)A2 2= = P(x)P(x)A3 3= = x(P(x)P(x)计算机学院55计算机学院55 xP(x) xP(x)A1 1= xP(x) P(y)A2 2=(xP(x) P(y) (P(y) xP(x) )A3 3= P(y) xP(x)A4 4= P(y) P(y) A5 5= P(y) xP(x)A6 6= xP(x) P(y)A7 7= xP(x) xP(x)计算机学院56计算机学院56主要性质主要性质 xR(x) y R(y) xR(x) y R(y) xR(x) xR(x) x(P(x) Q(x) (xP(x) x Q(x) x

37、(P(x) Q(x) (xP(x) x Q(x) x(P(x) Q(x) (xP(x) xQ(x) x(P(x) Q(x) (xP(x) xQ(x) x(P(x) Q(x) (xP(x) xQ(x) xP(x) xQ(x)x(P(x) Q(x) xy R(x,y) yxR(x,y) xy R(x,y) yxR(x,y) xyR(x,y) yx R(x,y) xyR(x,y) xR(x,x) xR(x,x) xyR(x,y) 计算机学院57计算机学院57 xQ(x) xQ(x) y Q(y) (yy Q(y) (y不在不在Q Q中出现中出现) ) A A1 1= = xQ(x) xQ(x) Q(

38、y)Q(y) A A2 2= = y y( ( xQ(x) xQ(x) Q(y)Q(y) A A3 3= = y y( ( xQ(x) xQ(x) Q(y)Q(y)( ( xQ(x) xQ(x) y Q(y)y Q(y) A A4 4= = xQ(x) xQ(x) y Q(y)y Q(y)计算机学院58计算机学院58 x x y R(x,y)y R(x,y)y y xR(x,y)xR(x,y) A A1 1= = x x y R(x,y) y R(x,y) y R(x,y)y R(x,y) A A2 2= = y R(x,y)y R(x,y)R(x,y)R(x,y) A A3 3= = x x

39、 y R(x,y) y R(x,y) R(x,y)R(x,y) A A4 4= = x x ( ( x x y R(x,y) y R(x,y) R(x,y)R(x,y) A A5 5= = x x ( ( x x y R(x,y) y R(x,y) R(x,y) R(x,y) ( ( x x y R(x,y) y R(x,y) xR(x,y)xR(x,y) ) A A6 6= =( ( x x y R(x,y) y R(x,y) xR(x,y)xR(x,y) ) A A7 7= = y y( ( x x y R(x,y) y R(x,y) xR(x,y)xR(x,y) ) A A8 8= =

40、y y( ( x x y R(x,y) y R(x,y) xR(x,y)xR(x,y) ) ( ( x x y R(x,y)y R(x,y)y y xR(x,y)xR(x,y) ) A A9 9= =( ( x x y R(x,y)y R(x,y)y y xR(x,y)xR(x,y) )计算机学院59计算机学院59 x x yR(x,y)yR(x,y)xR(x,x)xR(x,x) A A1 1= = x x yR(x,y)yR(x,y)yR(x,y)yR(x,y) A A2 2= = yR(x,y) yR(x,y) R(x,x)R(x,x) A A3 3= = x x yR(x,y)yR(x,

41、y) R(x,x)R(x,x) A A4 4= = x x ( ( x x yR(x,y)yR(x,y) R(x,x)R(x,x) A A5 5= = x x ( ( x x yR(x,y)yR(x,y) R(x,x) R(x,x) ( ( x x yR(x,y)yR(x,y)xR(x,x)xR(x,x) ) x x yR(x,y)yR(x,y)xR(x,x)xR(x,x)计算机学院60计算机学院60 Q(c) Q(c) xQ(x) xQ(x) A A1 1= = x x Q(x) Q(x) Q(c)Q(c) A A2 2=(=( x x Q(x) Q(x) Q(c) Q(c) ( (Q(c)

42、 Q(c) x x Q(x)Q(x) A A3 3= =Q(c) Q(c) x x Q(x)Q(x) A A4 4= = Q(c) Q(c) Q(c)Q(c) A A5 5= = Q(c) Q(c) x x Q(x)Q(x) A A6 6= = Q(c) Q(c) xQ(x)xQ(x)计算机学院61计算机学院61 Q(c) Q(c) xQ(x)xQ(x) A A1 1= = xQ(x) xQ(x) Q(c)Q(c) A A2 2=(=( xQ(x) xQ(x) Q(c) Q(c) ( ( Q(c)Q(c) xQ(x)xQ(x) A A3 3= = Q(c)Q(c) xQ(x) xQ(x) 计算

43、机学院62计算机学院62 xQ(x)xQ(x)xQ(x)xQ(x) A A1 1= = xQ(x)xQ(x) Q(c) Q(c) A A2 2= = Q(c) Q(c) xQ(x) xQ(x) A A3 3= = xQ(x)xQ(x) xQ(x) xQ(x) 计算机学院63计算机学院63 x(P(x)x(P(x)Q(x)Q(x) ( ( xP(x) xP(x) x x Q(x) Q(x) A A1 1= = ( ( x(P(x)x(P(x)Q(x)Q(x)(P(x)(P(x)Q(x)Q(x) A A2 2= =(P(x)(P(x)Q(x)Q(x)( ( xP(x)xP(x) P(x) P(x)

44、( ( xP(x) xP(x) Q(x)Q(x) A A3 3= (= ( x(P(x)x(P(x)Q(x)Q(x) ( ( xP(x)xP(x)P(x)P(x)( ( xP(x) xP(x) Q(x)Q(x) A A4 4= (= ( x(P(x)x(P(x)Q(x)Q(x) ( ( xP(x) xP(x) Q(x)Q(x) A A5 5= = x (x ( x(P(x)x(P(x)Q(x)Q(x) ( ( xP(x) xP(x) Q(x)Q(x) A A6 6= = x(P(x)x(P(x)Q(x)Q(x)x x ( ( xP(x) xP(x) Q(x)Q(x) A A7 7= = x x

45、 ( ( xP(x) xP(x) Q(x) Q(x) ( ( xP(x) xP(x) x x Q(x) Q(x) A A8 8= = x(P(x)x(P(x)Q(x)Q(x) ( ( xP(x) xP(x) x x Q(x) Q(x)计算机学院64计算机学院64 (xP(x) xQ(x) x(P(x) Q(x) A1 1= (xP(x) xQ(x) xP(x) A2 2= xP(x) P(x)A3 3= (xP(x) xQ(x) P(x)A4 4= (xP(x) xQ(x) xQ(x)A5 5= xQ(x) Q(x)A6 6= (xP(x) xQ(x) Q(x)A7 7= (xP(x) xQ(

46、x) P(x) Q(x)A8 8=x(xP(x) xQ(x) P(x) Q(x)A9 9= (xP(x) xQ(x) x(P(x) Q(x)计算机学院65计算机学院65演绎定理演绎定理 A A B B 当且仅当当且仅当 A AB B 因为因为A AxA不是有效公式，不是有效公式，A A 可证，可证， xA可证？ 变元变元 约束变元约束变元 自由变元自由变元 出现出现 约束出现约束出现 自由出现自由出现计算机学院66计算机学院66演绎定理演绎定理 A A B B，且且A A为闭公式为闭公式， 当且仅当当且仅当 A AB B 归纳基础：归纳基础：用关于用关于 A A 到到B B的推演长度的推演长度

47、n n作归纳证明。作归纳证明。 当当n=1n=1时，时，B B或为公理，或属于或为公理，或属于 ，或，或B B是是A A。 若若B B是公理，则是公理，则A A1 1=B=BA A2 2= B= B(AB)A A3 3= = (AB)所以所以 AB，从而从而 A AB B 若若 B B ，则，则 若若B=AB=A，则，则 A A A AA A1 1=B =B 所以所以 A AA AA A2 2= B= B(AB)A A3 3= = (AB)有有 A AB B计算机学院67计算机学院67演绎定理演绎定理(2)(2) 归纳假设：归纳假设：假设假设 A A 到到B B的推演长度小于的推演长度小于n

48、n定理成立。定理成立。 归纳证明：当归纳证明：当 A A 到到B B的推演长度等于的推演长度等于n n时，并且时，并且B B由分离由分离规则推出有规则推出有 A A B B A A1 1=B=B1 1 A A2 2=B=B2 2 A An n=B=B A Ai i= = R R A Aj j= = R R B B 从从 的推演的推演 A A1 1=D=D1 1 A Am m= A= AR R A Ak k= A= A (R (RB B) ) A Ak+1k+1=(=(A A (R (R B B) ) (A A R R) ) (A (A B B) ) A Ak+2k+2= =(A A R R)

49、) (A (A B B) ) A Ak+3k+3=A =A B B 因为因为i,jn,i,jn,所以所以 A A R R A AR R A A R RB B A A (R (RB B) )计算机学院68计算机学院68演绎定理演绎定理(3)(3) 归纳证明：当归纳证明：当 A A 到到B B的推演长度等于的推演长度等于n n时，并且时，并且B B由综合规则推出，所以由综合规则推出，所以 从从 的推演的推演A A1 1= =B B1 1. . A Am m= = A A R R A Am+1m+1= =x(A A R R )A Am+2m+2= = A A xR A A为闭公式为闭公式 A B A

50、1=B1 A2=B2 An-1= R An= xR An=B 因为因为 A RA R推演推演长度等于长度等于n-1n-1，所以，所以 A AR R计算机学院69计算机学院69演绎定理演绎定理(4)(4) 到到A AB B 的推演的推演 由由 A AB B可知，有推理序列可知，有推理序列A A1 1, A, A2 2, A, Am m，使得，使得A Am m= = A AB B 。 证明有证明有 A A B B 。因为。因为 有推理序列有推理序列A A1 1, A, A2 2, A, Am m，其中，其中 A Am m= = A AB B A Am+1m+1= = A A A Am+2m+2=

51、= B B计算机学院70计算机学院70 选择规则：选择规则： xP(x)P(c) 引入规则：引入规则： P(c) xP(x) 计算机学院71计算机学院71 x(P(x) Q(x) (xP(x) xQ(x) ) x(P(x) Q(x)，xP(x) xQ(x) A1 1= = x(P(x) Q(x) A2 2= = x(P(x) Q(x) (P(c) Q(c) A3 3= = P(c) Q(c) A4 4= = xP(x) A5 5= = xP(x) P(c) A6 6= = P(c) A7 7= = Q(c) A8 8= =Q(c) xQ(x) A9 9= = xQ(x)计算机学院72计算机学院

52、72 x(P(x) Q(x) (xP(x) xQ(x) x(P(x) Q(x) xP(x) xQ(x)A1 1= x(P(x) Q(x)A2 2= x(P(x) Q(x) P(x) Q(x)A3 3= P(x) Q(x)A4 4= P(x) Q(x) P(x) A5 5= P(x) A6 6= xP(x) A7 7= P(x) Q(x) Q(x) A8 8= Q(x) A9 9= xQ(x)A1010= xP(x) xQ(x)计算机学院73计算机学院73 x(P(x,y)Q(x,y)( xP(x,y) xQ(x,y) )？ x(P(x,b)Q(x,b)( xP(x, b) xQ(x, b) )

53、计算机学院74计算机学院74 定理定理3.11 3.11 设设c1, cm是在是在语句集中不出现的不同常元，语句集中不出现的不同常元， y1, , ym是在公式是在公式Q(c1, cm)中不出现的不同变元，用中不出现的不同变元，用y1, , ym分别同时代替分别同时代替Q(c1, cm)中的中的c1, , cm得到得到Q(y1, ym) 。若。若 Q(c1, cm)，则，则 Q(y1, ym) 。计算机学院75计算机学院75 证明步骤证明步骤A1 1 An n： (1)(1)使用公理模式对应使用公理模式对应; ; (2)(2)使用使用Ak k对应对应; ; (3)(3) 使用使用MPMP规则对

54、应；规则对应； (4)(4)使用使用UGUG规则对应。规则对应。 证明：证明： Q(c1, cm) A1 1=Q1 (c1, cm) An n=Qn (c1, cm) An n=Q (c1, cm) z1, , zn是在是在中不出现的不同变中不出现的不同变元，并且元，并且z1, zn y1, yn=。 A1 1=Q1 (z1, zm) An n=Qn (z1, zm) An n=Q (z1, zm) An+1= z1 znQ (z1, zm) An+2= z1 znQ (z1, zm) Q (y1, ym) An+3=Q (y1, ym)计算机学院76计算机学院76 x(P(x,y)Q(x,y

55、)(xP(x,y)xQ(x,y) ) x(P(x,c)Q(x,c)(xP(x,c)xQ(x,c) ) x(P(x,c)Q(x,c), xP(x,c) xQ(x,c) A1 1= = x(P(x,c)Q(x,c) A2 2= = P(x,c)Q(x,c) A3 3= = xP(x,c) A4 4= = P(x,c) A5 5= = Q(x,c) A6 6= = xQ(x,c)计算机学院77计算机学院77 若若 A(x)B(x)，则则 xA(x) x B(x) A1 1= =C1 Am m= = A(x)B(x) Am+1m+1= = x A(x)A(x) Am+2m+2= =xA(x)B(x)

56、Am+3m+3= =x( (xA(x)B(x) Am+4m+4= =x( (xA(x)B(x)(xA(x)xB(x) Am+5m+5= =xA(x)x B(x) 问题是什么问题是什么? ? X X是自由出现是自由出现计算机学院78计算机学院78主要内容主要内容 概述概述 命题逻辑公理系统命题逻辑公理系统 谓词逻辑公理系统谓词逻辑公理系统 公理系统性质公理系统性质 理论与模型理论与模型 判定问题判定问题 总结总结计算机学院79计算机学院79可靠性可靠性 可靠性定理：若可靠性定理：若 Q ，则，则 Q。 证明：设证明：设A A1 1,A,A2 2, ,A An n是是Q Q的从的从 的推演。归纳证

57、明：对于的推演。归纳证明：对于 Q i i ，有有 Q i i，i=1,2,i=1,2,n ,n n=1n=1时，若时，若Q i是公理，则是公理，则Q i是永真式。若是永真式。若Q i，则，则 Q i ， 有有 Q i i 公理模式公理模式A1v(Qv(Q (RQ) v(Q)(v(R)v(Q) 如果如果v(Q)=1，则v(Q)(v(R)v(Q)=1。 如果如果v(Q)=0，则v(Q)(v(R)v(Q)=1。 公理模式公理模式A2(P(P (QR) (PQ) (PR)同理同理v(Pv(P (QR) (PQ) (PR)=1)=1 公理模式公理模式A3( (Q R) (RQ)同理同理v(v(Q R)

58、 (RQ)=1)=1计算机学院80计算机学院80可靠性定理可靠性定理 若若Q i，则，则 Q i, , 对于对于v()=1， Ai有有v(Q i)=1，所以，所以 Q i 假设假设inin时定理成立时定理成立 证明证明i=ni=n时，时， 设设Q i由由Q j, , Q k用用MPMP规则推出，其中规则推出，其中j,kij,ki， Q k为为Q j Qi。 由归纳假设知，由归纳假设知， Qj且且 Qj Qi ， 所以所以 Qj， Qj Qi Qi 。 因此因此 Qn 即即 Q。计算机学院81计算机学院81协调协调 定义定义3.3 3.3 如果对于每个公式如果对于每个公式Q Q， Q Q，则，则

59、 称不协调，称不协调，否则称否则称 协调。协调。计算机学院82计算机学院82 定理定理3.3 3.3 若若 Q Q Q Q ，则，则 不协调。不协调。 证明：证明： Q Q Q Q即为公式即为公式 (Q QQ Q)A A1 1= = (Q QQ Q)A A2 2= = (Q QQ Q) (R (Q QQ Q) )A A3 3= =R (Q QQ Q) A A4 4= (= (R (Q QQ Q) (Q QQ Q) R )A A5 5= = (Q QQ Q) R A A6 6= = (Q QQ Q) A A7 7= = R R计算机学院83计算机学院83 定理定理3.4 3.4 若若 协调，则协

60、调，则 可满足。可满足。计算机学院84计算机学院84完备性定理完备性定理 完备性定理：若完备性定理：若 Q Q ，则，则 Q Q。 证明：证明： 若真值赋值若真值赋值v v满足满足 ，则它必满足，则它必满足Q ,Q ,即不可满足即不可满足 Q Q， 所以所以 Q Q 不可满足。不可满足。 因此，因此， Q Q 不协调。不协调。 所以有所以有 Q QQ Q。 有演绎定理有有演绎定理有 Q QQ Q。 由由( ( Q QQ)Q)Q Q，因此，因此，QQ计算机学院85计算机学院85可靠性定理可靠性定理(1 )(1 )公理公理1-31-3 可靠性定理：若可靠性定理：若 Q Q ，则，则 Q Q。 证明