• 公理集
–公理是用于表达推理由之出发的初始肯定命题；
• 推理规则集
计算机学院
–推理规则是由公理及已证定理得出新定理的规则；
• 定理集
–表达了肯定的所有命题。
计算机学院
2
2
命题逻辑的公理系统
▪ 定义3.1 命题逻辑的公理系统定义:
▪ 符号
• 命题变元p1,p2,…pn
• 联结词符号，; • 括号(,)
• 命题变元复杂度为0，如果Q是命题变元，则FC (Q)=0。 • 如果公式Q=R，则FC (Q)=FC(R)+1。 • 如果公式Q=R1R2，则FC (Q)=max{FC(R1), FC(R2)}+1。
计算机学院
计算机学院
7
7
推理序列
▪ 已知Q成立， 证明R→Q成立
▪ A1= Q (RQ) ▪ A2= Q ▪ A3= RQ
计算机学院
11
11
▪ 例：├(QR) (QQ)
▪ A1=Q (RQ)
A1
▪ A2= (Q (RQ)) ((QR) (QQ)) A2
▪ A3= (QR) (QQ)
A2=A1A3
计算机学院
计算机学院
12
12
重要定律
▪ 三段论：Q, QR ├R ▪ 传递律：PQ,QR├PR
▪ 反证律：如果Γ, Q├ R, Γ, Q├R,则Γ├ Q ▪ 归谬律：如果Γ, Q├ R, Γ, Q├ R，则Γ├ Q
计算机学院
10
10
▪ P, Q(PR)├QR
▪ A1= P
A1Γ
▪ A2=P (QP)
A1
▪ A3=QP
A2 = A1 A3
▪ A4= Q(PR)
A4 Γ
▪ A5= (Q(PR))((QP)(QR))
A2
▪ A6= (QP)(QR)
计算机学院A5 = A4A6
▪ A7= (QR)
A6 = A3A7
计算机学院
计算机学院
14
14
三段论
▪ Q, QR ├R ▪ A1= QR
▪ A2= Q ▪ A3= R
A1 Γ A2 Γ A1=A2 A3
计算机学院
计算机学院
15
15
传递律
▪ PQ,QR├PR
▪ A1=(QR) (P (QR))
A1
▪ A2=QR
A2 Γ
▪ A3=P (QR)
A1= 若Q是公式，则(Q)是合式公式；计算机学院 • 若Q,R是公式，则(QR)是合式公式。
▪ 定义了所有合式公式
计算机学院
3
3
命题逻辑的公理系统
▪ 有以下三个公理模式，其中P,Q,R可为任意公式
• 公理模式A1
–Q (RQ)
• 公理模式A2
–(P (QR)) ((PQ) (PR))
▪ 卢卡西维茨公理系统 ▪ Q(RQ)
▪ QQ 计算机学院
▪ (P(QR)) ((PQ) (PR))
▪ (QR) (R Q)
计算机学院
5
5
缩写公式
▪ QR=(QR) ▪ QR= (QR) ▪ QR=(QR) (RQ) ▪ QR= (QR)
计算机学院
计算机学院
6
6
公式复杂度
▪ 公式Q的复杂度表示为FC(Q)
• A1=α1
• A2=α2
• ….
• An=αn
(αn =Q)
▪ 每个αk满足以下条件之一，
▪ 推理序列
• 如果推理步骤序列
是推理A1序,A列2,…长A度nn，。则
• (1) α是公理；
▪ 推论：
• (2) α kΓ； • (3) 有i,j<k αk= αi αj由αi, αj用MP规则
计算机•学如院Γ果，Q则是Γ公├ 理Q 或 Q
主要内容
▪ 概述 ▪ 命题逻辑公理系统 ▪ 谓词逻辑公理系统 ▪ 公理系统性质 ▪ 理论与模型 ▪ 判定问题 ▪ 总结
计算机学院
计算机学院
1
1
逻辑公理系统
▪ 公理系统
• 从一些公理出发，根据演绎法，推导出一系列定理，形成的演绎体 系叫作公理系统。
▪ 公理系统的组成：
• 符号集；
• 公式集
–公式是用于表达命题的符号串；
• 公理模式A3
–(Q R) (RQ)
▪ 推理规则(分离规则,MP规则)
• 从Q和QR推出R
计算机学院
–Q和QR称为前提
–R称为结论
计算机学院
4
4
公理系统
▪ 罗素公理系统 ▪ QQ Q ▪ QQR ▪ QRRQ ▪ (PQ)(PRQR)
▪ 弗雷格公理系统 ▪ Q(RQ) ▪ (P(QR)) ((PQ) (PR)) ▪ (P(QR)) (Q(PR)) ▪ (QR) (RQ) ▪ QQ
▪ 推理序列 • Γ=Q，公式集——前提 • A1、A2、A3 ——推理序列 • A3 ——结论
A1
QΓ
计算机学院
计算机学院
8
8
演绎与推理序列
▪ 定义3.2 设Γ是合式公式集, Q是合 式公式，有推理步骤A1,A2,…An， 公式序列α1, α2,… αn ，其中
▪ Γ称为推演的前提集， 称α为结论
▪ A4=(P (QR)) ((PQ) (PR))
A2
▪ A5=(PQ) (PR) ▪ A6=(PQ)
计算机学院 A4=A3 A5 A6 Γ
▪ A7=(PR)
A5=A6→A7
计算机学院
16
16
▪ ├ (P(QR))(Q(PR))
▪ A1=(P (Q R)) (( P Q)(P R))
A2
▪ A2= (( P Q)(P R))(Q(( P Q)(P R) ))
A1
▪ A3=(Q(( P Q)(P R))) (( Q( P Q)) (Q(P R))) A 2
▪ A4= ((P (Q R)) (( Q( P Q)) (Q(P R))))
A1, A2, A3├ A4
▪ A5=((P (Q R)) (( Q( P Q)) (Q(P R))))
▪
( (P (Q R)) ( Q( P Q)) (P (Q R)) (Q (P R))) A 2
计算机学院
计算机学院
13
13
重要定理
▪ ├ (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
推出。
▪ 则称它为Q的从Γ的一个推演(演绎), 记为Γ├ Q。
计算机学院
9
9
证明与定理
▪ 如果存在从Γ推演出Q，则记为Γ├Q 。 ▪ {Q1,Q2,…Qn}├Q简记为
• Q1,Q2,…Qn ├Q
▪ 如果Γ为空集 ，则记为├Q。
▪ 如则果 A1Γ,A├2,Q…，A并n称且为有的推一理个步证计骤算明机A。1学,A院2,…An， ▪ 如果├Q ，则Q称为定理。